2021. Wow. There it went. And far more interesting than most of us anticipated. While weathering the various world storms, we also managed to keep advancing the cause of building trustworthy computing systems. Galois continued pioneering work in formal methods, high-assurance cryptography, machine learning, data science, rigorous digital engineering, and more. From our virtual perch, we participated in a great variety of technical conversations and deep dives with refreshingly light travel schedules.
Below are pointers and references to the highlights of our year. A very sincere “Thank You” goes to the partners, customers, and teammates who helped advance this work. Let’s hope for a somewhat less interesting, but just as prosperous 2022!
Protecting a Vehicle’s Electronics at the Source
Dr. Joseph R. Kiniry, Dr. Daniel Zimmerman, Dr. Michal Podhradsky, Ethan Lew, and Dr. Ramy N. Tadros revealed the cyber-physical demonstrator for Galois’s BESSPIN technology. The demonstrator is intended to showcase the use of DARPA’s SSITH secure hardware technology in a passenger vehicle.
This exciting new technology aims to tackle underlying hardware vulnerabilities rather than relying on security patches for a car’s software.
You can read more about the BESSPIN cyber-physical demonstrator on Github. You can also watch a long and short video of the demonstrator showing what happens during a remote exploit of a vehicle, and how SSITH could prevent such an exploit from occurring.
The Book of FETT
Dr. Daniel Zimmerman presented a paper, FETT: Deploying RISC-V Systems-on-Chip to the Cloud for Security Research, at GOMACTech 2021. The paper described the tools and systems-on-chip that Galois developed for the SSITH program in service of running DARPA’s first-ever bug bounty program, the DARPA Finding Exploits to Thwart Tampering (FETT). The paper’s co-authors are Dr. Joseph Kiniry, Dr. Ramy N. Tadros, and Dylan Hand.
The Equivalence Must Flow
Galois hosted 2021’s International Symposium on Asynchronous Circuits and Systems (ASYNC) – “the premier forum for researchers to present their latest findings in the area of asynchronous design.” Dr. Daniel Zimmerman served as the invited sessions chair and publications chair; Dylan Hand and Dr. Matheus Trevisan Moreira served as general chairs, and Dr. Georgios Dimou and Milos Krstic served as Program chairs.
Keynote speakers were Edith Beigne, the Research Director of AR/VR Silicon at Facebook Reality Labs; Dr. Kwabena Boahen of Stanford University; and Dr. Ran Ginosar, from the Technion & Ramon Space.
Ms. Beigne’s talk was titled, “AR/VR silicon challenges and research directions – what opportunities for asynchronous design?”
Dr. Boahen’s talk was titled, “The Future of Artificial Intelligence: A 3D Silicon Brain.”
Dr. Ginosar’s talk was titled, “Asynchronous Design for Space Applications.”
More information about each keynote speech is here.
Additionally, Dr. Jennifer Paykin, Dr. Brian Huffman, Dr. Daniel Zimmerman, and Dr. Peter Beerel co-authored a paper, Formal Verification of Flow Equivalence in Desynchonized Designs, that was selected as Best Paper at the ASYNC ‘21 symposium.
Spin-Out News: MuseDev Acquired by Sonatype
Galois experienced two spin-out milestones in 2021. In March, MuseDev – which created a software solution that automatically analyzes and provides uniquely accurate feedback on each developer pull request – was acquired by Sonatype, the leader in developer-friendly tools for software supply chain management and security.
Spin-Out News: Announcing Niobium Microsystems
In July, we announced our newest spin-out, Niobium Microsystems, which is devoted to the creation of trusted microelectronic systems. Galois is well-known for its focus on formal methods and high assurance for software validation, but some of the company’s most cutting-edge research involves System-on-Chip design. Niobium Microsystems builds on this body of work, advancing into applied research and custom system design toward building high-performance and trustworthy systems.
Continuing Best Practices in Reliability
Galois’s podcast, Building Better Systems, established itself in 2021 with ten episodes exploring a wide range of topics, from censorship circumvention to formal methods and machine learning. Dr. Joey Dodds and Shpat Morina hosted guests that included Dr. Talia Ringer, Dan Guido, Dr. Aditya Thakur, Tycho Andersen, Dr. Gregory Malecha, Dr. Alastair Reid, Dr. Rod Chapman, and Dr. Leo de Moura, as well as fellow Galwegians Dr. Eric Davis, Dr. Alex J. Malezemoff, and Marc Rosen.
Galois in the Community
“Absolutely brilliant work,” said Amazon Web Services (AWS) CTO Werner Vogels about Galois’s project for AWS. Brett Boston, Samuel Breese, Dr. Joey Dodds, Dr. Mike Dodds, Dr. Brian Huffman, Andrei Stefanescu, and Adam Petcher completed machine-assisted proofs of two highly optimized cryptographic primitives, AES-256-GCM and SHA-384 – making Galois the first to formally verify these implementations, which protect the security of nearly everybody on the Internet. The team also presented their paper on the same subject at the 33rd International Conference on Computer-Aided Verification (CAV 21).
Galois customer Informal Systems wrote an informative blog post about Galois’s work verifying the Cosmos protocol.
Hacker News discussed Proofs Should Repair Themselves, a Galois blog post written by Dr. Mike Dodds.
Hacker News also discussed You Already Know Formal Methods, a Galois blog post written by Dr. Joey Dodds.
The Galois Blog
And, speaking of our blog, we wrote many informative articles throughout the year. Subjects included software tutorials and demos; asynchronous hardware design; cryptography; and discussions about formal methods, among many other topics.
Below, see links to our papers, software releases, and the public presentations we made throughout 2021.
Zero-Knowledge Proofs
Dr. David Archer’s article, Zero-Knowledge Proofs, D-Day, and the Promise of Trustable Software, which specifically focused on proofs of software security, appeared in United States CyberSecurity Magazine’s Winter 2021 issue.
Dr. David Darais co-authored a paper, Zero-Knowledge Static Program Analysis, which he presented at the virtual 2021’s ACM Conference on Computer and Communications Security (CCS 2021), held in November 2021. He discussed executing abstract interpretation in zero-knowledge for proofs of program properties which keep the program secret. Also part of the team: Joseph Near (University of Vermont); Zhiyong Fang (Texas A&M University) and Yupeng Zhang (Texas A&M University).
Dr. Alex J. Malozemoff and Marc Rosen, as well as Dr. Carsten Baum and Dr. Peter Scholl, gave a presentation – Mac ‘n’ Cheese: Zero-knowledge Proofs for Boolean and Arithmetic Circuits with Nested Disjunctions, in August 2021 at CRYPTO 2021. This paper (created as part of DARPA’s SIEVE program) introduces a new interactive zero-knowledge proof system that is both highly performant and allows optimization for network communication when proving statements with disjunctions. You can watch the video of the presentation here.
Marc Rosen presented (along with James Parker and Dr. Alex J. Malozemoff) the paper, Balboa: Bobbing and Weaving Around Network Censorship at USENIX Security 2021 in August 2021. This paper introduces a new approach to censorship circumvention developed in Galois’s ROCKY project (part of DARPA’s RACE program).
Dr. Benoit Razet co-authored a paper, Appenzeller to Brie: Efficient Zero-Knowledge Proofs for Mixed-Mode Arithmetic and Z2k. The paper (part of DARPA’s SIEVE program) introduces an efficient protocol for “switching” between fields in a zero-knowledge proof. Also part of the team: Dr. Carsten Baum, Lennart Braun, Alexander Munch-Hansen, and Dr. Peter Scholl.
High-Assurance Cryptography
Dr. Marios Georgiou gave a presentation, One-Shot Signatures, at Second Kyoto Workshop on Quantum Information, Computation, and Foundation on September 15, 2021. He discussed the use of quantum cryptography to create digital signatures that can sign a single message.
Dr. Marios Georgiou gave a presentation, Unclonable Secret Keys, at the Computation and Reasoning Laboratory Seminar, National Technical University of Athens in August 2021. He discussed the use of quantum cryptography to build cryptographic primitives whose secret keys cannot be copied.
Dr. Joey Dodds gave a talk, Challenges and Opportunities in Implementation and Verification of Cryptography, at IEEE Secure Development Conference 2021 on October 19, 2021.
Software Correctness and Formal Methods
Dr. Mike Dodds chaired the online Galois workshop, Formal Approaches to Certifying Compliance (FACC) 2021 on July 19, 2021. The workshop focused on compliance and certification using formal methods.
Dr. Joe Hendrix, Andrew Kent, and Simon Winwood gave a presentation on Verifiable Binary Lifting at HCSS 2021 on May 6, 2021. This talk describes work at Galois on building a verifiable decompiler from machine code to LLVM.
Dr. Joe Hendrix, Andrew Kent, and Simon Winwood gave a presentation at Lean Together 2021 on January 6, 2021 about how Galois uses Lean 4 to work toward verified decompilation.
Paul He, Dr. Eddy Westbrook, Brent Carmer, Chris Phifer, Dr. Valentin Robert, Dr. Karl Smeltzer, Andrei Stefanescu, Dr. Aaron Tomb, Dr. Adam Wick, Matthew Yacavone, and Dr. Steven Zdancewic co-authored a paper, A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs. They gave a presentation at OOPSLA 2021 in October 2021, discussing new approaches to formal verification in SAW of programs with unbounded loops.
Dr. Walt Woods gave a presentation, RL-GRIT: Reinforcement Learning for Grammar Inference, at The Seventh Workshop on Language-Theoretic Security (LangSec 2021, on May 27, 2021.
Dr. Stuart Pernsteiner and Dr. Adam Tomb gave a presentation introducing crux-mir, a Crucible-based testing tool for Rust programs at the Rust Verification Workshop 2021in April 2021.
Data Science
Dr. David Darais co-authored a paper: DDUO: General-Purpose Dynamic Analysis for Differential Privacy, presenting it at the 34th IEEE Computer Security Foundations Symposium(CSF 2021) on June 24, 2021. The paper discussed runtime verification of privacy in Python via dynamic enforcement of function sensitivity and differential privacy. Also part of the team: Chike Abuah, Joseph Near, and Alex Silence (all from the University of Vermont).
Dr. David Darias gave a presentation, Solo: Enforcing Differential Privacy Without Fancy Types, on June 21, 2021 at the Workshop on Foundations of Computer Security 2021 (FCS 2021) and also at Theory and Practice of Differential Privacy 2021 (TPDP 2021) in May 2021. The presentations related static verification of differential privacy in Haskell. Also part of the team: Chike Abuah, and Joseph Near (both from the University of Vermont).
Dr. David Darias and Dr. William Harris gave a presentation, Symphony: A Concise Language Model for MPC, at FCS 2021, discussing a programming language for dynamically coordinated secure multiparty computation. Also part of the team: Ian Sweet, Ryan Estes, David Heath, and Michael Hicks.
Dr. David Darais gave a presentation, Data-Oblivious Computation: A Common Paradigm for Private and Secure Computation, at HotSoS 2021 on April 14, 2021. Data-oblivious computation is a common paradigm for security and privacy-enhancing technologies, and developing new tools for this common paradigm has the potential to accelerate research for security and privacy.
Dr. David Darais gave a presentation, Improving Privacy-Preserving Deep Learning With Immediate Sensitivity, at TPDP 2021, discussing a new method for differentially private deep learning which achieves tighter bounds on privacy loss than prior techniques. Also part of the team: Timothy Stevens, Ben U Gelman, David Slater, and Joseph Near.
Dr. Scott Moore, Dr. Jennifer Paykin, and Dr. Olivier Savary Belanger will give an extended abstract and presentation describing their work on SEEC (part of DARPA’s AIMEE program) at Principles of Secure Compilation (PriSec 2022) in January 2022.
Hardware and Cyber-Physical Systems
Ethan Lew and Dr. Michal Podhradsky gave a presentation, Steal this Drone, at DEFCON 29 in August 2021. DEFCON participants were educated about – and challenged to hack – the SMACCMCopter secure quadcopter.
Dr. Joe Hendrix, Dr. Andrew Kent, and Ethan Lew wrote a blog post, Real-time Robotics Control in the Lean Language, in March 2021. The blog post described how the team wrote a Lean implementation of a robotics controller running on a single board computer.
Dr. Adam Wick and Dr. Aditya Zutshi hosted the Balloween workshop at Galois, bringing together autonomy and cyber-physical systems researchers to explore building a next-generation, high endurance, autonomous, lighter-than-air vehicle (blimps or balloons). You can read more about Balloween (which we hope will be in-person in the future) on the Galois blog.
Dr. Eric Davis, Dr. Sourya Dey, Matt LeBeau, and Ethan Lew participated in the SDCPS Hackathon with the SwRI corpus for UAV design as the ESSENCE team. The team achieved the highest scoring design and the only designs with fixed wings. They were the only team to optimize the control parameters of the autopilot.
Machine Learning
Dr. Eric Davis presented his paper, IAIDO: A Framework for Implementing Integrity-Aware Intelligent Data Objects, at iDSC in October 2021. He discussed utilizing artificial intelligence/machine learning to understand the trustworthiness of data in the wild and to remove threats for data poisoning.
Dr. Walt Woods was invited to speak at USC AAI Workshop 2021, giving a talk on, “Should it be easier to trust machines or harder to trust humans?” The talk focused on the following: “We trust humans to drive without comprehensive explanations, yet expect explanations from machines. Here, we’ll discuss specific limitations of current explainable AI, and have a brief discussion of these results contrasted against trusting humans on tasks like driving or reading radiology results.”
Dr. Eric Davis, Sourya Dey, Ethan Lew, Dr. Nichole Schimanski, Alex Grushin, and Sean Flannery hosted the virtual 2021 Galois Summer School for Trustworthy Machine Learning, Artificial Intelligence, and Data Science on June 28, 2021.
Contract Award Announcements
POLYMORPH: Part of DARPA’s V-SPELLS (Verified Security and Performance Enhancement of Large Legacy Software) program, POLYMORPH (Promotion to Optimal Languages Yielding Modular Operator-driven Replacements and Programmatic Hooks) will cover three technical areas – Levitate, Transmute and Augury, and Revivify. POLYMORPH’s goal is to allow domain experts to re-engineer legacy C/C++ systems by replacing components, recomposing existing components, and distributing components to hardware accelerators while improving run-time efficiency.
BASALISC: Part of DARPA’s Data Protection in Virtual Environments (DPRIVE) program, BASALISC (Bespoke Asynchronous Silicon-Accelerated LWE Intrinsics through Software/Hardware Codesign) aims to accelerate the “last mile” of data encryption with purpose-built ASICs that accelerate fully homomorphic encryption (FHE) computations. A key aim of the project is that our hardware should be cloud-ready – suitable for deployment in typical cloud server installations – to maximize commercial and government transition potential.
LAGOON: Part of DARPA’s SocialCyber program, LAGOON aims to protect online open-source software from social threats using AI.
GREASE: Generating Requirements Evidence with Analysis and System-level Enforcement (GREASE), a project for DARPA. Phase 1 SBIR award.
5STARS: Verification tools for software-defined networking in 5G infrastructure, a project for ONR. Phase 1 SBIR award.
Cybersecurity Characterization of Vehicle Electrical and Electronics Architectures, a project for the National Highway Traffic Safety Administration (NHTSA).
Software Releases
Cryptol: We released version 2.11 in March 2021.
Software Analysis Workbench (SAW): We released version 0.8 in April 2021.
UC-CRUX-LLVM: We released UC-CRUX-LLVM in 2021, an open-source command-line tool and Haskell library for performing under-constrained symbolic execution on LLVM code to expose bugs or verify the absence of certain types of undefined behavior. It requires only LLVM bitcode as input. It is built on Galois’s Crucible library for symbolic execution. You can read more about UC-CRUX-LLVM in our October 2021 blog post. Team: Langston Barrett, Ryan Scott, and Dr. Tristan Ravitch.
Control Systems Analysis Framework (CSAF): CSAF is a framework to minimize the effort required to evaluate, implement, and verify controller design (classical and learning enabled) with respect to the system dynamics. Team: Dr. Michal Podhradsky, Ethan Lew, Dr. Aditya Zutshi, and Chris Lockett.
LINK: LINK software for multi-physics model generation was released. Team: Chris Phifer, Dr. Yerim Lee, James LaMar, Richard Jones, and Dr. Eric Davis.
ESSENCE: The ESSENCE software for cyber-physical system design was released. Team: Chris Phifer, Dr. Yerim Lee, James LaMar, Richard Jones, and Dr. Eric Davis.
Other Community Engagements
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.
–Served on the program committee for PLDI 2021: Programming Languages, Design and Implementation, a top-tier publication venue in programming languages.
–Served on the program committee for TrustNLP @ NAACL 2021, held on June 10, 2021.
–Attended a panel at the National Science Foundation’s Software and Hardware Foundations program in 2021.
Dr. Eric Davis:
–Served on the program committee for Institute for Data Science and Computing (IDSC) held in October 2021.
–Served as a member of the University of Florida’s CISE Industrial Advisory Board.
Dr. Mike Dodds:
–Serving on the program committee for PLDI 2022: Programming Languages, Design and Implementation, a top-tier publication venue in programming languages.
–Served on the program committee for the SPLASH/OOPSLA 2021 conference held on October 17-22 2021.
Ethan Lew:
–Served on the program committee for ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2021) held on May 19-21, 2021.
–Served on the program committee for 7th IFAC Conference on Analysis and Design of Hybrid Systems, held July 7-9, 2021.
Dr. Scott Moore:
–Served on the IEEE Secure Development Conference 2021 Program Committee.
–Serving on the Principles of Secure Compilation Program Committee (PriSec 2022).
Dr. Tristan Ravitch:
–Served on the program committee for the CORRECTNESS ‘21 workshop.
Dr. Aaron Tomb (now at Amazon Web Services):
—Served on the program committee for the 33rd International Conference on Computer-Aided Verification (CAV 2021).
Dr. Aditya Zutshi:
–Served as Repeatability Evaluation PC Chair for the 7th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS ‘21).
–Served on the program committee for the ACM International Conference on Hybrid Systems: Computation and Control (HSCC 21), which was part of CPS-IoT Week, the premier event on Cyber-Physical Systems and Internet-of-Things.