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

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

Abstract: Multiparty garbling is the most popular approach for constant-round secure multiparty computation (MPC). Despite being the focus of significant research effort, instantiating prior approaches to multiparty garbling results in constant-round MPC that can not realistically accommodate large numbers of parties. In this work we present the first global-scale multiparty garbling protocol. The per-party communication […]

Abstract: Library authors often are faced with a design choice: should a function with preconditions be implemented as a partial function, or by returning a failure condition on incorrect use? Neither option is ideal. Partial functions lead to frustrating run-time errors. Failure conditions must be checked at the use-site, placing an unfair tax on the users who have ensured […]

Abstract: Since 2016, various members of Project Everest have been busy verifying layer after layer of critical software. We started with cryptographic primitives, moved on to high-level stateful APIs, followed by protocols, handshake state machines, and high-level defensive APIs complete with proofs of security in the Dolev-Yao symbolic model. In our most recent work, we […]

Abstract: This talk consists of two parts. In the first part of the talk I introduce the Message Passage Language (MPL), which is a statically typed concurrent programming language with message passing as the concurrency primitive. It brings communication safety to interacting processes using a type system. MPL consists of two languages, concurrent MPL and […]