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

Scalable Multiparty Garbling

Wednesday, March 15, 2023

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

Read More

Ghosts of Departed Proofs

Thursday, February 02, 2023

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

Read More

Towards a Fully Verified Protocol Stack, from Cryptographic Primitives to State Machines

Thursday, December 01, 2022

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

Read More

Concurrent Programming with Typed Channels and an Introduction to the Value Decomposition Framework for Explainable Computing

Thursday, November 17, 2022

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

Read More