Author

Adam Chlipala

96 papers · 2004–2026

2004peak 9 in 20222026

Frequent co-authors

Papers

showing 1–25 of 96 RSS

Using Crash Hoare logic for certifying the FSCQ file system

Haogang Chen, Daniel Ziegler, Tej Chajed +3 more

Computer Networks and Communications · October 2015 · cited 200× · DOI ↗ · more like this ·

FSCQ is the first file system with a machine-checkable proof (using the Coq proof assistant) that its implementation meets its specification and whose specification includes crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover the file system correctly without losing data.

Generating Tests from Counterexamples

Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger +2 more

Software · 2004 · cited 199× · OpenAlex ↗ · more like this ·

We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30 K lines of code. The analysis and test-vector generation is fully automatic (no user intervention) and exact (no false positives).

Mostly-automated verification of low-level programs in computational separation logic

Adam Chlipala

Artificial Intelligence · ACM SIGPLAN Notices · 4 Jun 2011 · cited 132× · DOI ↗ · more like this ·

Several recent projects have shown the feasibility of verifying low-level systems software. Verifications based on automated theorem-proving have omitted reasoning about first-class code pointers , which is critical for tasks like certifying implementations of threads and processes. Conversely, verifications that deal with first-class code pointers have featured long, complex, manual proofs. In this paper, we introduce the Bedrock framework, which supports mostly-automated proofs about programs with the full range of features needed to implement, e.g., language runtime systems. The heart of our approach is in mostly-automated discharge of verification conditions inspired by separation logic. Our take on separation logic is computational , in the sense that function specifications are usually written in terms of reference implementations in a purely functional language . Logical…

Parametric higher-order abstract syntax for mechanized semantics

Adam Chlipala

Artificial Intelligence · ACM SIGPLAN Notices · 20 Sep 2008 · cited 129× · DOI ↗ · more like this ·

We present parametric higher-order abstract syntax (PHOAS) , a new approach to formalizing the syntax of programming languages in computer proof assistants based on type theory. Like higher-order abstract syntax (HOAS), PHOAS uses the meta language's binding constructs to represent the object language's binding constructs. Unlike HOAS, PHOAS types are definable in general-purpose type theories that support traditional functional programming, like Coq's Calculus of Inductive Constructions. We walk through how Coq can be used to develop certified, executable program transformations over several statically-typed functional programming languages formalized with PHOAS; that is, each transformation has a machine-checked proof of type preservation and semantic preservation. Our examples include CPS translation and closure conversion for simply-typed lambda calculus, CPS translation for System…

A verified compiler for an impure functional language

Adam Chlipala

Artificial Intelligence · 17 Jan 2010 · cited 101× · DOI ↗ · more like this ·

We present a verified compiler to an idealized assembly language from a small, untyped functional language with mutable references and exceptions. The compiler is programmed in the Coq proof assistant and has a proof of total correctness with respect to big-step operational semantics for the source and target languages. Compilation is staged and includes standard phases like translation to continuation-passing style and closure conversion, as well as a common subexpression elimination optimization. In this work, our focus has been on discovering and using techniques that make our proofs easy to engineer and maintain. While most programming language work with proof assistants uses very manual proof styles, all of our proofs are implemented as adaptive programs in Coq's tactic language, making it possible to reuse proofs unchanged as new language features are added.

Kami: a platform for high-level parametric hardware specification and its modular verification

Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman +2 more

Computational Theory and Mathematics · Proceedings of the ACM on Programming Languages · 29 Aug 2017 · cited 95× · DOI ↗ · more like this ·

It has become fairly standard in the programming-languages research world to verify functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coq library that enables similar expressive and modular reasoning for hardware designs expressed in the style of the Bluespec language. We can specify, implement, and verify realistic designs entirely within Coq, ending with automatic extraction into a pipeline that bottoms out in FPGAs. Our methodology, using labeled transition systems, has been evaluated in a case study verifying an infinite family of multicore systems, with cache-coherent shared memory and pipelined cores implementing (the base integer subset of) the RISC-V instruction set.

Effective interactive proofs for higher-order imperative programs

Adam Chlipala, Gregory Malecha, Greg Morrisett +2 more

Artificial Intelligence · 31 Aug 2009 · cited 93× · DOI ↗ · more like this ·

We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with…

A certified type-preserving compiler from lambda calculus to assembly language

Adam Chlipala

Artificial Intelligence · 10 Jun 2007 · cited 93× · DOI ↗ · more like this ·

We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. We demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge large parts of our proof obligations automatically.

Static checking of dynamically-varying security policies in database-backed applications

Adam Chlipala

Artificial Intelligence · DSpace@MIT (Massachusetts Institute of Technology) · 4 Oct 2010 · cited 92× · DOI ↗ · more like this ·

We present a system for sound static checking of security policies for database-backed Web applications. Our tool checks a combination of access control and information flow policies, where the policies vary based on database contents. For instance, one or more database tables may represent an access control matrix, controlling who may read or write which cells of these and other tables. Using symbolic evaluation and automated theorem-proving, our tool checks these policies statically, requiring no program annotations (beyond the policies themselves) and adding no run-time overhead. Specifications come in the form of SQL queries as policies: for instance, an application’s confidentiality policy is a fixed set of queries, whose results provide an upper bound on what information may be released to the user. To provide userdependent policies, we allow queries to depend on what secrets the…

The bedrock structured programming system

Adam Chlipala

Artificial Intelligence · DSpace@MIT (Massachusetts Institute of Technology) · 25 Sep 2013 · cited 88× · DOI ↗ · more like this ·

We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally the saying that C is a "macro assembly language": we introduce an expressive notion of certified low-level macros, sufficient to build up the usual features of C and beyond as macros with no special support in the core. Furthermore, our macros have integrated support for strongest postcondition calculation and verification condition generation, so that we can provide a high-productivity formal verification environment within Coq for programs composed from any combination of macros. Our…

Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises

Andres Erbsen, Jade Philipoom, Jason Gross +2 more

Information Systems · DSpace@MIT (Massachusetts Institute of Technology) · May 2019 · cited 87× · DOI ↗ · more like this ·

We introduce a new approach for implementing cryptographic arithmetic in short high-level code with machine-checked proofs of functional correctness. We further demonstrate that simple partial evaluation is sufficient to transform into the fastest-known C code, breaking the decades-old pattern that the only fast implementations are those whose instruction-level steps were written out by hand. These techniques were used to build an elliptic-curve library that achieves competitive performance for 80 prime fields and multiple CPU architectures, showing that implementation and proof effort scales with the number and complexity of conceptually different algorithms, not their use cases. As one outcome, we present the first verified high-performance implementation of P-256, the most widely used elliptic curve. implementations from our library were included in BoringSSL to replace existing…

Fiat

Benjamin Delaware, Clément Pit-Claudel, Jason Gross +1 more

Artificial Intelligence · 19 Dec 2014 · cited 87× · DOI ↗ · more like this ·

We present Fiat, a library for the Coq proof assistant supporting refinement of declarative specifications into efficient functional programs with a high degree of automation. Each refinement process leaves a proof trail, checkable by the normal Coq kernel, justifying its soundness. We focus on the synthesis of abstract data types that package methods with private data. We demonstrate the utility of our framework by applying it to the synthesis of query structures -- abstract data types with SQL-like query and insert operations. Fiat includes a library for writing specifications of query structures in SQL-inspired notation, expressing operations over relations (tables) in terms of mathematical sets. This library includes a suite of tactics for automating the refinement of specifications into efficient, correct-by-construction OCaml code. Using these tactics, a programmer can generate…

Ur

Adam Chlipala

Artificial Intelligence · 5 Jun 2010 · cited 84× · DOI ↗ · more like this ·

Dependent types provide a strong foundation for specifying and verifying rich properties of programs through type-checking. The earliest implementations combined dependency, which allows types to mention program variables; with type-level computation, which facilitates expressive specifications that compute with recursive functions over types. While many recent applications of dependent types omit the latter facility, we argue in this paper that it deserves more attention, even when implemented without dependency.

Chapar: certified causally consistent distributed key-value stores

Mohsen Lesani, Christian J. Bell, Adam Chlipala

Computer Networks and Communications · DSpace@MIT (Massachusetts Institute of Technology) · 7 Jan 2016 · cited 76× · DOI ↗ · more like this ·

Today’s Internet services are often expected to stay available and render high responsiveness even in the face of site crashes and network partitions. Theoretical results state that causal consistency is one of the strongest consistency guarantees that is possible under these requirements, and many practical systems provide causally consistent key-value stores. In this paper, we present a framework called Chapar for modular verification of causal consistency for replicated key-value store implementations and their client programs. Specifically, we formulate separate correctness conditions for key-value store implementations and for their clients. The interface between the two is a novel operational semantics for causal consistency. We have verified the causal consistency of two key-value store implementations from the literature using a novel proof technique. We have also implemented a…

Ur/Web

Adam Chlipala

Computer Networks and Communications · 19 Dec 2014 · cited 62× · DOI ↗ · more like this ·

The World Wide Web has evolved gradually from a document delivery platform to an architecture for distributed programming. This largely unplanned evolution is apparent in the set of interconnected languages and protocols that any Web application must manage. This paper presents Ur/Web, a domain-specific, statically typed functional programming language with a much simpler model for programming modern Web applications. Ur/Web's model is unified, where programs in a single programming language are compiled to other "Web standards" languages as needed; supports novel kinds of encapsulation of Web-specific state; and exposes simple concurrency, where programmers can reason about distributed, multithreaded applications via a mix of transactions and cooperative preemption. We give a tutorial introduction to the main features of Ur/Web and discuss the language implementation and the production…

Jitk: A Trustworthy In-Kernel Interpreter Infrastructure

Xi Wang, David Lazar, Nickolai Zeldovich +2 more

Artificial Intelligence · 4 Sep 2015 · cited 57× · OpenAlex ↗ · more like this ·

Modern operating systems run multiple interpreters in the kernel, which enable user-space applications to add new functionality or specialize system policies. The correct-ness of such interpreters is critical to the overall system security: bugs in interpreters could allow adversaries to compromise user-space applications and even the kernel. Jitk is a new infrastructure for building in-kernel in-terpreters that guarantee functional correctness as they compile user-space policies down to native instructions for execution in the kernel. To demonstrate Jitk, we im-plement two interpreters in the Linux kernel, BPF and INET-DIAG, which are used for network and system call filtering and socket monitoring, respectively. To help ap-plication developers write correct filters, we introduce a high-level rule language, along with a proof that Jitk correctly translates high-level rules all the way…

Verifying a high-performance crash-safe file system using a tree specification

Haogang Chen, Tej Chajed, Alex Konradi +5 more

Computer Networks and Communications · DSpace@MIT (Massachusetts Institute of Technology) · 12 Oct 2017 · cited 54× · DOI ↗ · more like this ·

DFSCQ is the first file system that (1) provides a precise specification for fsync and fdatasync, which allow applications to achieve high performance and crash safety, and (2) provides a machine-checked proof that its implementation meets this specification. DFSCQ's specification captures the behavior of sophisticated optimizations, including log-bypass writes, and DFSCQ's proof rules out some of the common bugs in file-system implementations despite the complex optimizations.

TiML: a functional language for practical complexity analysis with invariants

Peng Wang, Di Wang, Adam Chlipala

Artificial Intelligence · Proceedings of the ACM on Programming Languages · 12 Oct 2017 · cited 51× · DOI ↗ · more like this ·

We present TiML (Timed ML), an ML-like functional language with time-complexity annotations in types. It uses indexed types to express sizes of data structures and upper bounds on running time of functions; and refinement kinds to constrain these indices, expressing data-structure invariants and pre/post-conditions. Indexed types are flexible enough that TiML avoids a built-in notion of ≴size,≵ and the programmer can choose to index user-defined datatypes in any way that helps her analysis. TiML's distinguishing characteristic is supporting highly automated time-bound verification applicable to data structures with nontrivial invariants. The programmer provides type annotations, and the typechecker generates verification conditions that are discharged by an SMT solver. Type and index inference are supported to lower annotation burden, and, furthermore, big-O complexity can be inferred…

The essence of Bluespec: a core language for rule-based hardware design

Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala +1 more

Hardware and Architecture · DSpace@MIT (Massachusetts Institute of Technology) · 7 Jun 2020 · cited 50× · DOI ↗ · more like this ·

The Bluespec hardware-description language presents a significantly higher-level view than hardware engineers are used to, exposing a simpler concurrency model that promotes formal proof, without compromising on performance of compiled circuits. Unfortunately, the cost model of Bluespec has been unclear, with performance details depending on a mix of user hints and opaque static analysis of potential concurrency conflicts within a design. In this paper we present Koika, a derivative of Bluespec that preserves its desirable properties and yet gives direct control over the scheduling decisions that determine performance. Koika has a novel and deterministic operational semantics that uses dynamic analysis to avoid concurrency anomalies. Our implementation includes Coq definitions of syntax, semantics, key metatheorems, and a verified compiler to circuits. We argue that most of the extra…

Position paper: the science of deep specification

Andrew W. Appel, Lennart Beringer, Adam Chlipala +4 more

Computational Theory and Mathematics · Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences · 4 Sep 2017 · cited 34× · DOI ↗ · more like this ·

We introduce our efforts within the project ‘The science of deep specification’ to work out the key formal underpinnings of industrial-scale formal specifications of software and hardware components, anticipating a world where large verified systems are routinely built out of smaller verified components that are also used by many other projects. We identify an important class of specification that has already been used in a few experiments that connect strong component-correctness theorems across the work of different teams. To help popularize the unique advantages of that style, we dub it deep specification , and we say that it encompasses specifications that are rich , two-sided , formal and live (terms that we define in the article). Our core team is developing a proof-of-concept system (based on the Coq proof assistant) whose specification and verification work is divided across…

The open verifier framework for foundational verifiers

Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula +1 more

Artificial Intelligence · 10 Jan 2005 · cited 34× · DOI ↗ · more like this ·

We present the Open Verifier approach for verifying untrusted code using customized verifiers. This approach can be viewed as an instance of foundational proof-carrying code where an untrusted program can be checked using the verifier most natural for it instead of using a single generic type system. In this paper we focus on a specialized architecture designed to reduce the burden of expressing both type-based and Hoare-style verifiers.A new verifier is created by providing an untrusted executable extension module, which can incorporate directly pre-existing non-foundational verifiers based on dataflow analysis or type checking. The extensions control virtually all aspects of the verification by carrying on a dialogue with the Open Verifier using a language designed both to correspond closely to common verification actions and to carry simple adeQuacy proofs for those actions.We…

Compiler verification meets cross-language linking via data abstraction

Peng Wang, Santiago Cuéllar, Adam Chlipala

Artificial Intelligence · DSpace@MIT (Massachusetts Institute of Technology) · 15 Oct 2014 · cited 31× · DOI ↗ · more like this ·

Many real programs are written in multiple different programming languages, and supporting this pattern creates challenges for formal compiler verification. We describe our Coq verification of a compiler for a high-level language, such that the compiler correctness theorem allows us to derive partial-correctness Hoare-logic theorems for programs built by linking the assembly code output by our compiler and assembly code produced by other means. Our compiler supports such tricky features as storable cross-language function pointers, without giving up the usual benefits of being able to verify different compiler phases (including, in our case, two classic optimizations) independently. The key technical innovation is a mixed operational and axiomatic semantics for the source language, with a built-in notion of abstract data types, such that compiled code interfaces with other languages…

3 Formal Verification of Hardware Synthesis

Thomas Braibant, Adam Chlipala

Computational Theory and Mathematics · DSpace@MIT (Massachusetts Institute of Technology) · 2013 · cited 30× · OpenAlex ↗ · more like this ·

Abstract. We report on the implementation of a certified compiler for a high-level hardware description language (HDL) called Fe-Si (FEatherweight SynthesIs). Fe-Si is a simplified version of Bluespec, an HDL based on a notion of guarded atomic actions. Fe-Si is defined as a dependently typed deep embedding in Coq. The target language of the compiler corresponds to a synthesisable subset of Verilog or VHDL. A key aspect of our approach is that input programs to the compiler can be defined and proved correct inside Coq. Then, we use extraction and a Verilog back-end (written in OCaml) to get a certified version of a hardware design.

Integration verification across software and hardware for a simple embedded system

Andres Erbsen, Samuel Gruetter, Joonwon Choi +2 more

Artificial Intelligence · DSpace@MIT (Massachusetts Institute of Technology) · 18 Jun 2021 · cited 28× · DOI ↗ · more like this ·

The interfaces between layers of a system are susceptible to bugs if developers of adjacent layers proceed under subtly different assumptions. Formal verification of two layers against the same formal model of the interface between them can be used to shake out these bugs. Doing so for every interface in the system can, in principle, yield unparalleled assurance of the correctness and security of the system as a whole. However, there have been remarkably few efforts that carry out this exercise, and all of them have simplified the task by restricting interactivity of the application, inventing new simplified instruction sets, and using unrealistic input and output mechanisms. We report on the first verification of a realistic embedded system, with its application software, device drivers, compiler, and RISC-V processor represented inside the Coq proof assistant as one mathematical…

C4: verified transactional objects

Mohsen Lesani, Li-yao Xia, Anders Kaseorg +4 more

Computer Networks and Communications · Proceedings of the ACM on Programming Languages · 29 Apr 2022 · cited 26× · DOI ↗ · more like this ·

Transactional objects combine the performance of classical concurrent objects with the high-level programmability of transactional memory. However, verifying the correctness of transactional objects is tricky, requiring reasoning simultaneously about classical concurrent objects, which guarantee the atomicity of individual methods—the property known as linearizability—and about software-transactional-memory libraries, which guarantee the atomicity of user-defined sequences of method calls—or serializability. We present a formal-verification framework called C4, built up from the familiar notion of linearizability and its compositional properties, that allows proof of both kinds of libraries, along with composition of theorems from both styles to prove correctness of applications or further libraries. We apply the framework in a significant case study, verifying a transactional set…