2024: Year in Review

As 2024  comes to a close and a new year begins, we’re excited to reflect on a great year at Galois that saw groundbreaking research projects, innovative software releases, and impactful new collaborations. We love what we do, and it’s fun to share highlights made possible by working well together!

Highlights

Formal Methods Goes Operational: Cryptol, Galois’s mathematically-focused programming language for creating, analyzing, and verifying complex cryptographic algorithms, was transitioned into pre-production in support of the Department of Defense (DOD). Taphos, Galois’s tool that automatically analyzes code, generating a map of the dependency relationships between each component, was also successfully deployed to operational use cases within the DOD.

Advancing the State of the Art in Zero Knowledge Proofs: Galois completed its work on DARPA’s Securing Information for Encrypted Verification and Evaluation (SIEVE) program. Over the course of our research, Galois pushed ZKP performance forward significantly and pioneered several new applications with far-reaching impact for proving vulnerabilities while maintaining privacy and security in both software and hardware. 

‍Blockchain Innovations: Galois wrapped up a project supporting a new data protection blockchain, known as “Midnight,” developed by IOG. As part of this effort, Galois collaborated with Midnight and Intersect to implement recursive zero-knowledge (ZK) proofs in an open source ZK library called Halo2. 

The highlights above are just a taste of the team’s numerous accomplishments over 2024. Scroll down and read on for more details about 2024 software/tool releases, as well as a detailed listing of all publications and presentations (organized by research area).

Software/Tool Releases, Updates, and Commercialization

Galois released Cryptol 3.2.0, Crux 0.9, and SAW 1.2 – all significant updates to our core set of formal verification tools.

Galois released several updates to the CAMET Base Pack, through version 1.8.1. This latest version updates the Risk Management Framework (RMF) analysis tool to support revision 5 of the NIST security controls catalog, and works with OSATE version 2.12. This version also includes a variety of bug fixes and enhancements.

Galois released GUMBO GUI, a graphical tool for specifying GUMBO Contract Language (GCL) in Cameo/MagicDraw.

Galois released the new INsight to Diverse Information using Graphs and Ontologies (INDIGO) tool to the CAMET Library. 

Galois released Cadenas, an Android application for covert communication, utilizing a technique known as model-based format-transforming encryption to help users subvert censorship.

Galois released Swanky 0.6, our open-source suite of Rust libraries for secure multiparty computation. This release was notable as the beginning of a “continuous publication” practice, where updates to our internally-maintained development branch are immediately made available to the public. 

Galois released Cheesecloth, a compilation pipeline for producing Zero-Knowledge Proofs (ZKPs) about LLVM (C, C++, Rust) programs. Also in the world of ZKPs, Galois released Diet Mac’n’Cheese, a ZK backend proof system based on VOLE

Software and Systems Analysis (SSA)

Galois published preprint papers describing two of our industry-strength verification tools. The first, Macaw: A Machine Code Toolbox for the Busy Binary Analyst,” was written by Galwegians Ryan Scott, Ben Davis, Iavor Diatchki, Mike Dodds, Kevin Quick, Daniel Matichuk, Valentin Robert, and Ben Selfridge, along with co-authors Brett Boston, Joe Hendrix, Tristan Ravitch, Andrei Ștefănescu, Daniel Wagner, and Simon Winwood. In this paper, the authors presented Macaw, a modular framework that makes it possible to rapidly build reliable binary analysis tools across a range of use cases. The second paper, “Crux, a Precise Verifier for Rust and Other Languages,” was written by Galwegians Stuart Pernsteiner, Iavor Diatchki, Mike Dodds, and Ryan Scott, along with co-authors Robert Dockins, Joe Hendrix, Tristan Ravich, Patrick Redmond, and Aaron Tomb. This paper presents Crux, a cross-language verification tool for Rust and C/LLVM. Both tools are being used extensively in the wide world beyond Galois’s hallowed halls.

Iavor Diatchki presented “Daedalus: Safer Document Parsing” at PLDI 2024. The paper, which resulted from Galois’s work on the DARPA SafeDocs Program, explores Daedalus – our new language-independent parser generator for implementing safe and efficient parsers, accompanied by a well-defined semantics and IR for implementing domain-specific parser analyses. It was written by Galwegians Iavor Diatchki, Mike Dodds, David Holland, Benoit Razet, and Cole Schlesinger, along with co-authors Harrison Goldstein, Bill Harris, and Simon Winwood.

Galwegian Benoit Razet, along with co-authors Paul Pazandak, Fabrizio Bertocci, and Brian Senese, presented a paper entitled “Fielding Faster: Remove Time and Cost Barriers to Software Certification Using Qualifiable Code Generators” at the 2024 AIAA DATC/IEEE 43rd Digital Avionics Systems Conference (DASC).

Galwegians David Darais, Sourya Dey, and Scott Moore, along with co-authors John M. Abowd, Tamara Adams, Robert Ashmead, Simson L. Garfinkel, Nathan Goldschlag, Daniel Kifer, Philip Leclerc, Ethan Lew, Rolando A. Rodríguez, Ramy N. Tadros, and Lard Vilhuber, published an article entitled “The 2010 Census Confidentiality Protections Failed, Here’s How and Why” with the National Bureau of Economic Research (NBER).

Mike Dodds gave several talks on the industry applications of formal methods. These included “N Things I Learned Trying to Do Formal Methods in Industry,” “Proofs in the Wild: What’s done today? What’s close? What’s far?,” “How Do We Know Weak Memory Matters”, and “LLMs are Useful for Small Problems.”

Galwegians Olivier Belanger, David Darais, and Cole Schlesinger, along with co-authors Mark Moeller, Jules Jacobs, Steffan Smolka, and Alexandra Silva, published an article entitled “KATch: A Fast Symbolic Verifier for NetKAT.” The paper, which resulted from Galois’s work on the ONR 5STARS project, describes the team’s work developing new structures and algorithms for performant, scalable, symbolic verification of network properties using NetKAT. It was presented at PLDI 2024.

Additional Thought Leadership and Blogs

• Function Argument Nullability Using an LLM by Mark Tullsen, Stuart Pernsteiner, and Mike Dodds
• Generative AI for Specifications by Mike Dodds, Joe Kiniry, and Shauna Sweet
• Galois / Twisp: Avoiding Foolishness in Distributed Systems by Mike Dodds
• Immunant, Inc. CEO Per Larson published an article entitled “Migrating C to Rust for Memory Safety,” which describes C2Rust, a joint Galois-Immunant project. 

Advanced Cryptography and Privacy 

Galwegian David Archer, along with co-authors Abha Moitra, Kit Siu, and Paul Cuddihy, published “Principles and Metrics for Digital Curation in Aviation.” The paper, which was presented at the Digital Avionics Systems Conference, formalizes the principles of data curation for digital engineering certification and assurance cases, and provides quantified metrics for assessing compliance of a dataset to those principles. Archer also presented a paper at GOMacTech 2024 entitled “BASALISC: Programmable Hardware Accelerator for BGV and CKKS FHE.” 

Archer also gave a talk entitled “Waiting for BASALISC - Silicon in the Oven!” at the KUL Hardware Summit for Computing on Encrypted Data, and another entitled “Fully Homomorphic Encryption in theory and practice” for the UK National Cyber Security Centre. 

Galwegian James Parker, along with co-authors Daniel Luick, John C. Kolesar, Timos Antonopoulos, William R. Harris, Ruzica Piskac, Eran Tromer, Xiao Wang, and Ning Luo, presented their paper “ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge” at USENIX Security 2024.

Additional Thought Leadership and Blogs

• Advancing the State of the Art in Zero Knowledge Proofs: SIEVE Wrap Up by Andrew Shaughnessy
• AI/ML and the Privacy/Security Dilemma - Q&A with David Darais, Rawane Issa, and Sourya Dey
• Formal Verso: the Formal Methods Future of Smart Contract Security by Andrew Shaughnessy
• Introducing Cheesecloth: A Tool for Proving Software Vulnerabilities in Zero Knowledge by Andrew Shaughnessy
• Galois Unlocks the Power of Private Set Intersection: A Game-Changer for Data Privacy by Andrew Shaughnessy
• Bringing Zero Knowledge Proofs to the Masses by Andrew Shaughnessy
• Subverting Censorship: How a Galois-developed Android App Could Change the Game for Pro-Democracy Activists by Andrew Shaughnessy

Rigorous Digital Engineering (RDE) 

Joe Kiniry gave a talk entitled “Scaling Formal Methods in the Field at Galois” for the NSF Formal Methods in the Field (FMitF) 2024 PI meeting. He also gave the keynote address, “What happens when the government starts encouraging the use of formal methods?” at ABZ 2024 – 10th International Conference on Rigorous State Based Methods

Galois published the final Open Systems Verification Demonstration (OSVD) report as part of our work in the Future Attack and Reconnaissance Aircraft (FARA) program. The report, entitled “Model Based Engineering Support for Future Attack Reconnaissance Aircraft,” was written by Galwegians Tyler Smith, Ed Sandberg, Steve Vestal, Alex Mahrer, and Taisa Kushner, along with co-authors Moira Southern and Charlie Payne.

Taisa Kushner gave a presentation entitled “Replicating Glucose Dynamics of People Living with T1D using Physiology-Guided AI MOdels” at the International Conference on Advanced Technologies and Treatments for Diabetes (ATTD) in Florence, Italy.

‍Additional Thought Leadership and Blogs

• Surrogate Modeling for Rapid Decision-Making by Alex Grushin
• Visualizing Codebases as Cities by Tyler D. Smith
• How Do You Modernize Safety Critical Designs in Nuclear Power? RDE! by Andrew Shaughnessy
• Rigorous Robot Security: How Galois’s RDE Framework is Streamlining NIST Compliance and Change Impact Analysis for Cyber-Physical Systems by Andrew Shaughnessy

AI/ML and Data Science

Galwegians Sourya Dey, Andrew Lauziere, Jonathan Daugherty, and Cait Burgess, together with co-authors Michael Robinson and Shauna Sweet, wrote a paper entitled Analyzing Large Language Model Behavior via Embedding Analysis. The paper, which was presented at the AHFE International Conference on Human Factors in Design, Engineering, and Computing (AHFE 2024 Hawaii Edition), explains the behavior of large language models (LLMs) by analyzing token embeddings in their internal structure. 

Galwegian Sourya Dey also co-authored a paper with Michael Robinson and Shauna Sweet entitled “The structure of the token space for large language models.” In the paper, the authors compute the dimension and curvature of the token space of large language models (LLMs) and analyze the implications of these topological and geometric properties on model behavior.

Galwegian Alexander Grushin, along with co-authors Walt Woods, Simon Khan, and Alvaro Velasquez, published a paper entitled “Combining AI Control Systems and Human Decision Support via Robustness and Criticality.” The paper, which describes a set of techniques for making reinforcement learning models more interpretable and robust, was presented by Grushin and Khan at Disruptive Technologies in Information Sciences VIII (part of SPIE Defense + Commercial Sensing 2024).

Additional Thought Leadership and Blogs

• Mechanism Design and the CAMDEN Program by David Burke
• What are Self-Organizing Maps? by Donya Quick
• The Need for Speed: Revolutionizing CPS Design with AI by Andrew Shaughnessy
• Prevent the Next XZ Incident: Galois’s LAGOON Tool Offers an Answer to Open-Source Software Threats by Andrew Shaughnessy
• Is Your Technology Human-Ready? By Katrina Scheisman
• How Machine Learning Can Transform Healthcare by Andrew Shaughnessy

Miscellaneous Blogs and Publications

• My People Experience at Galois: The Community Leads the Way by Julie A.

Community Involvement: Committees, Boards, Panels, Seminars, and Workshops

Ryan Scott served on the program committee for FUNARCH 2024. He also gave a keynote talk, entitled “Copilot, Assured Runtime Verification for Embedded Systems and Hardware,” for SSH-SoC (Safety and Security in Heterogenous Open Systems-on-Chip) 2024.

Scott Moore served on the USENIX Security program committee at the 34th USENIX Security Symposium, the LangSec program committee for the IEEE CS Security & Privacy Workshops, and on the Computer Security Foundations Symposium program committee for CSF 2025.

Tyler Smith served as a panelist at the 2024 MOSA Summit, speaking about Army Aviation digital engineering efforts and “Lessons Learned.” He also co-chaired the Army Aviation Architecture Collaboration Working Group (ACWG) Digital Engineering SubGroup (DESG), facilitating discussions on digital engineering strategy for Army Aviation efforts. 

David Archer served on a panel discussing applications and technology for fully homomorphic encryption (FHE) at MILCOM 2024. He also led a breakout session on hardware interfaces for FHE accelerators at the 7th HomomorphicEncryption.org Standards Meeting, and another on practical industry application for FHE at the Privacy Enhancing Technologies Summit for the EU. In addition, Archer was appointed to the Expert Panel for the newly formed National Secure Data Service, served on the NSF Privacy-Preserving Data Sharing in Practice (PDaSP) Selection Panel, and continues to serve as an active member of the Callisto Project cryptographic advisory board. 

Aditya Zutshi served on the program committee for the ARCH Workshop: Applied Verification for Continuous and Hybrid Systems. The ARCH workshop addresses verification techniques for continuous and hybrid systems with a special focus on the transfer from theory to practice and maintains a curated set of verification benchmarks submitted by academia and industry. 

Looking Forward

As we look back on 2024, we’re inspired by the progress our team has made and excited for the opportunities that lie ahead. Scientific research and technological innovation remain central to our mission, and the brilliance, creativity, and curiosity at the heart of the Galwegian community empowers us to address some of the world’s most pressing challenges. Thank you for being a part of this journey!