Categories

2023: Year in Review

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.  

Milestones

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). 

Launching a New Company: We spun out our latest company, ExistX, which aims to bridge the gap between groundbreaking research and real-world applications.

Highlights

Throughout 2023, Galois has made significant strides across multiple (often-overlapping) research domains. Highlights include:

  • 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. 
  • Alexander Grushin and Walt Woods published a paper presenting a novel method for automatically and accurately computing a safety margin for reinforcement learning.

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

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

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

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). 

David Burke presented the keynote, entitled “Foresight, Imagination, and AI,” at IEEE NAECON 2023.

Additional AI/ML/DS Thought Leadership and Blogs

Miscellaneous Blogs and Publications

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.

Scott Moore was on the Program Committee for the 2023 LangSec Workshop and will be on the Program Committee for the 2024 IEEE Computer Security Foundations Symposium.


Oliver Bračevac was on program committees for ICFP 2023 and miniKanren 2023, as well as external review and artifact evaluation committees for OOPSLA 2023 and ECOOP 2023.

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.

Joe Kiniry served on the editorial boards for IEEE Security and Privacy and the new Cambridge University Press Journal, Research Directions: Cyber-Physical Systems.

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.   

Looking Forward

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!