2020 was certainly an interesting year. Amidst a global pandemic and major societal issues, keeping software and hardware systems trustworthy continued to be challenging. From election systems to ransomware to privacy breaches and online banking theft, the challenges of trustworthy software are alive and well. In this arena, Galois and our partners advanced the state of art for high assurance cryptography, software correctness, formal methods, machine learning, data science, cybersecurity, hardware, and cyber-physical systems.
Even while transitioning to a 100% remote working environment for the first time in our 21 year history, we continued to share ideas through exciting new formats – including a new podcast, blog posts, articles in respected publications, and more. Thank you so much to our partners and customers, and teammates who helped this work advance. Below you can dig into some fun detail. Here’s to a prosperous 2021!
This is The Way
Galois led the team that created and helped run DARPA’s first-ever bug bounty program, the DARPA Finding Exploits to Thwart Tampering (FETT). Lead by Dr. Joseph Kiniry, Dr. Daniel Zimmerman, and Reuben Broadfoot.
How D-Day Relates to Zero-Knowledge Proofs
The United States CyberSecurity Magazine editors invited Dr. David Archer to write an article about zero-knowledge proofs and their applications, specifically focusing on proofs of software security. Zero-Knowledge Proofs, D-Day, and the Promise of Trustable Software appeared in the magazine’s January 2021 issue.
Best Practices in Reliability
Galois launched a brand new podcast, Building Better Systems, about tools and techniques that make programmers, and their programs, more correct and secure. Dr. Joey Dodds and Shpat Morina host the podcast.
A Series of Fortunate Blog Posts
We launched the blst blog series by Dr. Joey Dodds, which describes the blst verification Galois is undertaking with Supranational, Ethereum Labs, and Protocol Labs. We regularly contributed to the Galois blog in 2020, giving further context to the work we’re doing with our partners at DARPA and beyond. We also blogged on topics related to our continuing work. For example, Dr. Mike Dodds wrote that Proofs Should Repair Themselves, about the continuing state-of-the-art formal verification of software proofs.
New Grounds For Conversation
We continued to work on our internal company culture. COVID 19 and the resulting stay at home orders made it difficult for co-workers to discuss their shared interests. Galois created an aid for its internal culture with Coffeebot, a program that randomly pairs up willing participants for a weekly “coffee chat.” Anyone who would like to participate can sign up on a spreadsheet by adding their name, email address, and a list of topics they enjoy discussing. Galois made the program open source so other companies could give it a try.
Below, see links for our papers, talks, software releases, and public presentations we made in 2020.
High Assurance Cryptography
Dr. David Archer was invited to speak at 2020 Improving Privacy with Advanced Cryptographic Techniques (IMPACT) conference on the topic, “De-confliction in Large Coalitions: When you Gotta Know Where Not to Go.” The talk covered an increasing trend of diverse coalitions needing to avoid conflicting use of shared resources. Dr. Archer described recent privacy-preserving de-confliction prototypes that show how to resolve this conundrum efficiently and securely.
Dr. David Archer was a guest on the new Cryptography.fm podcast. The topic was Zero knowledge proofs and their applications for software vulnerabilities and safety.
Dr. Adam Wick, Dr. Eric Davis, and Erin Chapman co-authored a paper, Invasion of the Botnet Snatchers: A Case Study in Applied Malware Cyberdeception, that they presented at Hawaii International Conference on System Sciences (HICSS). Their presentation concerned the initial steps towards a botnet deception mechanism, called 2face. As context for the work, the team showed how 2face could be used to help reverse engineer and then generate deceptive traffic for the Mirai protocol. They also discussed how this work could be extended to address future threats. Also part of the team: Jared Chandler and Kathleen Fisher of TuftsUniversity.
Dr. David Darais co-authored a paper, DuetSGX: Differential Privacy with Secure Hardware, for Theory and Practice of Differential Privacy (TPDP 2020). The paper concerned publicly queryable databases over sensitive data, using differential privacy type systems (via Duet) and secure hardware (via SGX). Also part of the team: Phillip Nguyen (University of Vermont), Alex Silence (University of Vermont), and Joseph Near (University of Vermont).
Software Correctness and Formal Methods
Dr. Jennifer Paykin, Dr. Daniel Zimmerman, and Dr. Brian Huffman co-authored a paper,
Formal Verification of Flow Equivalence in Desynchronized Designs, for ASYNC Symposium. They presented a counterexample to a long-accepted proof related to flow equivalence, a notion of equivalence between synchronous circuit specifications and their desynchronized bundled-data asynchronous equivalents. The paper also demonstrated how to formalize flow equivalence in Coq and provide mechanized, machine-checkable proofs of our results. Also part of the team: Peter A. Beerel (Galois/USC).
Dr. Joseph Kiniry was a panelist at “Dead or Alive? The Fate of Formal Methods in Securing ‘Everyday’ SoCs” at the Design Automation Conference (DAC). The panel discussed using formal methods to reason about the security of hardware designs.
Dr. Aaron Tomb, Dr. Stuart Pernsteiner, and Dr. Mike Dodds gave a tutorial, Symbolic Testing for C and Rust, describing how to use Crux to improve assurance of C and Rust code at the Institute of Electrical and Electronics Engineers (IEEE).
Dr. Giuliano Losa co-organized The 7th Workshop on Formal Reasoning in Distributed Algorithms (FRIDA 2020) with Marijana Lazić.
Dr. Charisee Chiw was invited to speak about Tensor computations, applications, and optimization at the Dagstuhl Seminar.
Dr. Mike Dodds and Dr. Joey Dodds spoke at the High Confidence Software and Systems (HCSS) conference. Dr. Mike Dodds discussed Formal Verification of Production Distributed Protocols, real-world distributed protocols focusing on the Stellar Consensus Protocol. Dr. Joey Dodds gave a talk on Verification is Engineering, a discussion of the Galois engineering process, and how we treat verification like engineering to find success in developing proofs.
Dr. Giuliano Losa and Dr. Mike Dodds presented a paper, On the Formal Verification of the Stellar Consensus Protocol, for the Workshop on Formal Methods for Blockchains (FMBC 2020). They discussed the formal verification of safety and liveness properties of the Stellar Consensus Protocol, which forms the basis of the Stellar blockchain network.
Dr. David Thrane Christiansen and Langston Barrett presented a video abstract on “Klister,” an ML-like language, at TyDe 2020. Type-driven Development (TyDe) is a workshop on types, type-driven programming, and type-based formal methods. Klister’s hygienic type-driven macros have a predictable yet procedural programming model. Klister’s macros are hygienic because they prevent variable capture by default. They are type-driven because macros have access to the type that is expected for the expression that is to be produced. Macros are written in the full Klister language, rather than a restricted subset in the style of Scheme’s syntax-rules, and macro developers can be unaware of the type checker’s implementation details – particularly the order in which it traverses expressions. Also part of the presentation: Samuel Gelineau of SimSpace.
Machine Learning
Dr. Jennifer Paykin gave a presentation about quantum computing aimed at programming languages researchers at the PLanQC (Programming Languages for Quantum Computing) conference.
Dr. David Darais served as a program committee member of Programming Language Design and Implementation (PLDI), a top-tier publication venue in programming languages, and Dr. Mike Dodds served on the external review committee of PLDI 2020.
Dr. Walt Woods was a guest on the Data Skeptic podcast episode, Adversarial Explanations with Data Skeptic. The interview regarded adversarial explanations, which leverage a security loophole in state-of-the-art neural networks to demonstrate their internal logic more robustly.
Dr. Yerim Lee, Dr. Nichole Schimanski, Dr. William Harris, Dr. Mark Tullsen, Dr. Eric Davis, Dr. Walt Woods, Richard Jones, and Sam Cowger co-authored a paper, ICARUS: Building Parsers out of Feathers and Wax, for LangSec 2020, on how real-world data formats evolve as they find use in real-world applications. The paper discussed how a comprehensive ICARUS toolchain for understanding and hardening resulting de facto formats can identify and address security risks arising from this evolution. You can also view a video of the presentation.
Data Science
Dr. David Archer will present the paper, Privacy-Preserving Computation on Multi-Agency Sensitive Government Data, for the New Techniques and Technologies for Statistics (NTTS) conference in Spring 2021. He will report the methods, results, and performance characterization of statistical computations on multiple linked datasets. All data remains private to individual data providers during all parts of the data analysis.
Dr. David Darais co-authored Short Paper: Probabilistically Almost-Oblivious Computation, for Programming Languages and Analysis for Security (PLAS 2020). He discussed how oblivious data structures are not purely oblivious, but they are almost oblivious; or, some adventures in formally verifying oblivious algorithms. Also part of the team: Ian Sweet (University of Maryland) and Michael Hicks (University of Maryland).
Dr. James Parker presented a paper: Verifying replicated data types with typeclass refinements in Liquid Haskell for OOPSLA. The paper presented an extension to Liquid Haskell that facilitates stating and semi-automatically proving properties of typeclasses. Also part of the team: Yiyun Liu, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou.
Dr. Ajay Eeralla and Christopher Lynch presented a paper, Bounded ACh Unification, for MSCS (Mathematical Structures in Computer Science), on how they designed an algorithm to solve a problem of unification modulo ACh (Associativity, Commutativity, homomorphism) theory and implemented it in Maude.
Hardware and Cyber-Physical Systems
Dr. Georgios Dimou served on the steering committee for the ASYNC Composium, which sought to define the direction of the ASYNC Composium and the research community as a whole.
Dr. Daniel Zimmerman, Dr. Joseph Kiniry, and Max Orhai presented a paper, The BESSPIN Tool Suite: Balancing the Evaluation of System Security Properties with Industrial Needs, for GOMACTech. The paper provided a high-level overview of the BESSPIN Tool Suite, which Galois developed as part of our project in DARPA MTO’s SSITH program. The DARPA SSITH program aims to allow hardware security architectures and their properties to be expressed and reasoned about at both the abstract (model) and concrete (product) levels.
Dr. Joseph Kiniry participated on the Ask the Hardware Security Experts your Security Questions panel at the Virtual Hardware Security Summit panel on the core challenges and opportunities for hardware security.
Dr. Aditya Zutshi was a program committee member on Hybrid Systems: Computation and Control (HSCC), which is one of the most important conferences for hybrid systems and the intersection of controls and computer science.
Dr. Aditya Zutshi was invited to the Runtime Verification Panel for Autonomy to talk about runtime verification challenges at the 20th International Conference on Runtime Verification.
Dr. Aditya Zutshi, Dr. Matthew Clark, and Yi Chou presented a paper, High Assurance Run-Time Monitoring Architecture for Autonomous Control, for AIAA SciTech, on a run-time assurance approach to provide safe recovery when using complex learning-enabled autonomous components in safety-critical systems.
Cybersecurity
Dr. Joseph Kiniry was invited to be a guest speaker at USC Election Cybersecurity Initiative: Oregon, the Oregon edition of the USC Election Cybersecurity Initiative (USC Annenberg Center on Communication Leadership and Policy University of Southern California).
Dr. Daniel Zimmerman was a guest at the podcast embedded.fm episode, “Integrity of the Curling Club,” concerning election security and hardware security.
Dr. David Archer wrote, “Can private data as a service unlock government data sharing?” for Government Computer News. Government organizations hold sensitive data that can be used to improve citizen services, prevent cyber-related incursions, or provide more personalized health care. Although this data’s impact is capped because data sharing between organizations is highly restricted, emerging privacy-preserving technologies hold promise in solving this conundrum.
Dr. Tristan Ravitch gave a talk, Embrittle: Binary Diversification and Fault Encouragement, at Software Security Summer School at Purdue University. This tutorial session demonstrated the tools developed under the Software Fault Encouragement for practitioners.
Contract Award Announcements
LINK by Dr. Charisee Chiw and Dr. Eric Davis
Part of DARPA’s Computable Models (COMPMods) program, LINK aims to make it easier for scientists to build multiphysics models with an end-to-end, automatic, and portable solution.
A modeling-as-a-service (MaaS) model registry framework for existing models. Galois is developing the SuperMaaS project as part of DARPA’s World Modelers program. Galois is also partnering with the Bill and Melinda Gates Foundation and the Ethiopian government’s Decision Support Modeling Tools for Ethiopia (DSMT-E) project, which focuses on food security modeling.
AIMEE Program: SEEC project by Dr. Jennifer Paykin, Dr. Scott Moore, and Raj Petra.
SEEC is part of DARPA’s Artificial Intelligence Mitigations of Emergent Execution (AIMEE) program, whose goal is to anticipate the potential for emergent computations early in a system’s design. SEEC is designed to identify unexpectedly programmable behaviors of systems that could be manipulated by bad actors. SEEC’s goal is to create a reusable framework that helps designers build systems that are resilient to these emergent computations.
Galois’s Agile Metamodel Inference using Domain-specific Ontological Languages (AMIDOL) project has been a great success throughout 2020. The project funding currently amounts to $2.7 million as part of DARPA’s Automating Scientific Knowledge Extraction (ASKE) program, which was designed to encourage the automation of data models.
SIEVE Program: FROMAGER project by Dr. Bill Harris, Dr. Alex Malozemoff, and Dr. David Archer
A zero-knowledge proof (ZKP) is a mathematical tool that provides irrefutable proof of a claim’s validity without revealing anything else about the claim or the data used to prove it. We won a $12.6 million zero-knowledge proof contract with the U.S. Defense Advanced Research Projects Agency (DARPA) as part of the Securing Information for Encrypted Verification and Evaluation (SIEVE) program. FROMAGER seeks to scale ZKPs to support complex proof statements, such as proving that a vulnerability exists without revealing the vulnerability or proving that software satisfies safety guarantees without revealing the proof of safety.
RACE Program: ROCKY project by Dr. Alex Malozemoff and Dr. David Archer
Galois project, Reliable Obfuscated Communications Kit for everYone (ROCKY), won $7 million as part of the DARPA Resilient Anonymous Communication for Everyone (RACE) program. ROCKY seeks to hide critical data within network traffic through sophisticated cryptographic methods and advanced machine learning techniques – delivering a knock-out for privacy protection.
GAPS Program: PIRATE project by Dr. Joe Hendrix
Galois was awarded a $7.5 million contract by DARPA to work on PIRATE, a set of software development tools for designing and building high-performance, physically-partitioned applications that protect sensitive information. The project is part of DARPA’s Guaranteed Architecture for Physical Security (GAPS) program.
As part of DARPA’s Assured Autonomy program, this Galois project aims to develop an assurance framework specifically for cyber-physical systems that rely on machine learning or learning-enabled controllers.
NSA Vulnerability Triage Study by Dr. Ben Davis, Dr. Scott Moore, Dr. John Launchbury.
This project explores opportunities for machine assistance in assessing whether software vulnerabilities should be fixed or reserved for intelligence use.
ARCOS Program: RACK project by Dr. David Archer
RACK (Rapid Assurance Curation Kit), part of the DARPA ARCOS (Automated Rapid Certification Of Software) program, uses a structured semantic data model. RACK specifically provides a “data ingestion interface” for ARCOS performers who need evidence to craft assurance arguments.
Software Releases
DaeDaLus: DaeDaLus is a flexible data description language for generating parsers with data dependencies.
Format Analysis Workbench (FAW) : FAW is a platform for running and analyzing the output from many parsers dealing with a single file format.
Matterhorn: In 2020, we made 9 releases of the Matterhorn project (our Unix terminal Mattermost client) and added dozens of new features and bug fixes. Hundreds of users download Matterhorn each month, and it continues to be a successful open source Haskell project that Galois maintains. Many people also use Matterhorn within Galois. (The team included Jonathan Daugherty, Kevin Quick, Eric Mertens, Isaiah Mindich, as well as community members.)
Software Analysis Workbench (SAW): We released versions 0.5 and 0.6 in 2020 (PDI Team).
Crux: We made the first public release of Crux, version 0.4, in 2020 (PDI Team).
Cryptol: We released versions 2.9.0, 2.9.1, and 2.10.0 in 2020 (PDI Team).
Flex Language: This software was developed by Galois, and then transitioned to its spin-out, Tangram Flex. Flex Language was released in Tangram Pro 1.2. (The team included James Lamar, Andrew Kent, and Dr. John Launchbury.)
Other Community Engagements
Dr. David Archer:
–Serves on the United Nations Privacy-Preserving Task Team steering committee, which develops opportunities and provides training to United Nation member states on privacy-preserving techniques and technology, especially for official statistics computations.
–Serves as a member of the Information Science and Technology (ISAT)’s Data-Oblivious Interdisciplinary Representation (DOPLR) Working Group. Data-oblivious programming is a key enabler across several domains, yet remains impractical and unsupported by current programming languages. This working group seeks to explore the extent to which DARPA might address this problem.
–Served as a program committee member for Real World Crypto Conference 2021.
Dr. David Darais:
–Serves as chair of the steering committee for Type-driven Development (TyDe) a workshop on types, type-driven programming, and type-based formal methods.
–Provided perspectives on research opportunities in industry at the PhD Recruiting Workshop.
Dr. Eric Davis:
–Serves as a member of the University of Florida Industrial Advisory Board for research and academics at the University of Florida Computer and Information Science and Engineering Department.
–Serves on the program committee for the American Statistical Association’s Justice, Equity, Diversity, and Inclusion (JEDI) Outreach Group.
Dr. Mike Dodds:
–Serves on the steering committee for the Logic Mentoring Workshop, a mentoring workshop for members of the logic community at the Logic in Computer Science (LICS) conference.
Dr. Joseph Kiniry:
–Serves as a member of the Board of Advisors for Verified Voting.
–Serves on the editorial board of IEEE IT Pro He co-writes the column, “Formal Methods in Industry.”
Dr. John Launchbury:
–Identifies topics in cybersecurity that need to be brought to the attention of national policy makers for the National Academies Forum on Cyber Security.
–Serves on the Information Science and Technology (ISAT) Steering Committee, shaping and shepherding multiple concept studies to help DARPA visioning.
–Served on the National Security Agency’s panel of Distinguished Experts and helped select the annual best paper in Science of Security for an NSA award.
–Appeared at the SEI DARPA Workshop on Software Engineering, focusing on the Identification of Grand Challenges and Visions in future software engineering.
Dr. John Launchbury and Dr. Stephen Magill:
–Served on the steering committee for the NSA/DARPA conference on High Confidence Systems and Software (HCSS). Launchbury and Magill shaped the content and schedule for the HCSS conference, which brings together government, industry, and academia.
Dr. Jennifer Paykin:
–Served on the program committee for the 5th Workshop on Principles of Secure Compilation (PriSC) 2021.
Dr. Tristan Ravitch and Dr. Charisee Chiw:
–Served on the program committee for the Correctness Workshop.
Dr. Aaron Tomb:
–Served on the program committee for Computer Aided Verification (CAV) 2020.
Dr. Walt Woods:
–Invited to talk at PurdelPL about understanding de facto formats through grammar inference, and why reinforcement learning might help.