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
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

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