Tue 9 Jan 2018 11:00 - 11:30 at Museum A - Trusted Verification Frameworks and Systems Chair(s): Zhong Shao

\newcommand{\Oeuf}{\OE uf\xspace} \newcommand{\eg}{\emph{e.g.}\xspace}

Verifying systems by implementing them in the programming language of a proof assistant (\eg, Gallina for Coq) lets us directly leverage the full power of the proof assistant for verifying the system. But, to execute such an implementation requires \emph{extraction}, a large complicated process that is in the trusted computing base (TCB).

This paper presents \Oeuf, a verified compiler from a subset of Gallina to assembly. \Oeuf's correctness theorem ensures that compilation preserves the semantics of the source Gallina program. We describe how \Oeuf's specification can be used as a foreign function interface to reason about the interaction between compiled Gallina programs and surrounding shim code. Additionally, \Oeuf maintains a small TCB for its front-end by reflecting Gallina programs to \Oeuf
source and automatically ensuring equivalence using computational denotation. This design enabled us to implement some early compiler passes (\eg, lambda lifting) in the untrusted reflection and ensure their correctness via translation validation. To evaluate \Oeuf, we compile Appel's SHA256 specification from Gallina to x86 and write a shim for the generated code, yielding a verified \texttt{sha256sum} implementation with a small TCB.

Tue 9 Jan

CPP-2018
10:30 - 12:00: CPP 2018 - Trusted Verification Frameworks and Systems at Museum A
Chair(s): Zhong ShaoYale University
CPP-2018151549020000010:30 - 11:00
Talk
Mathias FleuryMPI-INF, Jasmin Christian Blanchette, Peter LammichTechnische Universität München
DOI
CPP-2018151549200000011:00 - 11:30
Talk
Eric MullenUniversity of Washington, Stuart PernsteinerUniversity of Washington, USA, James R. WilcoxUniversity of Washington, Zachary TatlockUniversity of Washington, Dan GrossmanUniversity of Washington
DOI
CPP-2018151549380000011:30 - 12:00
Talk
Maria Paola BonacinaUniversity of Verona, Italy, Stéphane Graham-LengrandCNRS, France, Natarajan ShankarSRI International, USA
DOI