John Launchbury: The Trajectory of AI

Friday, December 01, 2023

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

Read More

Protocol Analysis Using Real Analysis in ACL2

Tuesday, November 21, 2023

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

Read More

Aeneas: Rust Verification by Functional Translation

Wednesday, October 18, 2023

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

Read More

K9db: Privacy-Compliant Storage For Web Applications By Construction

Monday, September 25, 2023

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

Read More

Achieving robustness in learned control

Friday, July 14, 2023

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

Read More

An invertible transform for efficient string matching in labeled directed graphs

Wednesday, June 21, 2023

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

Read More

Flux: Liquid Types for Rust

Wednesday, May 17, 2023

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

Read More

Coyote: A Compiler for Vectorizing Encrypted Arithmetic Circuits

Monday, April 17, 2023

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

Read More

Building a Secure Software Supply Chain with GNU Guix

Monday, April 24, 2023

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

Read More

Large Scale MPC

Wednesday, March 29, 2023

Abstract: Scaling secure computation to very large numbers of parties introduces multiple interesting challenges, most obviously in designing efficient protocols that scale, but also in how we model the network and reason about its guarantees. In this talk we will cover 3 recent results. In the honest (super-)majority setting, we present a protocol for which […]

Read More