Categories

2018: Year in Review

2018 was a year of growth and impact at Galois. We furthered our work from cryptography to software and hardware assurance through both our R&D efforts and our spin-out companies. Our team grew significantly, and like most everyone in this industry, we continue to hire. We’ve been fortunate to work with many great partners and clients, many of them new this year, while publishing 35 papers and articles, and sharing 20 public talks.

Overview

2018 was an eventful year for our work on secure computation, the process of working with data without exposing it. Secure computation holds the promise of true data privacy without losing the utility of data analysis. Multiple government agencies and commercial entities engaged with us in 2018, not only to further research in secure computation, but also to deploy variants of it in real-world scenarios.

In software correctness, our experience in streamlining formal verification and assurance for real-world, impactful commercial software took center stage in our publications and talks. Together with the Amazon Web Services (AWS) team, we published a paper on our work to formally verify AWS’s s2n encryption library. We also spoke, published, and held many talks and workshops related to industrial formal methods and functional programming.

In 2018 we announced the BESSPIN project funded by DARPA’s SSITH program. The project aims to develop tools and methodologies that enable provable hardware security. In our talks and publications, we focused on sharing what we have learned and developed in BESSPIN and other projects in the space of hardware safety and verification. We directed our efforts in formal assurance for the RISC-V architecture and have held many talks and publications related to high-assurance hardware.

More generally in cybersecurity, we published papers related to our ADAPT project, part of DARPA’s Transparent Computing program. In ADAPT, we worked on anomaly detection to uncover unknown cyberattacks. We also wrote a number of articles and papers on our results from RADSS, our software diversity project within DARPA’s CFAR program. In RADSS, we try to mitigate memory corruption attacks against legacy C/C++ systems, without requiring finding and fixing each individual bug, by generating and running multiple variants of a program in parallel in a way that reveals attacks.

Additionally, in 2018 we launched our fourth spin-off company, Tangram Flex (Tangram), that provides software development tools for cyber assurance and resilience in embedded systems. Tangram is building on years of work developing cyber-physical systems safety, security, and reconfigurability to provide a product suite for complex embedded systems (planes, ships, automobiles, trains, drones, satellites, etc.). In December, Tangram announced a $4.5M investment from Hale Capital Partners and is growing accordingly.

Tozny, a Galois spin-out focused on data privacy and mobile security, also saw significant growth. In October, Tozny announced a number of commercial and government deployments of their InnoVault platform, a toolkit that enables developers to embed end-to-end data security encryption capabilities into their websites, apps, and other software.

Organizationally, we’re continually attending to how we work together as a team. This year we published https://lifeatgalois.com, a website where we detail the workings of our unconventional organizational structure. We consider the way we organize ourselves to be a staple of our well-being as people, in addition to facilitating our research and our business’s progress. Most articles are accompanied by videos that discuss specific topics; for example, here is one that talks about how we organize ourselves without a fixed hierarchy, and why it is essential to how we work together: A company without managers. We hope it gives a glimpse of what we’re about as a company.

Below you’ll find links to the papers, talks, and other public contributions we shared in 2018. We hope you find something interesting.

From all of us at Galois, we wish you a peaceful and productive 2019.

High Assurance Cryptography

Callisto: A Cryptographic Approach To Detect Serial Predators Of Sexual Misconduct, Best note at ACM COMPASS

Dr. David Archer was part of a team that published a paper about using secure computation to detect serial sexual misconduct. Also part of the team: Anjana Rajan Lucy Qin Dan Boneh Tancrède Lepoint Mayank Vari.

Architectural Security, the Ardennes, and Alfred the Great, U.S. Cybersecurity Magazine

Dr. David Archer published an article about the application of secure computation for the Callisto project above and the lessons that can be learned to make “hardened applications that treat information security as a first-class requirement — part of a checkerboard defense appropriate for the limited aims adversary model, and cryptographically hard to defeat,” outlining a design paradigm that stewards sensitive information. Dr. Archer also wrote a post on the ShareMind blog on a similar topic, which you find here: The Search for Killer Apps in Secure Computation.

From Keys to Databases – Real-World Applications of Secure Multi-Party Computation, The Computer Journal

Dr. David Archer was part of a team that published a paper discussing “the widely increasing range of applications of a cryptographic technique called multi-party computation. For many decades, this was perceived to be of purely theoretical interest, but now it has started to find application in a number of use cases.” IACR eprint.

Privacy-preserving, Evidence-based Decisions in Public Policy. Bipartisan Policy Center

Dr. David Archer spoke at the Bipartisan Policy Center on how organizations in the government can jointly use multi-party computation to make decisions based on their respective datasets, while protecting the privacy of that data.

Keep it Secret, Keep It Safe – Cryptographic Tools for EMR Security, UA Health Sciences

Dr. David Archer gave a talk at the UA Health Sciences Medicine Grand Rounds on information security as it relates to electronic medical records.

Your Secrets are Safe with Julia: A Compiler for Secure Computation, StrangeLoop

Jason Dagit gave a talk at StrangeLoop on a compiler that translates a subset of the Julia programming language into a form suitable for computation under homomorphic encryption, which provides the ability to compute functions over encrypted data without the need to decrypt.

The Zimmerman Telegram, Enigma, and Inter-Agency Data Sharing, U.S. Cybersecurity Magazine

Dr. David Archer published an article on practical, cost-effective inter-agency sharing of sensitive data. From the article: “Inter-agency sharing of sensitive data needs to move from the realm of ‘it would be nice, but I’m sorry…we just can’t’ to ‘we have a wealth of administrative data among us…what public good can we do?’ Technologies – some limited, others very promising – exist to get the job done.”

Software Correctness and Formal Verification

High-Assurance Blockchains: Applications and Verification, HCSS 2018

Dr. Joe Hendrix gave a talk at the High Confidence Software and Systems (HCSS) conference about providing and maintaining data integrity guarantees via blockchains even when systems are compromised, and verifying a blockchain implementation satisfies security and functionality requirements.

Continuous formal verification of Amazon s2n, CAV

The Galois team, working with Amazon Web Services on formal assurance for the s2n encryption library, published a paper at Computer Aided Verification (CAV) about our efforts so far. Authors: Andrey Chudnov, Nathan Collins, Byron Cook, Josiah Dodds, Brian Huffman, Colm MacCarthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb and Edwin Westbrook.

Continuously Verified Cryptography, PNW PLSE

Dr. Mike Dodds gave a talk on our work with Amazon Web Services to formally verify portions of the s2n encryption library at the Workshop on Programming Languages and Software Engineering.

Continuous verification in industry, FMATS

Dr. Mike Dodds gave a talk at Sixth Workshop on Formal Methods and Tools for Security on automating formal verification for use in industry.

Continuous Verification of Critical Software, IEEE SecDev

Dr. Mike Dodds, Dr. Stephen Magill, and Dr. Aaron Tomb held a tutorial at IEEE SecDev on continuous verification of critical software. You can find the paper on the sessions here.

Comprehensive Language and Protocol Verification at Galois. LangSec Workshop

Dr. Joey Dodds presented our team’s approach to language verification, considering both parsers and protocol languages. You can find the description of the talk and the slides here.

Proving the Correctness of Amazon’s s2n TLS Library, ICMC

Dr. Aaron Tomb held a talk on our approach to constructing proofs of the functional correctness of several components of s2n, and the tools and techniques we have leveraged. Find the slides here.

A Data-Driven CHC Solver, Distinguished Paper Award at PLDI

Dr. He Zhu, Dr. Stephen Magill, and Dr. Suresh Jagannathan (Purdue University) published a paper at PLDI on “data-driven technique to solve Constrained Horn Clauses (CHCs) that encode verification conditions of programs containing unconstrained loops and recursions.” You can watch the video of the presentation here: https://www.youtube.com/watch?v=MIVboi74v1w

Mechanizing the Construction and Rewriting of Proper Functions in Coq, CoqPL

Dr. Edwin Westbrook published and presented a paper at the on mechanising the construction and rewriting of proper functions in Coq at the Coq for Programming Languages Workshop.

Getting Satisfaction out of Games: Learning to use SAT solvers through puzzles and games, ICFP

Eric Mertens and Dr. José Manuel Calderón Trilla held a tutorial at the International Conference on Functional Programming (ICFP) on how to identify SAT problems and how to encode them using the Ersatz Monad by using puzzles and games as concrete examples.

A Surprisingly Competitive Conditional Operator: miniKanrenizing the Inference Rules of Pie, Scheme 2018

Dr. David Thrane Christiansen was part of a team that presented a paper on a new search operator in miniKanren that allows developers to use domain-specific knowledge to prioritize likely paths to solutions at the Workshop on Scheme and Functional Programming. The main contributors and the rest of the team: Benjamin Boskin, Weixi Ma, and Daniel Friedman. You can watch a video of the presentation here.

Extensible Type-Directed Editing, ICFP

Dr. David Thrane Christiansen and Joomy Korkut published a paper at the International Workshop on Type-Driven Development (TyDe) at ICFP on extending Idris’s metaprogramming facilities with primitives for describing new type-directed editing features.

A Little Taste of Dependent Types, Strange Loop

Dr. David Thrane Christiansen held a talk at Strange Loop that gave an introduction to dependent types and demonstrated a proof hat is also a program. Dr. Christiansen also held a talk on the same topic at FlatMap Oslo.

The Little Typer, book

Dr. David Thrane Christiansen, together with Daniel P. Friedman (Indiana University) published The Little Typer, a introductory book about dependent types that begins with a very small language that looks like Scheme and extends it to cover both programming with dependent types and using dependent types for mathematical reasoning.

Reflections on industrial use of Frama-C, Sound Static Analysis Workshop

Dr. Dan Zimmerman and Dr. Joe Kiniry gave a talk on the use of Frama-C across multiple projects at Galois focused on mission-critical systems at the Sound Static Analysis Workshop.

Haskell Mini-Course, IFL 2018

Dr. David Thrane Christiansen and Dr. José Manuel Calderón Trilla held a Haskell mini-course at the symposium on Implementation and Application of Functional Languages.

Integration of Quantifier Eliminator with Model Checker and Compositional Reasoner. IEEE ICCA

Matt Clark was part of a team that published a paper on integration of quantifier elimination (QE) technique with model checking and compositional verification at IEEE International Conference on Control and Automation. Also part of the team: Hao Ren and Ratnesh Kumar.

The Software Analysis Workbench, Dagstuhl Seminar on Program Equivalence

Dr. Aaron Tomb held a talk at the Dagstuhl Seminar on Program Equivalence on Galois’s Software Analysis Workbench (SAW) and its inner workings.

What is Formal Verification? (video)

We published a video giving a light introduction to mathematically verifying the correctness of software systems.

Cryptography and Formal Methods (video)

We published a video on cryptography and what makes it so difficult to get right, and what can we do to avoid flaws and vulnerabilities.

Hardware and Cyber-physical Systems

Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System, CAV

Dr. Mark Tullsen presented our work on verifying a V2V Messaging system at Computer Aided Verification. Authors: Mark Tullsen, Lee Pike, Nathan Collins and Aaron Tomb.

Formal Assurance for RISC-V Implementations, RISC-V Workshop

Dr. Dan Zimmerman presented our work on and approach to verifying the correctness and security of RISC-V implementations. Find the video in the link above and the slides here.

Formal Methods Need Not Be Black Magic, RISC-V Summit

Dr. Joe Kiniry and Dr. Dan Zimmerman held a talk at the RISC-V Summit that gave an introduction to formal methods as they relate to hardware development and RISC-V specifications. Find the video in the link above, and the slides of the talk here.

SSITH and BESSPIN, ERI Summit

Dr. Joe Kiniry and Dr. Linton Salmon (DARPA) introduced DARPA’s SSITH program and Galois’s BESSPIN project as part of SSITH at the Electronics Resurgence Initiative Summit.

A Formally Verified Cryptographic Extension to a RISC-V Processor, CARRV

Dr. Joe Kiniry, Dr. Dan Zimmerman, and Dr. Robert Dockins were part of a team that published a paper detailing the creation of a formally verified cryptographic extension to a RISC-V Processor at the Workshop on Computer Architecture Research with RISC-V (CARRV 2018). Also part of the team: Rishiyur Nikhil (Bluespec, Inc.).

Achieving memory safety without compromise, Embedded.com

Adam Foltzer published an article on Embeded.com about memory-safe programming languages and the tradeoffs involved in using them.

Construction of Stability-Based Hybrid Automata for Safety Verification Using Continuation Methods, 2018 AIAA Guidance, Navigation, and Control Conference

Matt Clark was part of a team that published a paper on the use of continuation methods to automatically transform a non-linear dynamical system into a series of simplified hybrid modes relative to particular bifurcation points. The method, as a proof of concept, enables the linearization and control of highly dynamical nonlinear systems. Also part of the team: Peter Uth, and Anshu Narang-Siddarth.

Loihi: A Neuromorphic Manycore Processor with On-Chip Learning, IEEE Micro

Dr. Georgios Dimou was part of a team that published a paper on Loihi, a 60-mm2 chip fabricated in Intel’s 14-nm process that advances the state-of-the-art modeling of spiking neural networks in silicon. See link above for the rest of the team.

Secure pprzlink: encrypted communications for open source drones

Michal Podhradsky wrote an article on Secure pprzlink, an encrypted communication protocol for UAVs that Galois was involved in developing. Secure Pprzlink is backed by a formally verified cryptographic library.

Cybersecurity

Enforcing Unique Code Target Property for Control-Flow Integrity, CCS 2018.

Dr. Bill Harris was part of a team that published a paper on a new approach for accurately and efficiently monitoring programs to ensure that they satisfy control-flow integrity, a fundamental security property. Also part of the team: Hong Hu, Chenxiong Qian , Carter Yagemann, Simon Pak Ho Chung, Taesoo Kim, and Wenke Lee.

Trustworthy Elections, DEFCON Voting Village

Dr. Joe Kiniry held a talk on trustworthy elections and voting technology at the DEFCON Voting Village. The talk focused on the deficiencies of the elections ecosystem today and what can be done to fix it.

Adding Noise to the Signal: Using Deceptive Traffic Generation to Defend and Distract, Cyber Shorelines

Dr. Adam Wick held a talk on using cyber deception to detect and prevent advanced attacks in networks.

Protecting Applications with Automated Software Diversity

Dr. Ben Davis wrote two posts detailing our work on the Robust, Assured Diversity for Software Systems (RADSS) project as part of DARPA’s CFAR program. Find the first post in the link above, and the second post here: Automated Software Diversity: Sometimes More Isn’t Merrier.

Composition Challenges for Automated Software Diversity, Tech Report

Dr. Ben Davis, Dr. Simon Winwood, and Dr. Stephen Magill were part of a team that published a tech report on the issues that must be considered when composing software diversity transformations and is part of Galois’s RADSS project. The tech report was originally presented at the Layered Assurance Workshop (LAW), 2016. Also part of the team: Per Larsen, Stijn Volckadert, David Melski, Michael Franz.

Blockchain: Hype or Hope for Transactional Security? Security Boulevard

Dr. David Archer published an article about blockchain technology, its types and uses, and the tradeoffs and security in relation to more traditional solutions.

Assuming you know: epistemic semantics of relational annotations for expressive flow policies, 2018 IEEE Computer Security Foundations Symposium.

Dr. Andrey Chudnov was part of a team that published a paper on “unified framework for expressing, giving meaning and enforcing information downgrading policies that builds on commonly known and widely deployed concepts and techniques, especially static and dynamic assertion checking.” Also part of the team: David A. Naumann.

What’s the Over/Under? Probabilistic Bounds on Information Leakage, POST 2018

Dr. José Manuel Calderón Trilla and Dr. Stephen Magill were part of a team that published a paper about using novel techniques for improving the bounds on computing quantitative information flow at Principles of Security and Trust Conference. Also part of the team: Ian Sweet, Chad Scherrer, and Michael Hicks.

Data Analysis and Machine Learning

Quine: A Temporal Graph System for Provenance Storage and Analysis, IPAW 2018

Ryan Wright published a paper and delivered a demonstration at the International Provenance and Annotation Workshop that introduced Quine, a prototype graph database and processing system designed for provenance analysis with capabilities that include fine-grained graph versioning to support querying historical data after it has changed, standing queries to execute callbacks as data matching arbitrary queries is streamed in, and queries through time to express arbitrary causal ordering on past data.

Detecting Cyberattack Entities from Audit Data via Multi-View Anomaly Detection with Feedback, AICS 2018

Dr. David Archer, Ryan Wright, and Alec Theriault published a paper on detecting unknown cyberattacks from audit data of system-level events at the Artificial Intelligence for Cyber Security (AICS). The work is the result of the ADAPT project funded by DARPA’s Transparent Computing program.

Feedback-Guided Anomaly Discovery via Online Optimization, KDD

Ryan Wright, Alec Theriault, and Dr. David Archer were part of a team that published a paper at the Conference on Knowledge Discovery and Data Mining introducing a new method for online training of anomaly detectors to tailor the results to what an analyst considers to be anomalous. This work (video) advances the state of the art in human-machine teaming for improved results over existing machine learning techniques alone, and was a result of the ADAPT project funded by DARPA’s Transparent Computing program.

Rendering and Extracting Extremal Features in 3D Fields, Best Paper award at EuroVis 2018

Dr. Charisee Chiw was part of a team that received the best paper award on their paper about the Diderot language at EuroVis 2018. Diderot is a DSL designed for scientific visualization and image analysis. The paper demonstrated the language’s ability to do feature extraction and volume rendering on 3D fields.

Code + ML – Will Automation Take Our Jobs? DevOps Summit

Dr. Stephen Magill gave a lighting talk about the state of the art in combining programming and machine learning at DevOps Summit.

Using Formal Methods to Reason About Neural Network Based Autonomous Systems, HCSS

Dr. Stephen Magill presented on using formal methods to reason about machine learning at the High Confidence Software and Systems (HCSS) conference.

Other

Life at Galois: We detailed the workings of our unconventional organizational structure through a series of articles. We discussed the following:

Tangram Flex: We spun out our fourth company, Tangram Flex (Tangram), that provides software development tools for cyber assurance and resilience in embedded systems. Tangram is taking years of work in safety, security, and reconfigurability of cyber-physical systems software and providing it as a product suite for complex embedded systems (planes, ships, automobiles, trains, drones, satellites, etc.). Tangram announced Ricky Peters as CEO.

Tangram Flex funding: In December, Tangram announced a $4.5M investment from Hale Capital Partners.

Tech talks: Galois organized and hosted 10 public tech talks on a variety of topics.

c2rust: We open sourced c2rust, a tool that translates C into semantically equivalent Rust code. Eric Mertens wrote a blog post with more details.

Cryptol 2.6.0: We released a new version of Cryptol with support for unbounded integers, modular integers, and parameterized modules.

Allegheny County: The Bipartisan Policy Center partnered with Allegheny County and Galois on a new privacy-preserving data project.

Tozny InnoVault: Charles River Analytics announced they are building a smartphone app that detects illnesses and injuries and that leveraging Tozny’s InnoVault product to protect the privacy of user data with end-to-end encryption.

Facebook C++ verification: Galois was awarded a grant from Facebook to build a verification toolchain for C++ cryptographic libraries.

Cryptographic Analysis, Verification, Exploration, and Synthesis (CAVES): Navy Awards Galois $2 Million Contract For Cryptographic Security.

Balancing Evaluation of System Security Properties with Industrial Needs (BESSPIN): Galois Awarded $4.5 Million DARPA Contract To Strengthen Hardware Security.

Framework for Information Disclosure with Ethical Security (FIDES): DHS Awarded Galois $800K Contract To Enable Sensitive Network Data To Remain Encrypted When Shared And Analyzed.

RISC-V Security Standing Committee: The RISC-V Foundation announced the Security Standing Committee with strong Galois involvement.

Press Highlights

Using Functions for Easier Programming: Dr. Iavor Diatchki gave an interview for CACM on using functions for easier programming.

Thoughts on Secure Development: Dr. Mike Dodds gave an interview on formal verification and secure development on the Thoughts on Secure Development blog.

Open-Source RISC-V Hardware and Security: Dr. Joe Kiniry was interviewed as part of a panel of experts on Open-Source RISC-V Hardware and Security in Semiconductor Engineering.

Building tools to secure computer processors: Dr. Joe Kiniry gave an interview as part of a Government Computer News (GCN) article that detailed our aims with the BESSPIN project on hardware security.

Navy Beefing Up At-Sea Enterprise Network: Dr. Aaron Tomb was interviewed as part of a National Defense Magazine article about Navy enterprise networks that in part detailed our work in the CAVES project.

How privacy is moving data security to the top of corporate agendas: Dr. David Archer spoke with CSO magazine about security as part of an article on corporate privacy and data issues.

Committees, reviewers, guest editing, panels

  • Dr. David Archer
    • Was part of the organizing team for the Provenance-based security workshop
    • Participated in Zero Knowledge Proof Standardization workshop
    • Served on the UN Statistics Division Privacy Preserving Technology Team
  • Dr. David Archer and Dr. Alex J. Malozemoff participated in the FHE standardization workshop
  • Dr. Charisee Chiw
  • Dr. David Thrane Christiansen
    • Served as Workshops chair for ICFP
    • Served on the ICFP Program Committee
    • Served on the ICFP Distinguished Papers Committee
  • Dr. Alex J. Malozemoff
    • Program Committee member at
      • Crypto
      • Workshop on Encrypted Computing and Applied Homomorphic Cryptography
    • External Reviewer at
      • Asiacrypt
      • Privacy Preserving Machine Learning Workshop
      • Computer and Communications Security Conference
  • Dr. John Launchbury participated in the IFIP Working Group 2.8 on Functional Programming
  • Dr. Scott Moore participated in DARPA’s ISAT workshop “An Analytic Framework for Cyber Automation”
  • Dr. Bill Harris
    • Served as a Program Committee member at the Symposium on Fundamentals of Computation Theory (FCT)
    • Served as External Reviewer for IEEE S&P (“Oakland”)
  • Dr. Georgios Dimou served on the best paper award committee at IEEE ASYNC 2018 Symposium.
  • Dr. Joe Kiniry and Dr. Dan Zimmerman participated in Open Source Trusted Enclaves Workshop
  • Dr. Joe Kiniry
  • Dr. Dan Zimmerman served on the RISC-V Cryptographic Hardware Extension Technical Group as vice-chair
  • Dr. Aaron Tomb served as member of the Pnwplse.org Committee