2015 was an active and productive year at Galois. From numerous awards, to new projects and spin-offs, to a vast array of publications and talks, Galwegians contributed to a wide range of fields this year. Below, we highlight some of the contributions we made in 2015.
Overview
In our core fields of cryptography and formal verification we further delved into secure computation, the groundbreaking process of using sensitive, encrypted data without decrypting it. We also shared formal verification methods and tools that ensure code correctness and minimize exploitable flaws. Finally, we announced a public preview of the Software Analysis Workbench (SAW), a toolset that leverages automated SAT and SMT solvers to formally verify properties of code.
Relating to cybersecurity, we explored using unikernels for increased security and resource efficiency. We wrote numerous articles in national publications on computer security, network security, data privacy, and mitigating IoT vulnerabilities. Galois technical staff were quoted on articles about election systems, vehicle security, and cybersecurity in general.
In 2015, we expanded into a relatively new field for us: the transparency and reliability of election systems. We were part of a team that released a comprehensive study on the feasibility of Internet voting. We also presented a variety of publications and talks on the transparency and trustworthiness of election systems. Our contributions included speaking before the San Francisco Election Commission on the benefits of open source software for elections technology.
This year we also made a significant number of contributions on the topic of the security and reliability of cyber-physical systems. We presented practical tools and methods to secure vehicles like UAVs and automobiles, making them invulnerable to a wide range of vulnerabilities. One paper detailed a comprehensive approach to securing the automobile that would start to address the cyber reliability of today’s automobiles. Other publications presented programming languages that can produce secure software for embedded systems. Our work on securing UAVs and automobiles was also featured on national media several times throughout the year.
This year, Galois and Tozny, our mobile security and identity spin-off, announced a $1.86M award from the National Institute of Science and Technology (NIST) to build a secure data storage system that enables next-generation IoT capabilities without sacrificing privacy. We announced three other major awards, and won many more. We also announced a new spin-off, Sailfan Research, that provides data analytics services in audio, video, and signal analysis.
Below you will find some of the intellectual contribution highlights of 2015 by field. Happy holidays from everyone at Galois; we wish you the best in the year to come.
Cryptography
Computing with Data Privacy: Steps toward Realization. IEEE Security & Privacy, 2015
Dr. David Archer, Galois’s Cryptography Research Lead, and Prof. Kurt Rohloff of the New Jersey Institute of Technology published an article for the IEEE Security and Privacy magazine on the topic of groundbreaking process of computing on sensitive, encrypted data without decrypting it. The method has major implications for businesses that would benefit from sharing data, yet need to keep that data private. The article looks at two new cryptographic methods: linear secret sharing (LSS) and fully homomorphic encryption (FHE).
Maturity and Performance of Programmable Secure Computation. IACR Cryptology, 2015
Dr. David Archer was part of a team that published a paper reviewing the results of U.S. and European secure computation research programs and other published literature to present the state of the art in what can be achieved with today’s secure computing technology. The team also included Dan Bogdanov, Benny Pinkas, and Pille Pullonen.
Applying Satisfiability to the Analysis of Cryptography. SAT 2015
Dr. Aaron Tomb, Galois’s Software Correctness Research Lead, delivered an invited talk on applying satisfiability to the analysis of cryptography at SAT 2015, the International Conference on Theory and Applications of Satisfiability Testing. In the talk, Dr. Tomb walked through the properties of cryptographic code that are within the reach of existing solvers, and described some of the tools in applying SAT solvers to cryptographic algorithms. Find the full abstract here, the slide deck here, and a collection of examples here.
Encrypting strings in Android: Let’s make better mistakes
Tozny, Galois’s mobile security and identity spin-off, released an open source Android class for encrypting and decrypting strings after a review of commonly available encryption code found online revealed serious flaws in most libraries. Watch Isaac Potoczny-Jones’s talk on the topic here.
Don’t be a Monkey: Do Crypto Right. BSides PDX 2015
Dr. Dylan McNamee and Dr. Joe Kiniry held a workshop at this year’s BSides PDX conference on implementing correct cryptographic code. In the two-part workshop, McNamee and Kiniry walked through using Galois’s Cryptol and other tools to verify that C and Java crypto implementations match the specification, ensuring that crypto implementations are free of bugs, and using Microsoft Research’s F* tool and others to specify, reason about, and synthesize code for crypto protocols.
High Assurance Cryptography Synthesis with Cryptol. HCSS 2015
Dr. Joe Kiniry presented a set of new backends for Galois’s open source Cryptol toolset and the Galois Software Assurance Workbench (SAW). The backends are capable of synthesizing formally verified implementations and test benches for arbitrary cryptographic algorithms, and target C, JCM, CHDL, and Verilog and will produce Cryptol-independent evidence of the synthesized code’s correctness.
Formal methods and verification
Multi-Language and Multi-Prover Verification with SAWScript. HCSS 2015
Dr. Aaron Tomb demonstrated SAWScript, Galois’s software analysis orchestration tool, at HCSS 2015. Dr. Tomb demonstrated using SAWScript to verify multiple programming languages using multiple provers. An integrated, interactive environment, SAWScript allows an automated and integrated proof process, replacing what would otherwise have been a tedious and error-prone effort of manually combining results from a collection of subsidiary proof attempts. SAWScript has been used to verify equivalence of a number of production-quality algorithms, including implementations of Suite B cryptographic primitives from the OpenSSL and BouncyCastle libraries. This talk demonstrated the use of SAWScript on a number of examples of verification and analysis.
Frama-C at Galois. Frama-C Day at CEA
Dr. Aaron Tomb gave a talk at the 2015 Frama-C Day about the ways in which Galois is using Frama-C or may use it in the future. It covered using Frama-C to verify unannotated programs, inspired by work on STORM; application of Frama-C to verifying a fragment of the kLIBC library; and the potential use of Frama-C to verify code generated by Ivory or Cryptol.
Model checking distributed mandatory access control policies. ACM Transactions on Information and System Security, 2015
Dr. Lee Pike was part of a team that published a paper on model checking techniques to verify system-level security properties of a collection of interacting machines. The paper examined how local access control policies can be shown to satisfy global access control constraints. Also part of the team were Peter Loscocco, NSA, and George Coker, NSA.
Bounded Integer Linear Constraint Solving via Lattice Search. SMT Workshop 2015
Dr. Benjamin Jones and Dr. Joe Hendrix published a paper presenting a novel algorithm for solving integer linear constraint problems of the form l ≤ Ax ≤ u. The algorithm, and the ensuing solver, was motivated by efforts to apply SMT solvers to signal processing algorithms. In particular, the paper describes the problem of reversing JPEG, that is, finding compressed data that decompress into an image satisfying given constraints. From the abstract: “This problem can be expressed as a bounded integer linear constraint problem, but was intractable to the SMT solvers we tried. In contrast, BLT is able to solve many of the examples in seconds, including both SAT and UNSAT problems.”
Formal methods at Galois. Workshop on Formal methods for Robotics: benchmarks and evaluation metrics
Dr. Peter Trautman gave an invited talk at the Workshop on Formal Methods for Robotics on formal methods work at Galois. Dr. Trautman talked about current results, ongoing work, and future challenges, and touched on Galois’s work on DARPA’s HACMS program.
Ten years of Layered Assurance at Galois, lessons learned and looking forward
Dr. Dylan McNamee gave an invited talk at the Layered Assurance Workshop of the 2015 Annual Computer Security Applications Conference, describing Galois’s work in the areas of using composable architectures to build high assurance cross domain systems, cyber-physical systems, and cryptographic systems.
Cyber-physical systems and robotics
Guilt-free Ivory. Haskell Symposium, 2015
A team of Galwegians published a paper detailing Ivory, a programming language for writing secure, high-assurance software for embedded systems such as those found in automobiles, UAVs, etc. Software written in Ivory is guaranteed to be memory safe and is provably invulnerable to large classes of attack. The paper provides a detailed overview of the Ivory language, semantics, implementation in the GHC type system, and the built-in tools for testing and verification. Ivory was designed and implemented as part of DARPA’s High Assurance Cyber Military Systems (HACMS) program and was used to write a secure UAV autopilot. The Galois team was comprised of Trevor Elliott, Lee Pike, Simon Winwood, Pat Hickey, James Bielman, and Jamey Sharp. Also part of the team were Eric Seidel, UC San Diego, and John Launchbury, Willamette University.
Securing the Automobile: a Comprehensive Approach. Embedded Security in Cars (ESCAR)
A team of Galwegians published a paper on securing the automobile, which was presented at the Embedded Security in Cars (ESCAR) Conference in May. The paper walks through a comprehensive approach to secure the modern automobile, taking into account static assurance, dynamic assurance, software, and networks, while considering the constraints of the automotive industry. The team comprised of Galois’s Lee Pike, Jamey Sharp, Mark Tullsen, Pat Hickey, and James Bielman.
Programming Languages for High-Assurance Autonomous Vehicles, VSTTE 2015.
Dr. Lee Pike gave the keynote talk on July 19 at the Conference of Verified Software: Theories, Tools, and Experiments. He described the use of embedded domain-specific languages to improve programmer productivity and increase software assurance in the context of building a fully featured autopilot for unpiloted aircraft.
Assuring the Guardians. Runtime Verification, 2015
Dr. Lee Pike, Galois’s Cyber-Physical Systems Research Lead, was part of a team that published a paper describing a framework for verifying runtime monitoring systems that check ultra-critical autonomous systems. Runtime verification involves monitors that detect and respond to stability issues and failures of critical systems at while they are running. The tools described in the paper are integrated in Copilot, a language developed by Galois and NASA to write runtime monitors for critical systems that detect software and system failures in critical systems. Also part of the team were Alwyn Goodloe, NASA Langley Research Center, and Jonathan Laurent, École Normale Supérieure.
Trustworthy Software in the Real World. Open Source Bridge 2015
Jamey Sharp presented SMACCMPilot, a high-assurance quadcopter autopilot developed as part of DARPA’s HACMS program, and the new tools and technologies that make it feasible to trust a large piece of software. In the talk, Jamey introduced tools for improving software quality that have been traditionally restricted to academia, and talked about how engineers can apply similar tools in real world-critical systems like vehicles, medical devices, banking systems, etc. Read the abstract here and watch the video here.
Assistive Planning in Complex, Dynamic Environments: a Probabilistic Approach. HRI 2015 Workshop on Human Robot Teaming
Dr. Peter Trautman presented a paper on shared control at Human Robot Interaction (HRI) 2015. From the abstract: “Shared control fuses human inputs and autonomy inputs into a single command. However, if the environment or the operator exhibits ambiguity (common to search and rescue robots, teleoperated robots facing communication degradation, assistive medical devices, and assistive driving technologies), many state of the art approaches (e.g., linear blending) are suboptimal with respect to safety, efficiency, and operator-autonomy agreement—see our recent paper at http://arxiv.org/pdf/1506.06784.pdf. To prove and rectify the above sub-optimalities, we introduced probabilistic shared control (PSC), which simultaneously optimizes autonomy objectives and operator-autonomy agreement under ambiguous conditions. Importantly, because PSC optimizes operator-autonomy agreement, it exhibits stronger ‘centaur’ like properties than the state of the art: PSC naturally leverages the complementary abilities of the human and the machine.”
Other shared control contributions in 2015 included a conference paper at Systems man and cybernetics, and talks at the Interactive Robotics group at MIT, Oregon State university robotics lab, and the Safe and Secure Systems Symposium (S5).
Elections technology
Elections technology and the benefits of open source software, San Francisco Elections Commission
Dr. Joseph Kiniry, Galois’s election systems expert, spoke before the Elections Commission of San Francisco on open source software and the benefits it will bring to elections technology. Dr. Kiniry also touched on the barriers that have kept open software from manifesting in the elections world until now. Find our responses to the questions posed by the Elections Commission on this topic here. Listen to the recording here.
The Future of Voting: End-to-End Verifiable Internet Voting – Specification and Feasibility Study, National Association of Secretaries of State
Galois’s election systems team, in collaboration with the U.S. Vote Foundation, a team of elections experts, and the Democracy Fund, published a comprehensive study on the feasibility of conducting secure elections online. Starting from the premise that public elections in the U.S. are a matter of national security, the report explores whether End-to-End Verifiable Internet Voting (E2E-VIV) systems are a viable and responsible alternative to traditional election systems. It contains the most complete set of requirements to date that must be satisfied by any Internet voting system used in public elections. The team included experts in election integrity, election administration, high-assurance engineering, and cryptography. The U.S. Vote Foundation, the Democracy Fund, and Galois presented the report at the National Association of Secretaries of State (NASS) Conference in Portland, Maine.
Promises of Technology to Increase the Transparency and Trustworthiness of Elections, Voting and Elections Summit
Dr. Joseph Kiniry gave a talk on the promises of technology to increase the transparency and trustworthiness of elections at the Voting and Elections Summit. Dr. Kiniry discussed the trade-offs that election officials face when considering currently available election technology systems. He also outlined some of the benefits that well-built elections systems offer to voters and officials, including efficient voting, verifiability, auditing, and accountability.
The Impact of Legislation on Election Systems: Design, Cost and Lifespan
Dr. Joseph Kiniry was a member of a panel on the impact of legislation on election systems at the National Conference of State Legislators (NCSL). Find Galois’s comments here.
Cybersecurity
7 Cyber security questions to expect to answer after OPM breach. Government Computer News
In the wake of the OPM breach, Dr. David Archer and a team of Galwegians presented a set of questions that officials in private companies and public institutions can ask to quickly assess the security stance of an organization. The piece included example answers that would give confidence that a sound security stance is an active priority. The article also lists key, practical steps an organization can follow as a first step toward a positive security stance.
Tor in Haskell & Other Unikernel Tricks. QCon 2015
Dr. Adam Wick, Galois’s Systems Software and Mobile Security Research Lead, gave a talk at QCon 2015 about implementing the Tor anonymity system using unikernels, which are single-purpose, lightweight virtual machines. The talk discussed the aspects of Tor that make it an attractive target for unikernels, what it took to build a Tor unikernel, and what actual challenges developers will face when implementing real-world systems.
An Introduction to Unikernels with the HaLVM. StrangeLoop 2015
Adam Wick, Trevor Elliott, and Adam Foltzer introduced unikernels in a workshop at StrangeLoop 2015. The attendees were introduced to Galois’s open-source Haskell Lightweight Virtual Machine (HaLVM) and were guided through using unikernels and building lightweight web services.
IoT security and passwords on Network Computing
Isaac Potoczny-Jones, CEO of Tozny and Galois’s Mobile Security and Identity Research Lead, published two educational articles around network computing, on the topics of IoT and password security. The articles explore IoT vulnerabilities and alternative approaches to building protection in IoT devices, as well as why passwords are inadequate security measures in today’s world:
Strategies for building cyber security into software development. Software Magazine
Isaac Potoczny-Jones wrote an article on what vendors can do to build cyber security into their products from the start. “Cyber security should not be an afterthought in the software development process; it should be the first thought. As applications, systems and devices increasingly fall victim to hacks, vendors may be tempted to assume that business users and consumers have become desensitized to the problem. That adding two-factor authorization or offering three months of credit monitoring service will somehow wipe the slate clean with no damage done to brand perception, customer growth, and revenues. This is not the case. Building cyber security into the front end of the software development process is critical to ensuring software works only as intended.”
Network defense, secure computation, and email security on “The State of Security”
Dr. David Archer, Galois’s Cryptography Research Lead, published three educational blog posts for Tripwire’s “The State of Security” blog. The posts introduced innovative ways to defend networks against malicious attackers, new methods to keep data encrypted and secure while in use, and what can be done to avoid spam and phishing attempts through email.
- Asymmetric Network Defense: It’s 1904 All Over Again
- Secure Computation and The Right to Privacy
- Killing Phish the Sumerian Way
Acoustic Kitty and Zombie Home Appliances: Yesterday’s Theories Shape Tomorrow’s Technologies. Signal Magazine
Dr. David Archer wrote an article for AFCEA’s Signal magazine on the potential damage from compromised IoT devices on the battlefield, and what can be done to protect the cybersecurity of the troops of tomorrow from determined adversaries.
The unrealized potential of interagency total information sharing. Government Computer News
Dr. David Archer wrote an article for Government Computer News on interagency total information sharing, why it can be ineffective and the path forward for total information sharing systems that benefit national security without sacrificing privacy.
Other announcements and launches
Galois announced a $6.3M DARPA contract to research private data as a service
Galois announced a $6.3M award for our Jana project as part of DARPA’s Brandeis program, which aims to develop tools and techniques for building systems in which private data may be used only for its intended purpose and no other. The awarded project, a collaboration between Galois, the University of Bristol, Rutgers University and George Mason University, aims to provide a practical implementation of private data as a service (PDaaS), which would allow data to be protected against misuse while retaining its utility to analysts.
Galois announced DARPA sub-contract to strengthen supply-chain protection of electronic components
Galois announced a sub-contract by SRI International under a DARPA’s SHIELD program to protect against counterfeit electronic components and associated security concerns by introducing low-cost secure authentication components in the hardware supply chain. Building upon our 15-year history developing defensive cybersecurity technologies, Galois’s effort will focus on cryptography, secure network protocols, and authentication.
Tozny and Galois announced $1.86M NIST award to secure IoT-enabled smart homes
Tozny and Galois were awarded a $1.86 million NIST National Strategy for Trusted Identities in Cyberspace (NSTIC) grant to build a secure data storage system that enables next-generation IoT capabilities without sacrificing privacy. Galois’ authentication and mobile security subsidiary, Tozny, will serve as the technical lead for the NSTIC pilot program.
Galois was awarded $1.7M DHS contract create DDoS defense technologies.
DHS announced a $1.7M award for Galois to create technology to defend against large and sophisticated Distributed Denial of Service (DDoS) attacks. The project, called “DDoS Defense for a Community of Peers,” uses a unique collaborative model wherein multiple organizations work together to detect DDoS attacks, compute mitigations, and convince service providers to take action. For more information, visit the project page.
Galois launched the Software Analysis Workbench, a toolset to formally verify code properties
Earlier this year we launched the Software Analysis Workbench (SAW) provides the ability to formally verify properties of code written in C, Java, and Cryptol. It leverages automated SAT and SMT solvers to make this process as automated as possible, and provides a scripting language, called SAW Script, to enable verification to scale up to more complex systems.
Galois launched Fuse Analyzer to help with Android permissions’ migration and app security
Fuse Analyzer, a tool that resulted from a DARPA-funded SBIR, launched earlier this year. The tool provides Android developers two capabilities:
- Prepare for Android 6 migration by discovering and fixing unhandled permission requests
- Analyze Android apps for security issues, data leaks, and weak encryption
Galois’s secure UAV tools were featured on 60 Minutes
Galois helped demonstrate security vulnerabilities in modern automobiles and small UAVs as part of a “60 Minutes” profile of DARPA. We also demonstrated our secure UAV autopilot technology as an alternative to the currently available software systems that are prone to remote takeovers and other security vulnerabilities.
Galois launched haskell-tor, a Tor client written purely in Haskell
Haskell-tor is the beginning of a full-featured Tor replacement written in a high-level language. Through integration with the HaLVM, haskell-tor offers an opportunity to for large numbers of lightweight Tor nodes, each of which is free from common classes of errors, with critical properties preserved by the type system.
Entrepreneurship and angel investing
Entrepreneurial Expertise and the Use of Control, Journal of Business Venturing Insights 2015
Dr. Rob Wiltbank, Galois CEO, was part of a team that published a paper on the effect that entrepreneurial expertise has on control and prediction strategies to to situations which vary in environmental predictability and controllability. Results show that entrepreneurial expertise yields significant decision-making improvements in the situational use of control strategies – those strategies conceptually associated with uncertain new ventures, products, and markets. The team also included Nicholas Dew, Stuart Read, and S.D. Sarasvathy.
Investment and Returns in Successful Entrepreneurial Sell-outs, Journal of Business Venturing Insights
Dr. Rob Wiltbank was part of a team that published a paper examining returns to capital invested in new ventures. The research looked at 3000+ private firms that were acquired by U.S. publicly traded firms and revealed that, while new venture growth is positively related to invested capital, terminal value of the venture and entrepreneur returns see steeply diminishing returns to invested capital. The results indicate that the primary benefit of equity investment is accelerated liquidity, not terminal value of the venture or entrepreneurs returns. Dr. Wiltbank was part of a team that also included Nicholas Dew and Stuart Read.
The Role of Personality in Angel Investing. International Journal of Entre. & Innovation 2015
Dr. Rob Wiltbank was part of a team that published a paper examining the relationship between an entrepreneur’s personality and angel investor evaluations of the management team of venture opportunities. The research also analyzes the influence of an entrepreneur’s start-up experience and the angel investor’s investing experience on the evaluation of the management team. Results suggest that investor ratings of management teams are influenced by the personality traits of the lead entrepreneur. Dr. Wiltbank was part of a team that also included Charles Y. Murnieks, and Richard Sudek
Media coverage highlights
Covering Galois projects:
Engadget: The Pentagon wants unhackable drone helicopters by 2018
GCN: Galois wins DARPA funding for private data as a service
GCN: Making mobile phones the authentication hubs for smart homes
ZDNet: NSTIC commits $3.7 million to new round of identity pilot programs
Quoting experts from Galois:
Isaac Potoczny-Jones on C4ISR & Networks: DoD embraced public key infrastructure to secure tactical networks
Isaac Potoczny-Jones on KGW: The Internet of Things: How safe is ‘smart’ technology?
Joseph Kiniry on Washington Post: Can you vote for the next president on your smartphone? Not just yet.
Joseph Kiniry on Computerworld: Internet voting isn’t ready yet, but it can be made more secure
Lee Pike on Nextgov: Pentagon on Path to Launch Hacker-Proof Boeing Drone by 2018 – Nextgov.com
Robert Wiltbank on Forbes: How To Tell If An Entrepreneur Will Be Effective? What Angels Need To Know – Forbes
Robert Wiltbank on Geekwire: More cash for startups: Median angel investment round size increases in Q3