2022 wasn’t a return to pre-pandemic times, but we’ll call it a “return to almost-normal.” At Galois, we continued a hybrid model of in-person and virtual collaboration. We also added several members to our team, including the acquisition of Adventium Labs! (More on that below.)
Throughout the year, we made considerable progress applying our efforts in formal methods, high-assurance cryptography, machine learning, and data science into new applications and use cases. There has been genuine progress in all of these areas with regards to what is now possible and practical. A lot of this comes together in our rigorous digital engineering work, and we’re excited to announce upcoming projects in that area in the next few months.
Below are pointers and references to the highlights of our year. A sincere thank you to the partners, customers, and teammates who helped advance this work.
We wish you all a fulfilling 2023!
Adventium Acquisition
In September 2022, Galois acquired Adventium Labs, which develops innovative solutions for building safe and secure software-intensive complex systems. Adventium “shares Galois’s DNA when it comes to applying deep research, delighting our clients, and collaborating as a true community,” said Dr. Rob Wiltbank, CEO of Galois. “It feels like we’re joining a long lost sibling: so much of what we do and how we do it is complementary,” added Kyle Nelson, CEO of Adventium.
The different but complementary approaches of the two companies is beneficial to our customers. Galois’s focus on formal methods at the code level ensures that individual components of a system are trustworthy, while Adventium’s focus on higher-level aspects such as architecture and design helps to ensure that the overall system is safe and secure. Together, these dual approaches cultivate a more holistic trust and security ecosystem for critical systems.
Adventium operated as a wholly owned subsidiary of Galois until the end of 2022, and is now fully integrated into Galois.
Experience Our Cyber-Resilient Car For Yourself
Dr. Michal Podhradsky and Ethan Lew reported some cool news about our BESSPIN cyber-physical demonstrator. Visitors to the National Cryptographic Museum can now interact with the “quirky little car” whose hardware can thwart automobile-focused cyber attacks. The demonstrator showcases the use of DARPA’s SSITH secure hardware technology in a passenger vehicle.
Visitors to the museum can experience both the process of hacking and the experience of being hacked for an unprotected and secure car. By the end of the demonstration, visitors will have a better understanding of the dangers of driving a vulnerable car and the importance of protecting their vehicles with secure hardware.
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.
Autonomous Driving For the Win
Continuing the car theme, Ethan Lew and Dr. Aditya Zutshi wrote a blog post about placing first in the GRAIC (Generalized RAcing Intelligence Competition) hosted at CPS-IoT week. Autonomous vehicles are prime examples of complex systems which operate in uncertain and unstructured environments.
They developed a racing strategy that would serve as a good case study for our Cyber Physical Systems (CPS) assurance research, focusing on Explainable Decision Making and Automated Scenario Testing. GRAIC is ideal for both of these topics because of the GRAIC simulator, which provides a Perception Oracle that would eliminate the need to process raw sensor data and enable us to focus on decision-making and control. Given the simulator’s Perception Oracle, the Galois team’s control architecture uses road boundary and obstacle motion predictors to inform our top-level control, path planner, and steering and throttle/brake controller.
The code is available here. It’s also reimplemented in Rust for improved performance – this faster version of the program is able to find an even better path in the same time window.
CRYPTOL Overview for Non-Scientists
One of the major goals of our blog is to create content for several audiences, including non-scientists. We specifically created a blog post about Cryptol, one of flagship cryptography tools, for our non-scientist audience. We discuss Cryptol’s history, its current capabilities, and how this versatile tool is positioned to help organizations in a post-quantum computing world.
The Galois Blog
Speaking of our blog, we wrote 18 informative articles throughout the year. Subjects included software tutorials and demos; asynchronous hardware design; and cyber-physical systems, among many other topics.
Galois in the Community
Dr. Mike Dodds’s article, Formally Verifying Industry Cryptography, was published in the May/June 2022 issue of the journal IEEE Security & Privacy. The article explained Galois’s approach to these formally verifying cryptographic systems, focusing on the practical engineering challenges that exist when building and deploying proofs in industry.
Portland State University invited Ethan Lew to speak on the subject of, “Dynamical System Reachability, Conformance, and Control via Koopman Linearization,” on September 13, 2022. This was PSU’s first workshop on learning nonparametric differential equations from data.
Tyler Smith, John Shackleton, and Charles Payne’s article, Constructing an Authoritative Source of Truth in a Changing Information Landscape, appeared April 12, 2022 in INCOSE Insight Magazine. The article discussed the nature of an Authoritative Source of Truth and its role in digital engineering.
Spin-Out News: Tozny
Galois Spin-out Tozny merged with OneID Lab to form Tozny, Inc. Tozny is an identity management and data security company, and OneIDLab is a zero-trust posture security technology company. The merger combines Tozny’s integrated Identity and Access Management (IdAM), Privileged Access Management (PAM), Key Management, and Data Encryption Solutions with OneIDLab’s Secure Remote Access and advanced decentralized identity token solutions.
Both Tozny and OneIDLab products have benefited from deeply rooted engagements with government organizations like the Department of Defense, Department of Homeland Security, the National Institutes of Health, and many other federal agencies. Tozny is headquartered in Camas, Washington, with offices in Portland, Oregon.
Below, see links to our software releases, papers, workshops, and other public presentations we made throughout 2022.
Zero-Knowledge Proofs and High-Assurance Cryptography
Dr. Mike Dodds gave a talk, Formally Verifying Everyone’s Cryptography, at Strange Loop in September 2022. He discussed how recent advances have made formal verification a cost-effective assurance tool for real-world cryptographic systems. Dr. Joey Dodds co-presented at the talk.
Dr. Marios Georgiou and Dr. Alex J. Malozemoff presented a paper, “Security Foundations for Application-Based Covert Communication Channels,” at the IEEE Symposium on Security and Privacy in May 2022. They discussed security formalisms for censorship circumvention systems based on tunneling covert data through existing applications. Also part of the team: James K. Howes IV and Thomas Shrimpton.
Dr. Marios Georgiou, Ben Hamlin, and Dr. Alex J. Malozemoff presented a paper, “Towards a Formal Treatment of Logic Locking,” at CHES: Workshop on Cryptographic Hardware and Embedded Systems in September 2022. They discussed cryptographic formalisms for logic locking, and showing how to satisfy these formalisms using universal circuits. Also part of the team: Peter Beerel and Pierluigi Nuzzo.
Dr. Alex J. Malozemoff, Dr. David Archer, and James Parker gave a talk – FROMAGER – A Scalable Toolchain for Complex ZK Proofs About Software – at ZKProof, in November 2022. Their talk focused on proving software vulnerabilities in zero-knowledge and our backend implementation of the fastest interactive zero-knowledge proof protocol. FROMAGER is part of DARPA’s SIEVE program.
Dr. James Parker gave a talk on Galois’s cutting-edge work involving zero-knowledge proofs at GE Edge Symposium in October 2022.
Dr. William Harris’s paper, “Proving UNSAT in Zero Knowledge,” at 2022’s Computer and Communications Security Conference (CCS) in November 2022. The paper received the “Distinguished Paper Award” from CCS. Also part of the team: Ning Luo, Timos Antonopoulos, Ruzica Piskac, Eran Tromer, and Xiao Wang.
Rigorous Digital Engineering
Tyler Smith gave a keynote speech, From Documentation to Discovery: Fostering Insight in Digital Engineering, at the Dayton Digital Transformation Summit on August 1, 2022. In the speech he described a vision for digital engineering in which tools and methods help everyone make better decisions. You can read a recap of the summit here.
Tyler Smith, together with Alfred Schenker and William Nichols (both from Carnegie Mellon University Software Engineering Institute), shared their paper, “Measuring Digital Engineering Effectiveness for Embedded Computing Systems,” at the Naval Postgraduate School Acquisition Research Symposium on June 1, 2022. The paper discussed a review of recent Army Science and Technology embedded computing systems research through the lens of effectiveness measurement.
Software Correctness and Formal Methods
Todd Carpenter and Dr. Danielle Stewart took part in a talk, Model-Based Information Flow Specification and Management for seL4, at the Trusted Computing Center of Excellence in February 2022. They discussed how to specify flows within a modeling environment and various analysis techniques to ensure that security properties are maintained. Mr. Carpenter was the presenter, and the team included Dr. John Hatcliff and Dr. Robby (both from Kansas State University).
Todd Carpenter and Dr. Danielle Stewart took part in a talk, Integrated Formal Verification Environment for seL4 Applications, at the Trusted Computing Center of Excellence in February 2022. They discussed an overview of the Logika program verifier and how it enables usable formal methods. Dr. Robby was the presenter, and Dr. John Hatcliff was also part of the team.
Todd Carpenter and Dr. Danielle Stewart took part in a talk, Model-Based Code Generation for seL4, at the Trusted Computing Center of Excellence in February 2022. They discussed an overview of the HAMR toolset for code-generation and the GUMBO Contract Language extension for code-level verification. Dr. John Hatcliff was the presenter, and Dr. Robby was also part of the team.
Dr. Mike Dodds took part in a mentoring workshop, Formal Methods: Theory and Practice, at 27th ACM SIGPLAN International Conference on Functional Programming (ICFP 2022) in September 2022.
Dr. James Parker co-authored a paper, “Understanding the How and the Why: Exploring Secure Development Practices through a Course Competition,” at the Computer and Communications Security Conference (CCS) in November 2022. The paper concerned the results of in-depth study of 14 teams’s development processes during a three-week undergraduate course organized around a secure coding competition. The paper’s co-authors are: Kelsey Fulton, Daniel Votipka, Desiree Abrokwa, Michelle Mazurek, and Michael Hicks.
Dr. Stuart Pernsteiner gave a talk on Compositional Verification with crux-mir, a Crucible-based testing tool for Rust programs at the Rust Formal Methods Interest Group on May 30, 2022.
Dr. Tristan Ravitch and Ryan Scott participated in the Competition on Software Verification (SV-COMP) with Crux, Galois’s verification tool, in early 2022. This was the first time Galois participated in the competition. Also part of the team: Aaron Tomb and Robert Dockins.
Dr. Danielle Stewart co-authored a paper, “Formalization of the AADL Run-Time Services.” Dr. John Hatcliff presented it at ISOLA 22 in October 2022. The paper described the formalization of the Architecture Analysis and Design Language run-time services and thread behaviors. Also part of the team: Jerome Hugues and Lutz Wrage.
Dr. Danielle Stewart and Dr. August Schwerdfeger co-authored a paper, “An AADL Contract Language Supporting Integrated Model- and Code-Level Verification.” Dr. John Hatcliff gave a presentation on the paper at HILT ‘22 in October 2022. The presentation described the GUMBO Contract Language (GCL) which is specified in the model and translated into code-level contracts using HAMR; verification was performed by Logika, ensuring the application code meets the model-level specifications. Also part of the team: Dr. Robby and Jason Belt.
Dr. Danielle Stewart co-authored a paper – “Mechanization of a Large DSML: an Experiment with AADL and Coq.” Jerome Hughes gave a presentation on the paper at MEMOCODE 22 in October 2022. The paper described the Coq specification of AADL static and dynamic models to provide a foundation for rich analysis capabilities. Also part of the team: Dr. John Hatcliff and Lutz Wrage.
Dr. Mark Tullsen co-authored a paper, “Strengthening Weak Links in the PDF Trust Chain,” at The Eighth Workshop on Language-Theoretic Security (LangSec 2022) at IEEE Symposium on Security and Privacy in May 2022. Also part of the team: Dr. William Harris and Peter Wyatt.
Data Science
Sam Cowger, Dr. Eric Davis, Dr. Sourya Dey, Matt LeBeau, Ethan Lew, Dr. Panchapakesan Shyamshankar, and Ted Hille gave a workshop – ORCA: Orchestrating Symbiotic Intelligence for Agile and Adaptable, Crisis Response Decision Making – at Chesapeake Large-Scale Analytics Conference (CLSAC ‘22) in October 2022. The workshop discussed surrogate modeling for mixed HPC and edge computing workloads due to mission requirements and resource restrictions.
Dr. David Darais co-authored a paper, “Solo: a Lightweight Static Analysis for Differential Privacy,” and presented it at OOPSLA 2022 in October 2022. He discussed a new approach to static program analysis for differential privacy that can be enforced using the type system of functional programming languages like Haskell. Also part of the team: Chike Abuah and Joseph P. Near (both from the University of Vermont).
Dr. Olivier Savary Belanger, Dr. Scott Moore, and Dr. Jennifer Paykin delivered an extended abstract and Dr. Moore gave a presentation describing their work on SEEC (part of DARPA’s AIMEE program) at Principles of Secure Compilation (PriSec 2022) in January 2022.
Dr. James Parker co-authored a paper, “ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification,” and presented it at PLDI 22. He discussed a method to ensure that programs only answer safe queries that do not reveal too much about private information. Dr. Parker also gave a rundown of the paper’s premise on Galois’s blog. The paper’s co-authors are Sankha Guria, Niki Vazou, and Marco Guarnieri.
Cyber-Physical Systems
Todd Carpenter served as the discussion moderator for the panel, Gaps and Needs, at the Trusted Computing Center of Excellence in February 2022. The discussion identified gaps and needs within cyber-physical systems engineering and safe and secure computations.
Dr. Danielle Stewart serves on the Dagstuhl 2023 Organizing Committee for Integrated Rigorous Analysis in Cyber-Physical Systems Engineering, a workshop focused on bringing industry and academia together to discuss open problems in cyber-physical systems engineering. The workshop will occur in January 2023.
Machine Learning
Dr. Sourya Dey and Dr. Walt Woods gave a presentation, LAGOON: an Analysis Tool for Open Source Communities, at the Mining Software Repositories (MSR 2022) in May 2022. They discussed how LAGOON is an open source platform for understanding the complex ecosystems of Open Source Software (OSS) communities. You can watch a short video about LAGOON here.
Dr. Sourya Dey submitted a paper, “DLKoopman: A Deep Learning Software Package for Koopman Theory,” to the 2023 Learning for Dynamics & Control Conference (L4DC). The paper describes the DLKoopman software package to implement Koopman theory using deep learning.
Dr. Alexander Grushin and Dr. Walt Woods gave a presentation, Anomaly Detection with Neural Parsers That Never Reject, for The Eighth Workshop on Language-Theoretic Security (LangSec 2022) at IEEE Symposium on Security and Privacy in May 2022.
Ethan Lew co-authored a paper, Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement. The paper was accepted at the 34th International Conference on Computer Aided Verification. Also part of the team: Stanley Bak, Sergiy Bogomolov, Brandon Hencey, Niklas Kochdumper, and Kostiantyn Potomkin.
Ryan Peroutka gave a talk, FRIGATE: Uniting Hierarchical Planning and Model-Based Systems Engineering to Automate Failure Recovery Planning, at the AAAI 2022 Fall Symposium in November 2022. FRIGATE is a NASA-funded tool for automated failure recovery plan generation and verification.
Contract Award Announcements
Discovering and Explaining Threats of Emergent Computation to enable Transformations (DETECT) will help programmers discover vulnerabilities within a system’s design. As part of DARPA’s HARDEN program, DETECT builds upon SEEC, a Galois project that was part of DARPA’s AIMEE program.
TRIFECTA achieves a stronger combination of utility preservation and privacy protection than data anonymization techniques, while also providing similar support for general public sharing of sensitive data. DoE SBIR Phase 1 Award.
Software Releases
CAMET: We released CAMET Base Pack 1.4 in November 2022.
CRUX: We released version 0.6 in June 2022.
Cryptol: We released version 2.13 in June 2022.
DLKoopman: We released this Python package to implement Koopman theory using deep learning in November 2022.
Other Community Engagements
Dr. Mike Dodds:
– Served on the program committee for PLDI 2022: Programming Languages, Design and Implementation, a top-tier publication venue in programming languages.
– Serves on the program committee for ESOP: European Symposium on Programming.
– Served on the program committee for the ACM International Conference on Hybrid Systems: Computation and Control (HSCC ‘22).
Dr. John Launchbury:
– Served as a NSA cybersecurity distinguished expert, advising NSA on their annual Best Scientific Cybersecurity Research Paper Competition held in July 2022.
– Served as a Member of the National Academies Forum on Cyber Resilience, an independent and trusted venue in which experts from industry, academia, and government work collaboratively to explore emerging critical challenges related to the security, trustworthiness, and resilience of the nation’s computing, communications systems, and critical infrastructures.
– Served on the steering committee for the High Confidence Software and Systems Conference, s world class community of researchers who focus on new scientific and technological foundations that can enable entirely new generations of engineered designs.
Dr. Alex J. Malozemoff:
– Served on the program committee for CRYPTO 2022.
– Served as an external reviewer for the National Science Foundation’s Secure and Trustworthy Cyberspace program.
Dr. Scott Moore:
– Served on the program committee for The Eighth Workshop on Language-Theoretic Security (LangSec 2022) at IEEE Symposium on Security and Privacy.
– Served on the program committee for Principles of Secure Compilation (PriSC 2022).
Dr. Danielle Stewart:
– Served on the program committee for FMDT (Formal Methods Digital twins), which aims to find common ground between industrial needs for model-based engineering of digital twins and formal methods.