Privacy Protecting Programming Languages

Privacy is important! My students and I have been exploring new language designs that make powerful privacy-preserving technologies like secure multiparty computation more accessible to programmers. One of our key innovations is oblivious algebra datatypes (OADTs), a novel datatype mechanism that combines ideas from dependent types and security type systems to statically ensure that programs do not leak information about sensitive data. Using OADTs, we have built a language in which users program mostly as normal, but also provide a policy describing the privacy requirements for any datatypes their program uses. The compiler then generates a provably secure implementation which uses cryptography to enforce the desired policy. This compiler is equipped with a variety of privacy-aware optimizations, in order to minimize the performance overhead of the underlying cryptographic protocols.

Representative Papers:

• Oblivious Algebraic Datatypes
• Taype: a Policy-Agnostic Language for Oblivious Computation
• Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation

Coverage Types

Random input generators play an important role in automated testing and data-driven program analyses. Typically input generators need to produce data satisfying some semantic properties: in Property Based Testing frameworks, for example, they are used to construst inputs meeting the precondition of a function under test. To be effective, generators must be able to efficiently produce a variety of valid inputs; in many cases, this means that developers have to write a generator by hand, and then rely on manual inspection and post-mortem analysis of test runs to evaluate its effectiveness. The goal of this project is to develop principled approaches for automatically verifying and synthesizing input generators. Our secret sauce is Coverage Types, a form of refinement types that reason about the completeness of nondeterministic programs, i.e., the range of inputs that it must be capable of producing.

Representative Papers:

• Covering All the Bases: Type-based Verification of Test Input Generators
• A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata

Data-Driven Abductive Verification

Verification-aware programming languages allow users to annotate a program with information about its desired behaviors and then automatically check that the program satisfies its specification at compile time. Unfortunately, the amount of annotations required grows with both the complexity of the program and the richness of the properties being checked. The goal of this project is to automatically infer these annotations for users, so that programmers only need to manually supply the key, system-level properties of their programs. In order to provide rigorous, best-effort guarantees about program behaviors in the face of incomplete information, we use a novel form of abduction, a logical proof principle that seeks to find explanatory hypotheses sufficient to validate a logical statement. In order to compensate for missing specifications, our abductive reasoning engine relies on observations, gleaned from program executions, to drive machine learning methods that inform the search for plausible explanations of program behaviors.

Representative Papers:

• Data-Driven Abductive Inference of Library Specifications

Program Synthesis in an Interactive Proof Assistant

The goal of program synthesis is to automatically generate the implementation of a program from a high-level specification of its behavior. Fiat is a deductive synthesis framework for the Coq proof assistant that combines foundational ideas from programming language and formal methods to build an automated refinement system from first principles that produces correct-by-construction sofware with a minimal trusted code base. Starting from high-level specifications in Coq's rich logic, Fiat helps users interactively construct an executable implementation. Every step in the process is justified by a machine-checked refinement proof which, when composed together, certifies that the derived implementation meets the original specification. The framework provides libraries of domain-specific specification languages and reusable refinement tactics for guiding the search for an implementation, leveraging Coq's powerful Ltac metaprogramming language to achieve a high degree of automation. Each refinement step is certified by Coq, allowing users to freely incorporate their own implementation strategies into a derivation without compromising the guarantees of its correctness.

Representative Papers:

• Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
• The End of History? Using a Proof Assistant to Replace Language Design with Library Design
• Using Coq to Write Fast and Correct Haskell

Synthesis of Communication Code from Binary Formats

The code responsible for encoding and parsing external data is a vital component of any software that communicates with the outside world: failure to produce or correctly interpret encoded data that conform to a standard format can result in lost or corrupted data, while bugs in the decoder code that takes untrusted external data as input represents a key attack surface for malicious actors. Writing code that conforms to a high-level format description by hand is both tedious and error-prone. This project seeks to eliminate both the tedium and the potential for error in building binary encoders and decoders via a framework, called Narcissus, that allows users to express a format as a binary relation that precisely captures all the valid binary encodings of an arbitrary datatype instance. From this specification, Narcissus synthesizes a decoder that is guaranteed to both be the inverse of this relation and to detect malformed encodings by failing on any inputs not included in this relation. Narcissus produces a proof trail certifying the correctness of the synthesized decoder. Using Narcissus, we have synthesized replacement decoders for all packet formats used in the standard network stack of the MirageOS unikernel.

Representative Papers:

• Deriving Correct-By-Construction Decoders and Encoders from Binary Formats with Narcissus
• A Verified Protocol Buffer Compiler

Modular and Extensible Programming Language Metatheory

Static program analyses are an important tool for ensuring the absence of run-time errors. A faulty analysis is ofentimes worse than none at all, providing users with a false sense of security. This makes it particularly important that static analyses are sound, only validating programs that are actually error-free. Designers typically establish soundness via a mathematical meta-theory proof connecting the analysis to a formal description of a language's semantics. To ensure the correctness of these intricate proofs, researchers commonly mechanize them in computerized proof assistants. These mechanized proofs can be both tedious and labor-intensive, but this effort results in a foundational proof of the correctness of the analysis, which is automatically conferred onto any analyzed program.

These mechanized proof developments are artifacts that, much like source code, can be adapted and extended with new features, enabling the development of variant languages. Unfortunately, the standard approach to language extension is essentially to copy the existing formalization, modify that copy, and then patch up the proofs. The effects of an extension can be woven throughout the meta-theory proofs of a language, making it difficult to both identify and apply the meta-theory changes required by a new feature. This project attempts to solve these challenges by developing sound and modular approaches to extend programming languages with new features, allowing programming language researchers to better leverage existing mechanized formalizations of languages, enabling innovation without compromising soundness.

Representative Papers:

• Meta-Theory a la Carte
• Modular Monadic Meta-Theory
• Product Lines of Theorems