Œuf

Verified Coq Extraction in Coq

Running code written in Coq requires first extracting the code to a more conventional programming language (usually OCaml) and then compiling the extracted code with that language's compiler. Hence, the extraction mechanism, the OCaml compiler, and the OCaml runtime are all in the trusted computing base (TCB). In some sense, the runtime is even "more trusted" because it is present when the verified kernel executes—the other components are trusted only to produce correct binary code, so any exploit would have to rely on a compiler bug producing exploitable code. Moreover, the OCaml runtime can be a burden for performance and fine-grained interoperability with unverified code. Œuf is a complier from a subset of Gallina to x86 that uses CompCert instead of the OCaml compiler. Thus, Œuf-compiled code does not require a complex runtime library, reducing the TCB, improving performance, and allowing interoperability with other x86 code through a well-defined binary interface.

Œuf is itself verified and written in Coq. We start with a sound reflection of the Gallina program inside of Coq and eventually produce, via a series of meaning-preserving transformations, a program in a high-level IR of CompCert. We can then rely on CompCert and its correctness theorem to produce equivalent x86. Because our compiler and CompCert are themselves written in Coq and extracted to OCaml, we are still trusting OCaml, but in a much-reduced way: We are trusting OCaml only to compile and execute our compiler (and CompCert) correctly. Given that, the code produced by our compiler is correct and the OCaml runtime is not present when the code is run under potentially adversarial inputs. An attacker, with no control over the Gallina program we write, our compiler, CompCert, or OCaml, would have to discover a Gallina program that, due to an OCaml or Coq bug triggered when compiling our compiler, was miscompiled by our compiler in such a way that a security vulnerability arises.

Our compiler does not support the entire Gallina language and does not prescribe a particular resource management scheme. Instead, we are targeting a subset of Gallina sufficient for implementing event handlers in reactive systems. We also believe that more traditional systems, including file system libraries and compilers, will be implementable in our Gallina subset. Resource management is parameterized in the sense that we expect code extracted from Gallina and compiled to x86 to be invoked from other systems languages (like C), which will be responsible for reclaiming resources like memory, e.g., via slab allocation.

Source

Œuf will become open source when published. It is still under development, i.e., not working yet.

The Œuf Team

Œuf is developed in the University of Washington Programming Languages and Software Engineering group, by

  1. Eric Mullen
  2. Stuart Pernsteiner
  3. James R. Wilcox

  4. Zachary Tatlock
  5. Dan Grossman