Extended treatment of a new style of operational semantics that was applied in the work from our PLDI'21 paper
Extended version of our ITP'16 paper
Overview of and case for the DeepSpec project
A file system implemented and verified in Coq, using separation logic, connected to Linux and providing respectable performance
Introducing the Ur/Web programming language
Excerpts from CPDT
Extended version of my ICFP'06 paper
How to verify formally that an enclave-style hardware architecture fully isolates running threads from each other, e.g. considering timing side channels
Proving the right correctness relationship between two RISC-V implementation techniques: multiplication via a hardware instruction or via trapping to a software routine
Security verification of file systems that takes probabilistic failures into account
An integrated Coq proof of a cryptographic server, as one machine-code image that runs on bare metal, built up from quite different programming languages and verification approaches
Pushing the Coq-verified compilation guarantees even lower (to a C subset), within our ATL tensor-programming project
Could Coq be an even more pleasant C-programming IDE than the big names, if we work the right magic with notations and tactics?
Our lightweight but flexible approach to mechanized semantics of hardware instruction sets
Genetic program search meets translation validation for Fiat Cryptography, improving performance and shrinking the trusted base even while bringing in more avant-garde compiler techniques
Modular proofs of concurrent libraries, mixing classic lock-free data structures and transactional memory, in the style of interaction trees
Taking all the fine-grained concurrency reasoning out of design and proof of cache-coherence protocols, via a DSL proved sound with commutativity analysis
Mechanized cryptographic protocols that are guaranteed to resist adversary interference, in much the same way that traditional type systems resist memory errors
Generating formally verified compilers modularly via Coq-proved rewrite rules, applied to make Fiat Cryptography a lot faster
Understanding regressions in Coq itself with automatic reduction of test cases
Round two of using Coq to compile functional programs to imperative programs with proof, using proof-generating extensions for flexibility
Deriving correct imperative loop programs from functional programs with Coq proof, in a style inspired by Halide
Using Coq to derive correct first-order implementations of network protocols from higher-order descriptions, applied to TLS 1.3
Overview of a key design principle in FRAP courses: mixed embeddings for concise but flexible syntax definitions for embedded languages
An end-to-end, software+hardware Coq proof for an Internet-connected lightbulb
Bootstrapping on software-development tools to create a good experience simulating, debugging, and profiling hardware designs in Bluespec-like languages, taking advantage of high-level properties of source files
The last link in a pipeline for automatic compilation, with proofs, from relational specifications to Bedrock assembly programs
A new hardware-description language that combines Bluespec's modular-decomposition style with fine-grained control of timing; includes Coq embedding with a verified compiler to circuits
Using Coq to derive efficient binary-format parsers from declarative specifications, automatically
Correct-by-construction generation of low-level crypto-primitive code using Coq
Summarizing our team's work with formal methods in the DARPA SSITH program
FSCQ extended to track information-flow policies that distinguish between different users
An introduction to a slick way of implementing programming languages concisely and modularly, focusing on type checking, told in the style of a play, including songs
A theorem in real analysis shows that, in a world where all computations are continuous, we can't implement interesting conditional tests over, say, the real numbers. Here we show how to get around the problem with a functional-programming-friendly topological treatment of nondeterminism. (We can make discrete decisions about values from continuous spaces so long as we leave some wiggle room about what will actually happen at runtime.)
A surprisingly simple way to convert terms in higher-order logic into first-class syntax trees, using standard features: would you believe that reification can mostly be done by term normalization in the metalanguage?
FSCQ extended to support "flush" operations and delayed syncing of data to disk, as a performance optimization
Using refinement types to upper-bound program asymptotic running time, taking advantage of invariants specific to data structures
A Coq framework for modular correctness proofs of computer-architecture designs, supporting automatic extraction to circuits that run on FPGAs, etc.
The sales pitch for our Fiat system as embodying a new programming style, with novel and effective kinds of abstraction and modularity
A compiler optimization for Ur/Web that adds caching for SQL-query results and derived computations, inferring sound invalidation strategies that often avoid bottlenecks for parallel execution
A Coq framework for verifying that nested loops obey dependency constraints, in message-passing distributed programs that collaboratively fill in the cells of large multidimensional grids
Coq proofs of several distributed key-value store algorithms, including principles for modular reasoning about client programs that use them
A file system implemented and verified in Coq, using separation logic, connected to Linux and providing respectable performance
The whole-program optimizing compiler for Ur/Web
Modular Coq proofs of Bluespec-style hardware descriptions, where processors and memory systems can be verified separately against generic specs (in the style of labeled transition systems) that are compatible with many different optimizations
Deriving efficient OCaml implementations of abstract data types, from declarative specifications, in Coq, mostly automatically. The main case study works with SQL-style relational queries and update operations.
At long last, a paper on the design of Ur/Web, a DSL for Web applications, supporting novel encapsulation techniques and a simple concurrency model for distributed applications
A case study in building a whole-program Coq proof that covers both an application (a database-backed dynamic Web application) and systems infrastructure (a cooperative thread library). The components are verified modularly with Bedrock, and there is a verified compiler for a domain-specific language that can be used to derive similar theorems for similar Web applications, with minimal new proving work.
An approach to verifying multilanguage programs in the Bedrock framework, mixing operational semantics for intralanguage reasoning and axiomatic semantics for interlanguage reasoning
Coq-verified just-in-time compilation for packet filters, etc., in Linux
A framework for combining reflective Coq tactics, applied in the Bedrock system to verify imperative programs
A Coq category-theory library, designed to support computationally efficient proofs of large goals, taking advantage of recent improvements to the homotopy-type-theory Coq version and giving some other wishlist items for Coq
Bedrock takes literally the idea of C as a "macro assembly language." All the programming features are built up as macros on top of assembly language, and macros have verified Hoare logic-style proof rules attached to them, so that one gets a "free" environment for mostly automated deductive program verification for any mix of macros used in a particular program.
A verified compiler for an idealization of the Bluespec hardware description language
A constructive proof that automating separation logic proofs for systems code is easy, despite claims to the contrary coming from SMT solver-centric perspectives. ;-) Specifically, this paper introduced Bedrock, a Coq library for foundational verification of code at the assembly level of abstraction. A mostly-automated separation logic prover uses a modest amount of programmer annotation to drive verification of examples like imperative data structures and a cooperative threading library.
Static analysis for security policies for Ur/Web applications, based on the key new idea of representing policies as SQL queries. The analysis follows the well-trod path of symbolic evaluation and automated first-order-logic theorem-proving.
A first paper about Ur, focusing on the metaprogramming aspect: we can write generic programs that write programs, based on inputs like database schemas, summaries of HTML form configurations, etc., and we can type-check our generators statically without needing to write any proof terms.
A case study in verifying a compiler to an idealized assembly language from an untyped source language with most of the key dynamic features of ML: functions, products, sums, mutable references, and value-carrying exceptions. Syntax is encoded with parametric higher-order abstract syntax (PHOAS), which makes it possible to avoid almost all bookkeeping having to do with binders and fresh name generation. The semantics of the object languages are encoded in a new substitution-free style. All of the proofs are automated with tactic programs that can keep working even after changing the definitions of the languages.
An approach to automating correctness proofs about higher-order, imperative programs in Coq, based on an extensible simplifier for separation logic formulas
A new trick for encoding variable binders in Coq, along with an exploration of its consequences: almost trivial syntax and type-theoretic semantics for languages including such features as polymorphism and complicated binding structure (e.g., ML-style pattern matching); almost trivial type preservation proofs for compiler passes that don't need intensional analysis of variables; mostly-automated semantic correctness proofs about those passes, by way of adding an axiom to make the parametricity of CIC usable explicitly in proofs; and the ability to drop down to more traditional syntactic representations for more arduous but feasible proofs of the same properties, when intensional variable analysis is needed.
A compiler for a tiny statically-typed functional programming language, implemented in Coq with a proof of correctness. The main interesting bits are my use of dependently-typed abstract syntax and denotational semantics, along with some engineering tricks for making the task manageable.
I report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checkable proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's soundness theorem is expressed in terms of the bit-level semantics of x86 programs, so its correctness depends on very few assumptions. I take advantage of Coq's support for programming with dependent types and modules in the structure of my development. The approach is based on developing a library of reusable functors for transforming a verifier at one level of abstraction into a verifier at a lower level. Using this library, it's possible to prototype a verifier based on a new type system with a minimal amount of work, while obtaining a very strong soundness theorem about the final product.
We propose a new technique in support of the construction of efficient Foundational Proof-Carrying Code systems. Instead of suggesting that pieces of mobile code come with proofs of their safety, we instead suggest that they come with executable verifiers that can attest to their safety, as in our previous work on the Open Verifier. However, in contrast to that previous work, here we do away with any runtime proof generation by these verifiers. Instead, we require that the verifier itself is proved sound. To support this, we present a novel technique for extracting proof obligations about ML programs. Using this approach, we are able to demonstrate the first foundational verification technique for Typed Assembly Language with performance comparable to that of the traditional, uncertified TAL type checker.
We describe how to use the BLAST model checker to generate program test suites that achieve full coverage with respect to a given set of predicates.
On verifying functional properties of filesystems in the presence of failures, using proof assistants
Some thoughts on how Coq is actually in pretty good shape to use today for non-trivial programming with dependent types
We show how to combine the interactive proof assistant Coq and the Nelson-Oppen-style automated first-order theorem prover Kettle in a synergistic way. We do this with a Kettle tactic for Coq that uses theory-specific reasoning to simplify goals based on automatically chosen case analyses, returning to the user as subgoals the cases it couldn't prove automatically. The process can then be repeated recursively, using Coq's tactical language as a very expressive extension of the matching strategies found in provers like Simplify. We also discuss how to encode specialized first-order proofs efficiently in Coq using proof by reflection.
We propose a new framework for the construction of trustworthy program verifiers. The Open Verifier architecture can be viewed as an optimized Foundational Proof-Carrying Code toolkit. Instead of proposing that code producers send proofs of safety with all of their programs, we instead suggest that they send re-usable proof-generating verifiers. The proofs are generated in an online fashion via a novel interaction scheme between the untrusted verifier and the trusted core of the system.
A new approach to checking assembly programs in a way similar to that used in the Java Bytecode Verifier. We introduce a novel mixed type/value technique that makes it tractable to deal with some of the "dependent typing" issues that come up. We also present results on using this technique to help students in an undergraduate compilers class debug their class projects.
We present a type system that is useful in saving type annotation space in intermediate language terms expressed in the restricted form called "A-normal form" or "one-half CPS." Our approach imports ideas from strict logic, which is based on the idea of hypotheses that must be used at least once. The resulting system is relevant to the efficiency of type-preserving compilers.
A poster about certified program verifiers in Coq
We describe a system that combines security automaton-based program specification with a facility for relational-style queries about the possible execution paths of a program.
How to do dependently-typed generation of proofs about programming language syntax and semantics
My PhD dissertation, re-presenting the work on certified program verifiers (from ICFP'06) and certified compilers (from PLDI'07)
An overview of a work-in-progress functional programming language that puts dependent types and theorem proving to work to make it easier to write concise and maintainable web applications
This is an extended version of our VMCAI'06 paper, containing a formalization of our model extraction procedure and additional examples.
A summary of my experiences developing a proof-generating TAL type checker within the Open Verifier framework. In the style of Foundational PCC, the soundness of this verifier and the proofs it generates is based on no assumptions about the TAL type system. This was one of the first projects to consider the runtime performance of Foundational PCC-style verification.