Abstract: For over a decade, a buffer overflow vulnerability in the “official” SHA-3 implementation by its designers remained unnoticed. This vulnerability was assigned CVE-2022-37454 and impacted several projects such as Python and PHP that relied on this implementation. We provide a proof of concept for arbitrary code execution and explain how we found the vulnerability […]

Back in 2015, Galois Chief Scientist and Founder, John Launchbury, started developing and discussing “Three Waves of AI” as a framework for understanding the new burst of machine learning developments that were taking place, and to put DARPA I2O’s research portfolio into context. Now, eight years later, ChatGPT and friends have burst on the scene. In this […]

Abstract: When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of mathematics that deals with limits and the foundations of calculus. In a prior work, we used real analysis in the interactive theorem prover ACL2s […]

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 […]

Abstract: Data privacy laws like the EU’s GDPR grant users new rights, such as the right to request access to and deletion of their data. Manual compliance with these requests is error-prone and imposes costly burdens especially on smaller organizations, as non-compliance risks steep fines. K9db is a new, MySQL-compatible database that complies with privacy […]

Abstract: In robot controller design, we try to find controllers which satisfy our high-level intuitions for how they must behave, these notions are sometimes represented as specifications. In this talk, I will be exploring difficulties in defining such controllers when learning is involved. I will then walk through our journey in achieving performant and robust […]

Abstract: The typical software pipeline for processing a human DNA sequencing sample begins by mapping reads to a previously assembled single linear reference—that is, a collection of long strings of nucleotides approximating one genome. This permits determining variation in the sample with respect to the reference, including the single nucleotide variants (SNVs), insertions, and deletions […]

Abstract: Low-level, pointer-manipulating programs are tricky to write and devilishly hard to verify, requiring complex spatial program logics to reason about heap updates. Recent systems like Prusti and Creusot take advantage of Rust ownership mechanisms to shield the programmer from some spatial assertions, allowing them to only write pure, first-order logic specifications which can be […]

Abstract: Fully Homomorphic Encryption (FHE) is a scheme that allows a computational circuit to operate on encrypted data and produce a result that, when decrypted, yields the result of the unencrypted computation. While FHE enables privacy-preserving computation, it is extremely slow. However, the mathematical formulation of FHE supports a SIMD-like execution style, so recent work […]

Abstract: A key element of supply chain security is updates: how can we make sure software updates are secure? That one doesn’t risk running malicious software when updating software their system? For free system distributions, The Update Framework (TUF) has become a reference on these matters. However, TUF is designed with binary distributions in mind—think Debian or even PyPI—and is […]