Abstract: We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust’s rich region-based type system to eliminate memory reasoning for a large class of Rust programs by translating them to a pure lambda-calculus, as long as they do not rely on interior mutability or unsafe code. Doing […]

There has been a lot of chatter recently about large language models, including GPT-4 and LLaMa. At Galois, we have been experimenting with GPT-4, the most capable available large language model. One group of intriguing results that I am excited to present is in the creation of SAWScript memory safety proofs. Using a very simple […]

Abstract: In this talk we give an introduction to Mirrorsolve, a Coq library for solving Coq proofs using SMT solvers. Foundational theorem provers such as Isabelle/HOL and Coq are the gold standard for building certified systems, enabling the verification of extremely rich properties while having a minimal trusted code base. Unfortunately, these provers come with […]

Abstract: We will give a general introduction to Gillian, a platform for the development of symbolic-execution tools for many programming languages.  Gillian currently supports three types of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. It uses a core symbolic execution engine with strong mathematical foundations […]

Abstract: Advances in deep neural networks (DNNs) have increased their deployment in safety-critical systems, such as vision perception modules for autonomous vehicles and airborne collision avoidance system controllers for unmanned aircraft. Modern DNNs and linear classifiers are susceptible to adversarial input perturbations. Adversarial perturbations are small changes to an input that result in unexpected changes […]

What does long-term success look like for a verification tool like SAW? For us, it involves improving the quality, correctness, and security of as much code as possible. We know that the best way to get there is not Galois hoarding all of the proofs and proof skills and keeping you all out. We love […]

We are happy to announce the first formal release of Crux, a new open-source verification tool from Galois. This new tool aims to improve software assurance using symbolic testing, a technique that allows for smooth migration from testing to verification. Crux builds on the same infrastructure as our Software Analysis Workbench (SAW), but with a […]

I’m happy to share something new the Galois cryptography verification team is working on in collaboration with the Ethereum Foundation, Protocol Labs, and Supranational. However, I’m sorry to inform you that Galois has sold out to dramatic live-blogging. We’ve sold out so much that I, unrequested by anyone, took the liberty of making us a […]

Machine learning has revolutionized cyber-physical systems (CPS) in multiple industries – in the air, on land, and in the deep sea.  And yet, verifying and assuring the safety of advanced machine learning is difficult because of the following reasons:  State-Space Explosion: Autonomous systems are characteristically adaptive, intelligent, and/or may incorporate learning capabilities.  Unpredictable Environments: The […]

At Galois, we develop formal verification tools that rely on a variety of automated solvers for answering mathematical queries. The main solvers we use are called Satisfiability Modulo Theories (SMT) solvers.  These solvers offer the ability to answer questions such as “find me inputs for which a mathematical property holds.”  We have found these tools […]