As 2023 draws to a close, we take a moment to look back. It’s been a jam-packed year for Galois, from software releases to research breakthroughs. Our intrepid team of engineers and scientists has published papers, led workshops, served on committees and boards, presented at conferences, led science communication efforts, and spearheaded truly cutting edge research.
We are truly grateful to our partners and customers for the chance we have to work with you in these endeavors.
An Award a Decade in the Making: The HACMS Program, in which Galois played a key role, received DARPA’s prestigious “Game Changer Award,” honoring the significant and lasting impact HACMS has had over the past decade as the “gold standard” for cybersecurity and hack-proofing cyber-military systems.
100% Employee Ownership: In June, Galois officially became 100% employee-owned—a milestone made possible through our Employee Stock Ownership Plan (ESOP).
Throughout 2023, Galois has made significant strides across multiple (often-overlapping) research domains. Highlights include:
- Ryan Scott and Mike Dodds presented the CopilotVerifier tool as a method for ensuring the correctness of safety-critical monitoring code through automatically generated proofs, as detailed in their paper “Trustworthy Runtime Verification via Bisimulation.”
- David Archer, Ben Selfridge, and Daniel Wagner published a paper on BASALISC, an architecture family of hardware accelerators that aims to substantially accelerate Fully Homomorphic Encryption (FHE) computations in the cloud.
- Santiago Cuéllar, James Parker, and Stuart Pernsteiner advanced the state of the art for Zero-Knowledge Proofs in their paper “Cheesecloth: Zero-Knowledge Proofs of Real World Vulnerabilities.”
- Joe Kiniry gave a talk at this year’s ERI Summit about Galois’ groundbreaking work developing a side channel-resistant ASIC for DARPA.
- In “Automated Property-based Testing from AADL Component Contracts,” Danielle Stewart and Todd Carpenter presented the GUMBOX property-based testing framework, which automatically generates automated testing infrastructure for AADL component application code from AADL models and formal specifications written in the GUMBO Contract Language.
- Alexander Grushin and Walt Woods published a paper presenting a novel method for automatically and accurately computing a safety margin for reinforcement learning.
- Eric Davis, Sourya Dey, Adam Karvonen, Ethan Lew, Donya Quick, Panchapakesan Shyamshankar, Ted Hille, and Matt LeBeau co-authored a paper on “Leveraging Manifold Learning and Relationship Equity Management for Symbiotic Explainable Artificial Intelligence.”
These highlights are just a taste of the team’s numerous accomplishments over 2023. Scroll down and read on for more details about 2023 software/tool releases, as well as a detailed listing of all publications and presentations (organized by research area).
Software/Tool Releases, Updates, and Commercialization
Faster, Better, Easier-to-Use Verification Tools: We released Cryptol 3.0.0, Crux 0.7, and SAW 1.0. This significant update brought extensive overhauls and new features – an exciting leap forward for our core verification tools. As part of our wider effort focused on making formal verification tools more practical, speedy, and user-friendly, we also developed and released a new fuzzing tool aimed at streamlining the cryptographic verification process in SAW; and finished the REVERSER project and the “AutoSAW” tool, which reduces the overall time required of human engineers and lowering the barrier for verifying a system.
Building Out the Digital Engineering Toolbox: We added or upgraded several tools in the CAMET Library. This effort included releasing the CAMET Base Pack Comprehensive Bundle, releasing our FRIGATE modeling tool (which provides sensor coverage analysis and failure recovery planning for cyber-physical systems) and adding fully automated SysML v1 to AADL data translation capabilities and bidirectional translation capabilities to the SysML to AADL Bridge Tool. We also upgraded SLICED, our embedded computing integration behavioral modeling tool, to version 2.10.1, which supports and runs on top of the OSATE 2.11 modeling environment.
With more people than ever using digital engineering tools, we released an extensive set of practical, task-specific training materials for the Architecture Analysis & Design Language (AADL) and the freely available Cyber Assured Systems Engineering (CASE) tools developed by DARPA.
Zero Knowledge Proof Advances: As part of the Zero-Knowledge Proof-focused Fromager research project, we released Cheesecloth, which encodes proof statements for memory safety, integer overflow safety, performance security, information flow security, and functional equivalence. We also released version 2.1.0 of the SIEVE Circuit IR, a standardized format for encoding zero-knowledge proof statements as arithmetic or boolean circuits.
Rigorous Digital Engineering for Nuclear Power Systems: In the High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) project, Galois developed a high-assurance, safety-critical demonstration system for the Nuclear Regulatory Commission using Rigorous Digital Engineering (RDE). The HARDENS project was subsequently used as the foundation for the entire HALDEN workshop this year, and has influenced the future of nuclear power plants’ Digital Instrumentation & Control (DI&C) systems. It has also been reused and extended by at least two other government-sponsored programs.
Advancing UAV Cybersecurity: Galois’ ADIDRUS team, composed of David Burke, Raj Patra, David Lamkins, and Ted Hille, successfully produced a commercialization effort demo for DoD clients and investors/stakeholders from the Applied AI Company.
Building Better Tools for Legacy Software Analysis and Modeling: Galois open-sourced Yapall (Yet Another Pointer Analysis for LLVM), a static pointer analysis tool for programming languages that compile to LLVM. Developed as a part of the POLYMORPH project (itself part of the larger DARPA V-SPELLS program), this remarkable tool is instrumental in structural analysis of legacy applications and the generation of structural models of legacy software.
And More: Galois also formally specified post-quantum cryptographic algorithms recommended by the NSA for the Commercial National Security Algorithm Suite (CNSA 2.0); reached a major milestone in our first project for the U.S. Space Development Agency, focused on the creation of high-assurance, high-performance implementations of cryptographic functions for deployment in low earth orbit; and released a DLKoopman (v1.2.0), a general-purpose Python package for Koopman theory using deep learning.
Software and Systems Analysis (SSA)
Galwegians Scott Moore and Langston Barrett, together with co-authors Arash Sahebolamri and Kristopher Micinski, presented a paper entitled “Bring Your Own Datastructures to Datalog” at OOPSLA 2023, where it received a Distinguished Paper Award. The paper presents a framework for extending Datalog engines with custom data structures to improve performance or extend the semantics of Datalog.
Galwegians Eddy Westbrook, Matthew Yacavone, and Ryan Scott, along with co-author Lucas Silver, presented a paper entitled “Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification” at the 2023 European Conference on Object-Oriented Programming (ECOOP). This paper presents a specification framework for monadic, recursive, interactive programs that supports auto-active verification, an approach that combines user-provided guidance with automatic verification techniques.
Galwegian Naomi Spargo, together with co-authors Milijana Surbatovich, Limin Jia, and Brandon Lucia, presented a paper entitled “A Type System for Safe Intermittent Computing” at PLDI 2023. This paper presents a type system for enforcing safe intermittent execution; bugs unique to batteryless energy-harvesting devices (which execute intermittently, as energy is available) are caught at compile time.
Galwegian Oliver Bračevac, along with co-authors Guannan Wei, Songlin Jia, Ruiqi Gao, Haotian Deng, Shangyin Tan, and Tiark Rompf, presented a paper entitled “Compiling Parallel Symbol Execution with Continuations” at the 2023 IEEE/ACM International Conference on Software Engineering (ICSE).
Bračevac, along with co-authors Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, Tiark Rompf, presented a paper entitled “Graph IRs for Impure Higher-Order Languages – Making Aggressive Optimizations Affordable with Precise Effect Dependencies” at OOPSLA 2023.
Bračevac, along with co-authors Guannan Wei, Songlin Jia, Yuyan Bao, and Tiark Rompf, wrote a paper entitled “Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs,” which was accepted for POPL 2024.
Ryan Scott gave a talk at the 2023 GHC Contributors’ Workshop entitled “Getting Up, Running, and Contributing to GHC.” The talk was an introduction to working on GHC, including an overview of the structure of the code and the compilation pipeline; instructions for building it from source; and a description of using and configuring the build system, and efficiently working on projects.
Galwegians Ryan Scott and Mike Dodds, together with co-authors Ivan Perez, Alwyn Goodloe, and Rob Dockins presented a paper entitled “Trustworthy Runtime Verification via Bisimulation (Experience Report)” at ICFP 2023.
Galwegian David Darais, together with co-authors Matías Toro, Chike Abuah, Joseph P. Near, Damián Árquez, Federico Olmedo, Éric Tanter, published a paper entitled “Contextual Linear Types for Differential Privacy” in ACM Transactions on Programming Languages and Systems.
Galwegians Eric Mertens and David Archer, together with co-authors Paul Cuddihy, Daniel Russell, Kit Siu, and Jenny Williams, presented an article entitled “Aviation Certification Powered by the Semantic Web Stack” at ISWC 2023, winning the “Best Paper in Track” award.
Additional SSA Thought Leadership and Blogs
- “The Impact of Provable Security: AWS and Supranational” by Mike Dodds
- “Cryptol, SAW, and the Galois Origin Story” by Andrew Shaughnessy
- “Proof Assistance and Repair in Crux” by Ryan Scott and Arjun Viswanathan
- “Making a scalable, SMT-based machine code memory model” by Ryan Scott and Brett Boston
Cryptography and Privacy
Galwegians David Archer, Ben Selfridge, and Daniel Wagner, together with co-authors Robin Geelan, Michiel Van Beirendonck, Hilder V. L. Pereira, Brian Huffman, Tynan McAuley, Georgios D. Dimou, and Ingrid Verbauwhede, published a paper entitled “BASALISC: Programmable Hardware Accelerator for BGV Fully Homomorphic Encryption” in IACR Transactions on Cryptographic Hardware and Embedded Systems.
Galwegians David Archer, Eric Mertens, Kevin Quick, and Valentin Robert, together with co-authors Abha Moitra, Paul Cuddihy, Kit Siu, Daniel Russell, and Baoluo Meng, presented an article entitled “RACK: A Semantic Model and Triplestore for Curation of Assurance Case Evidence” at SAFECOMP Workshops 2023.
David Archer published an article entitled “Using and Sharing Sensitive Data Securely – Fact or Miracle?” in U.S. Cybersecurity Magazine, Fall 2023. Also, his submission to GOMacTech’24 was accepted for publication and will appear at the March 2024 Conference.
Galwegians Santiago Cuéllar, James Parker, and Stuart Pernsteiner, along with co-authors Bill Harris and Eran Tromer, presented a paper entitled “Cheesecloth: Zero-Knowledge Proofs of Real World Vulnerabilities” at Usenix Security 2023.
David Archer gave an invited talk entitled “Privacy Enhancing Technologies for Official Statistics” at the 54th session of the United Nations Statistical Commission. He also gave an untitled invited talk at GOMACTech 2023, an invited lecture on privacy enhancing technologies at Bilgi University in Istanbul, Turkey, and was an invited subject matter expert for the National Center for Science and Engineering Statistics effort to understand privacy-enhancing technologies for the newly planned National Secure Data Service.
James Parker and Kimberlee Model gave a talk entitled “SIEVE Circuit IR Specification” at ZKProof 5.5 in Barcelona, Spain. James also gave a talk entitled “ZKPs for Trust in Software and Hardwar” at ZKProof Policy @ DC.
Galwegians Ian Sweet and David Darais, together with co-authors David Heath, William Harris, Ryan Estes, and Michael Hicks published a paper entitled “Symphony: Expressive Secure Multiparty Computation with Coordination” in The Art, Science, and Engineering of Programming.
Darais, together with co-author Joseph Near, also published “SP 800-226: Guidelines for Evaluating Differential Privacy Guarantees,” a special publication for the National Institute of Standards and Technology (NIST).
Additional Cryptography & Privacy Thought Leadership and Blogs
- “Securing Software Supply Chains with Zero Knowledge Proofs” by James Parker
Rigorous Digital Engineering (RDE)
Danielle Stewart presented the GUMBO Contract Language to the AADL Committee to continue to foster collaboration and standards. We developed this contract language on our US Army GUMBO program. GCL is implemented as an AADL annex language extension.
Todd Carpenter gave an invited talk on Model-based High Assurance Development at the annual Trusted Computing Center of Excellence in May 2023. He discussed the maturity, usability, and capabilities of the model-based frontend and available analysis, automatic code generation, and formal verification of the resulting deployable system. Mr. Carpenter was the presenter. The team included Danielle Stewart, as well as John Hatcliff, Robby, and Jason Belt from Kansas State University.
Joe Kiniry gave an invited talk at the ERI Summit. Entitled “No Trade-off Necessary: Security, Performance, Ultra-Low Energy, and Assurance,” The article summarized Galois’ R&D on side channel-free ASIC development using Rigorous Digital Engineering for hardware in the 21CC project for DARPA. Finally, he gave the kickoff talk at the Dagstuhl Seminar 23041: Integrated Rigorous Analysis in Cyber-Physical Systems Engineering. Entitled “Reflections on Transition,” the talk covered Kiniry’s 20+ years of experience with industrial formal methods and transitioning concepts, tools, and technologies from the university to the field.
Galwegians Danielle Stewart and Todd Carpenter, together with co-authors John Hatcliff, Jason Belt, Robby, and Jacob Legg, published a paper that was accepted to the 2023 Formal Methods for Industrial Critical Systems (FMICS) Conference. “Automated Property-based Testing from AADL Component Contracts” presents the GUMBOX property-based testing framework, where automated testing infrastructure for AADL component application code is automatically generated from AADL models and formal specifications written in the GUMBO Contract Language. It allows developers to switch between using testing and formal verification with specifications derived from the GCL.
At the High Confidence Software and Systems (HCSS) 2023 Conference, “Semantically Rigorous and Integrated High-Level Abstractions,” Todd Carpenter and Danielle Stewart took part in a talk about the High-Assurance Model-based Rapid engineering for embedded systems. The talk focused on the rule-based operational semantics formalization of key aspects of the AADL Run-time Services that we use as a reference architecture to guide code generation for the software infrastructure.
Joe Kiniry gave two invited talks at the HALDEN Workshop. The first, entitled, “From the Informal to the Formal: Refining English Descriptions into Formal Specifications,” was about Galois’ R&D on specifying systems at various levels of formality, refining from English to rigorous formal specifications, now with LLMs as co-pilots. The second, entitled “The Correct-by-Construction Future of Assurance,” explored the future of DI&C control/protection systems with high-assurance for nuclear power plants.
Additional RDE Thought Leadership and Blogs
- “Digital Engineering: Changing the Paradigm” by Aaron Miller
- “U.S. Government Programs Need Authoritative Sources of Truth Aligned with Multi-organization Workflows” by Tyler Smith
- “Digital Engineering: From Point Solutions to Trusted Processes” by Matt Bauer
- “Can We Digitally Engineer Expertise for the Masses?” by Shauna Sweet
- “Digitally Engineering Infinite Patient Trials” by Taisa Kushner
- “Digital Engineering – CPS Behavior Modeling and Beyond” by Aditya Zutshi
- “Vehicle E/E Architectures – The Last Ten Years and the Future” by Aditya Zutshi
AI, Machine Learning, and Data Science
Galwegian Ethan Lew, along with co-authors Abdelrahman Hekal, Kostiantyn Potomkin, Niklas Kochdumper, Brandon Hencey, Stanley Bak, and Sergiy Bogomolov, presented a paper entitled “AutoKoopman: A Toolbox for Automated System Identification via Koopman Operator Linearization” at the 2023 International Symposium on Automated Technology for Verification and Analysis (ATVA). AutoKoopman is a python library for learning Koopman operators for data-driven dynamical systems analysis and control, automatically searching for the best Koopman observables and hyperparameter values.
Galwegians Alexander Grushin and Walt Woods, together with co-authors Alvaro Velasquez and Simon Khan, presented a paper entitled “Safety Margins for Reinforcement Learning” at the 2023 IEEE Conference on Artificial Intelligence. This paper presents a method for automatically and accurately computing a safety margin, which is defined (roughly) as the number of mistakes that an autonomous agent can afford to make in a given situation, before consequences are sufficiently severe.
Sourya Dey and Eric Davis presented a paper entitled DLKoopman: A Deep Learning Software Package for Koopman Theory at the 5th Annual Learning for Dynamics & Control Conference (L4DC). In the paper, Dey and Davis introduced an open-source software package for Koopman theory that uses deep learning to model nonlinear systems.
Sourya Dey gave an invited talk entitled “DLKoopman: A Deep Learning Software Package for Koopman Theory” at the Workshop on Symbiotic AI for Robust Digital Engineering. DLKoopman is an open-source software package for Koopman theory that uses deep learning to model nonlinear systems.
Eric Davis, Sourya Dey, Adam Karvonen, Ethan Lew, Donya Quick, Panchapakesan Shyamshankar, Ted Hille, and Matt LeBeau co-authored a paper entitled “Leveraging Manifold Learning and Relationship Equity Management for Symbiotic Explainable Artificial Intelligence,” which was presented by Davis at the 14th International Conference on Applied Human Factors and Ergonomics (AHFE).
Additional AI/ML/DS Thought Leadership and Blogs
- “Generative AI, Mission Critical Systems, and the Tightrope of Trust” by Walt Woods and Shauna Sweet
- “The Promise of AGI and Neuroscience, or ‘Hold your Horses’” by Katrina Schleisman
- “‘I’m a Good Bing’: Large Language Model Capabilities and Current Research” Tech Talk video (with transcription) by Shauna Sweet
- “Confabulators, Persuaders, and Imagination Catalysts: An Expert Perspective on the Chatbot Phenomenon” by David Burke
- “Broken Clocks and Generative Models: Human-Machine Trust Can Be Ephemeral” by Walt Woods
- “Language is a Noisy Measure” by Shauna Sweet
- “Formal Methods + AI: Where Does Galois Fit In?” by Taisa Kushner
- “Harnessing Deep Learning to Model Complex Systems” by Sourya Dey
- “Ontology, AI, and Human-Machine Teaming: How Does a Machine Know What We Mean?” by Joey Bingham
- “Applying GPT-4 to SAW Formal Verification” by Adam Karvonen
- “Using GPT-4 to Assist in C to Rust Translation” by Adam Karvonen
- “Using AI to Combat Illegal Fishing” by Eric Davis
- “Machine Learning and Analytics for Port Security” by Andrew Lauziere
Miscellaneous Blogs and Publications
- “Shaping Tomorrow’s Innovators” by Andrew Shaughnessy
- “Spinning Out, Creating Impact” by Rob Wiltbank
- “Spinout Stories: MuseDev” by Matt Bauer
- “Galois Engineer Fosters Future Tech Talent with LEGO Robotic Competition” by Andrew Shaughnessy
- “Building Connection in a Distributed Environment” by Marios Georgiou
- “Galwegians Reach a 20 Year Milestone!” – Q&A with Jef Bell and Mark Tullsen
- “Joy at Work: How Galwegians Chart Their Professional Destinies” by Anne Marie McClaran
- “The Galois Internship Experience: Mason Read”
- “Galois Game Jam 2023: A Creative Collision of Minds, Technology, and Pixels”
- “The Galois Internship Experience: Himanshu Goyal”
- “Haskell and Hacking” by Ryan Scott
- “Galois Celebrates New Office in Minneapolis”
- “Galois is now 100% Employee Owned! Here’s What That Means” by Dan Boyer
Community Involvement: Committees, Boards, Panels, Seminars, and Workshops
Danielle Stewart was on the program committee for the Application of Formal Methods and Digital Twins Workshop (FMDT) 2023 and reviewed three papers for the Journal of Computer Languages. In addition, Danielle Stewart (Galois) and John Hatcliff (KSU) were co-organizers along with Stefan Hallerstede (Aarhus University – Denmark) and Erika Abraham (RWTH Aachen University, Germany) of a week-long Dagstuhl seminar entitled “Integrated Rigorous Analysis in Cyber-Physical Systems Engineering.” The Dagstuhl seminar brought together 42 researchers and industrial representatives in CPS and formal methods from around the world to assess the state of the art, identify gaps in current CPS/formal methods capabilities, and formulate research plans to address community challenges.
Ryan Scott served as the program chair for the 2023 Haskell Implementors’ Workshop.
Todd Carpenter was a member of the program committee for the 2023 September seL4 Summit held in Minneapolis MN. He also served as the discussion moderator for the panel, OS on seL4: So Many Options!, at the Summit. The discussion covered capabilities, maturity, and benefits of several different operating systems running on seL4. The discussion highlighted the maturity of the seL4 ecosystem.
Ethan Lew served on the repeatability evaluation program committee at HSCC 2023.
David Darias was chosen to serve on program committees for OOPSLA 2024 and PLDI 2024.
Mike Dodds was chosen to serve on program committees for ESOP 2024 and FTfJP 2024.
Eddy Westbrook was chosen to serve on the program committee for NASA Formal Methods 2024.
David Archer serves on the Board of Directors of Niobium Microsystems, on the Cryptography Advisory Board of Callisto Project, and continues as a member of the United Nations Privacy Preserving Technology Task Team. He also serves as one of seven judges nationwide on the U.S. Privacy Enhancing Technologies Prize Challenge created by the White House and sponsored by NIST.
David Archer served as a co-editor for the new UN Handbook on Privacy-Preserving Computation Techniques.
Sourya Dey served as a reviewer for an article entitled “Efficient IOT-Based Mobile Edge Computing Network Using Transfer Learning Algorithm” in the Springer Nature Computer Science (SNCS) Journal.
As we reflect on the successes of the past year, we’re looking forward to the adventures that lie ahead. Scientific research is, for us, a source of enormous joy and satisfaction – an avenue for us to harness the potential of technology to solve some of the world’s most pressing challenges. It’s humbling to look back and see the progress we’ve made in a year, and exciting to imagine what’s next!