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

Tech Talk: “Can we Prove Facts About Machine-Learning Models via Code synthesis?” by Samuel Gélineau

Monday, September 26, 2022

Abstract: We have a lot of tools (static analyzers, type systems, proof assistants, linters) for analysing and proving things about programs written as source code in traditional languages. However, we are currently poorly equipped to analyze and prove things about machine learning models, simply because the resulting programs are represented as a bunch of weights […]

Read More

Public Tech Talk: “Foundational and Automated Verification, Together at Last” by John Sarracino

Monday, August 29, 2022

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

Read More

Public Tech Talk: “hacspec – a specification language for crypto primitives and more” by Franziskus Kiefer

Monday, August 15, 2022

Abstract: An introduction and overview of hacspec, its design principles, and usage. Bio:   Franziskus is a security & cryptography engineer and researcher based in Berlin. He is co-founder of Cryspen, a company that builds custom high assurance cryptography. Franziskus holds a PhD in provable cryptography and was previously leading the security engineering efforts at Wire […]

Read More

Public Tech Talk: “Verifying the Ethics of Autonomous Systems” by Colin Shea-Blymyer

Monday, August 22, 2022

Abstract: Autonomous Intelligent Systems are often designed with complex, interacting objectives, or have learned behavior that is difficult to specify. This obfuscates the social and ethical rules of systems like self-driving vehicles and nursing robots in hospitals. Though their missions (e.g., go from point A to point B) are known, we need to determine their […]

Read More

Public Tech Talk: “Secure System Composition and Type Checking using Cryptographic Proofs” by Dani Barrack

Wednesday, July 20, 2022

Abstract: Formally verifying security properties and the functional correctness of systems involves comprehensive analyses of system compatibility and interoperability. Many conventional approaches require trusted systems in order to assure properties of transmitted data that are difficult to authenticate, or the undesirable exposure of additional data for the purpose of verification. We overcome this limitation by […]

Read More

Public Tech Talk: “Designing Data-Driven Yet Verifiably Safe Autonomous Medical Systems” by Taisa Kushner

Tuesday, July 12, 2022

Abstract: The exponential rise in data has spurred significant interest in developing personalized machine models for a seemingly infinite range of applications. However, in the case of safety critical systems such as autonomous medical systems, classical algorithms have failed due to complications spanning from limited data to the requirement that systems be explainable and verifiably […]

Read More