Build-it, Break-it, Fix-it (BIBIFI) is a programming contest which aims to assess the ability to securely build software, not just break it. During the Build-it round, contestants implement software according to a provided specification with security goals. The software is scored for being correct, efficient, and featureful. The second round asks teams to find defects in other teams’ build-it submissions (Break-it) and patch the bugs and vulnerabilities found in their code (Fix-it). In addition to being an excellent learning opportunity for participants, the BIBIFI contest produces data that provides insights into secure development practices and software quality.

Programming in C and C++ is risky. Unlike modern languages, C/C++ programs do not enjoy spatial safety, an aspect of memory safety that is ensured when a pointer dereference is always within the memory allocated to that pointer. Buffer overruns—a spatial safety violation—still constitute one of the most frequent and pernicious sources of vulnerability, despite their long history and many attempts to eliminate them. We have been working with Microsoft on Checked C, an extension to C that aims to provide spatial memory safety.

For many modern software systems, constant availability is a key requirement. At the same time, such systems are often subject to frequent updates, including security patches and feature improvements. Applying such updates by stopping, patching, and restarting the system results in an unacceptable loss of availability. Dynamic Software Updating (DSU) is a general-purpose technique for patching stateful software without shutting it down, which enables both timely updates and non-stop service. Over nearly 20 years, we have been researching how to build practical, general-purpose DSU systems, which are safe, efficient, and easy to use. We have been exploring semantic foundations, analyses, and implementation techniques toward meeting this challenge in a variety of domains.

As the practice of formally verifying software in proof assistants increases in importance and popularity, the lack of proper support for large-scale proof engineering is becoming increasingly apparent. In particular, the productivity of proof engineers is lowered by inadequate interfaces, processes, and tool support, which lone expert users may not be hindered by, but become serious problems in large evolving projects with many contributors. Traditional software engineering practices fail to carry over in a unique setting that mixes formal requirements with rigorous mathematical proofs, and powerful reasoning capabilities with limited computational support. This project aims to increase the productivity of proof engineers by simplifying the process of developing, executing, and maintaining verified software in proof assistants, leveraging synthesis and testing based approaches to facilitate proof construction, extraction, and maintenance, as well as to establish the trustworthiness of proof checkers themselves.

An oblivious program is one that is free of direct and indirect information leaks, e.g., due to observable differences in the content, timing, or pattern of direct outputs, or even network messages and memory access patterns. The latter may be exploited when an attacker has physical access to the machine, or remote access to hardware traces (e.g. through a remotely exposed debug interface). Our approach uses type systems to ensure that all well-typed programs are oblivious.

For quantum computers to be useful, we need to provide software development tools for would-be quantum programmers. Our main project is the VOQC compiler, the first fully verified compiler for quantum programs. It takes programs written in a small quantum intermediate representation, SQIR, and both maps them to a specified architecture and aggressively optimizes them to use a minimal number of quantum gates. We also use SQIR to directly verify quantum programs, such as Quantum Phase Estimation or Deutsch-Jozsa, which we can then convert to IBM’s OpenQASM standard and execute on real world devices.

Liquid Haskell extends Haskell with a refinement type system. Refinement types add predicates to types, which allow users to specify properties about their code. Due to the Curry-Howard isomorphism, users can prove these properties are satisfied by writing programs as proof. In our research, we encode and verify security and correctness properties about Haskell programs using Liquid Haskell. For one project, we show that LWeb, a dynamic information flow control (IFC) framework for database-backed web applications, enjoys non-interference. In another project, we prove that replicated data types, which are used to build distributed applications, satisfy required mathematical properties to ensure strong convergence.

Software correctness is becoming an increasingly important concern as our society grows more and more reliant on computer systems, with even even the simplest of software errors having devastating financial or security implications. How can we find errors in real-world applications? How can we guarantee that such errors don’t exist? To even begin to answer these questions we need a specification: a description of what it means for a piece of code to be correct, stated either explicitly (e.g. my private data are never leaked to third parties) or implicitly (e.g. this code will not terminate with an uncaught exception). This project’s goal is to develop efficient ways to write, debug, and reason about software and specifications through the use of random testing.

Dynamic languages are flexible, allowing small, expressive programs to be written with little effort. As these programs evolve, the lack of static typing makes them increasingly difficult to maintain, extend, and reason about. We explore static type systems for dynamic languages like Ruby. Our type systems are designed to handle common idioms used by Ruby programmers meaning that programs need not be changed in order to gain the benefits of static checks. Our main project is RDL, a lightweight system for adding types, type checking, and contracts to Ruby. RDL supports just-in-time static type checking that allows it to type check Ruby code that uses metaprogramming. This is possible because the programmer may control at what point of execution the type checking is done.

• Statically Verifying Contracts in Higher-order Languages. Phil Nguyen, David Van Horn.
• Programming Languages for Secure Multiparty Computation. Michael Hicks, David Darais.
• Dynamic Updating for High-Availability Software Systems. Michael Hicks, Luis Pina.