research-article

Œuf: minimizing the Coq extraction TCB

Authors:

Stuart Pernsteiner,

James R. Wilcox,

Zachary Tatlock,

Dan GrossmanAuthors Info & Claims

CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 172 - 185

https://doi.org/10.1145/3167089

Published: 08 January 2018 Publication History

Abstract

Verifying systems by implementing them in the programming language of a proof assistant (e.g., 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 extraction, a large complicated process that is in the trusted computing base (TCB).

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

References

[1]

Amal Ahmed. 2015. Verified Compilers for a Multi-Language World. In 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA . 15–31.

[2]

Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O’Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, and others. 2016. Cogent: Verifying high-assurance file system implementations. In ACM SIGPLAN Notices, Vol. 51. ACM, 175–188.

Digital Library

[3]

Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In CoqPL Workshop (CoqPL ’17).

[4]

Andrew W. Appel. 2011. Verified Software Toolchain. In Proceedings of the 20th European Conference on Programming Languages and Systems: Part of the Joint European Conferences on Theory and Practice of Software (ESOP’11/ETAPS’11) . Springer-Verlag.

Digital Library

[5]

Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37, 2 (April 2015).

Digital Library

[6]

Nick Benton and Chung-Kil Hur. 2009. Biorthogonality, Step-indexing and Compiler Correctness. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP ’09) . 97–108.

Digital Library

[7]

H Boehm and M Weiser. 1988. Garbage Collection in an Uncooperative Environment. In Software Practice and Experience.

Digital Library

[8]

Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2015. Using Crash Hoare Logic for Certifying the FSCQ File System. In Proceedings of the 25th Symposium on Operating Systems Principles (SOSP ’15) . ACM.

Digital Library

[9]

Adam Chlipala. 2007. A certified type-preserving compiler from lambda calculus to assembly language. In Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007 . 54–65.

Digital Library

[10]

Adam Chlipala. 2010. A Verified Compiler for an Impure Functional Language. SIGPLAN Not. 45, 1 (Jan. 2010), 93–106.

Digital Library

[11]

Adam Chlipala. 2013. Certified Programming with Dependent Types. MIT Press.

Digital Library

[12]

Guillaume Claret. 2016. Coq.io. (2016). http://coq.io/

[13]

David Costanzo, Zhong Shao, and Ronghui Gu. 2016. End-to-end Verification of Information-flow Security for C and Assembly Programs. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16) . 648–664.

Digital Library

[14]

Maulik A. Dave. 2003. Compiler Verification: A Bibliography. SIGSOFT Softw. Eng. Notes 28, 6 (2003), 2–2.

Digital Library

[15]

Maxime Dénès and Xavier Leroy. 2015. Coqonut: A verified JIT compiler for Coq. http://www.maximedenes.fr/download/coqonut.pdf . (January 2015).

[16]

Paul Govereau. 2012. Denotational Translation Validation. Ph.D. Dissertation. Harvard University.

Digital Library

[17]

Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015 . 595–608.

Digital Library

[18]

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016. 653–669.

Digital Library

[19]

Arjun Guha, Mark Reitblatt, and Nate Foster. 2013. Machine-verified Network Controllers. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’13) . ACM.

Digital Library

[20]

Dongseok Jang, Zachary Tatlock, and Sorin Lerner. 2012. Establishing Browser Security Guarantees Through Formal Shim Verification. In 21st USENIX Conference on Security Symposium (SECURITY ’12). USENIX Association.

Digital Library

[21]

Jacques-Henri Jourdan, François Pottier, and Xavier Leroy. 2012. Validating LR (1) Parsers. In Proceedings of the 21st European Symposium on Programming (ESOP 2012) (Lecture Notes in Computer Science), Vol. 7211. Springer, 397–416.

Digital Library

[22]

Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis. 2016. Lightweight Verification of Separate Compilation. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16) . 178–190.

Digital Library

[23]

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: Formal Verification of an OS Kernel. In Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles (SOSP ’09) . ACM.

Digital Library

[24]

Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14) . ACM.

Digital Library

[25]

Xavier Leroy. 2006. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’06) . ACM.

Digital Library

[26]

Mohsen Lesani, Christian J. Bell, and Adam Chlipala. 2016. Chapar: Certified Causally Consistent Distributed Key-value Stores. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16) . ACM.

Digital Library

[27]

Pierre Letouzey. 2008. Extraction in Coq: An Overview. In Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008 (Lecture Notes in Computer Science), Vol. 5028. 359–369.

Digital Library

[28]

Gregory Malecha. 2015. Template Coq Plugin. https://github.com/ gmalecha/template-coq . (2015).

[29]

John McCarthy and James Painter. 1967. Correctness of a compiler for arithmetic expressions. Mathematical aspects of computer science 1 (1967).

[30]

Andrew McCreight, Tim Chevalier, and Andrew Tolmach. 2010. A Certified Framework for Compiling and Executing Garbage-collected Languages. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP ’10) . 273–284.

Digital Library

[31]

J. Strother Moore. 1989. A Mechanically Verified Language Implementation. J. Autom. Reasoning 5, 4 (1989), 461–492.

Digital Library

[32]

Eric Mullen, Daryl Zuniga, Zachary Tatlock, and Dan Grossman. 2016. Verified Peephole Optimizations for CompCert. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16) .

Digital Library

[33]

Magnus O. Myreen and Scott Owens. 2012. Proof-Producing Synthesis of ML from Higher-Order Logic (ICFP ’12).

Digital Library

[34]

Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. 2015. Pilsner: a compositionally verified compiler for a higher-order imperative language. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015 . 166–178.

Digital Library

[35]

James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings . 128–148.

Digital Library

[36]

Clément Pit-Claudel. 2016. Compilation Using Correct-by-Construction Program Synthesis . Master’s thesis. Massachusetts Institute of Technology. http://pit-claudel.fr/clement/MSc/

[37]

Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS ’98) . Springer-Verlag.

Digital Library

[38]

Hanan Samet. 1978. Proving the Correctness of Heuristically Optimized Code. Commun. ACM (1978).

Digital Library

[39]

R. Statman. 1985. Logical relations and the typed lambda-calculus. Information and Control 65, 2 (1985), 85 – 97.

[40]

Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15) . 275–287.

Digital Library

[41]

Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. 2016. A New Verified Compiler Backend for CakeML (ICFP ’16).

[42]

Ken Thompson. 1984. Reflections on Trusting Trust. Commun. ACM 27, 8 (Aug. 1984).

Digital Library

[43]

Peng Wang, Santiago Cuellar, and Adam Chlipala. 2014. Compiler verification meets cross-language linking via data abstraction. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014 . 675–690.

Digital Library

[44]

Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, and Zachary Tatlock. 2014. Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI ’14) . USENIX Association.

Digital Library

[45]

James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. 2015. Verdi: A Framework for Implementing and Formally Verifying Distributed Systems. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15) . ACM.

Digital Library

Cited By

Forster YSozeau MTabareau N(2024)Verified Extraction from Coq to OCamlProceedings of the ACM on Programming Languages10.1145/36563798:PLDI(52-75)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656379
Yuan SBesson FTalpin J(2024)End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoTComputer Aided Verification10.1007/978-3-031-65627-9_16(325-347)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65627-9_16
Tan YHeule MMyreen M(2023)Verified Propagation Redundancy and Compositional UNSAT Checking in CakeMLInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00690-y25:2(167-184)Online publication date: 27-Feb-2023
https://doi.org/10.1007/s10009-022-00690-y
Show More Cited By

Recommendations

Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq
Haskell '17

We demonstrate for the first time that Liquid Haskell, a refinement type checker for Haskell programs, can be used for arbitrary theorem proving by verifying a parallel, monoidal string matching algorithm implemented in Haskell. We use refinement types ...
Call-by-push-value in Coq: operational, equational, and denotational theory
CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

Call-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2018

306 pages

ISBN:9781450355865

DOI:10.1145/3176245

Program Chairs:
June Andronick
Data61 at CSIRO, Australia / UNSW, Australia
,
Amy Felty
University of Ottawa, Canada

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 January 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CPP '18

Sponsor:

SIGPLAN

CPP '18: Certified Proofs and Programs

January 8 - 9, 2018

CA, Los Angeles, USA

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
149
Total Downloads

Downloads (Last 12 months)17
Downloads (Last 6 weeks)3

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Forster YSozeau MTabareau N(2024)Verified Extraction from Coq to OCamlProceedings of the ACM on Programming Languages10.1145/36563798:PLDI(52-75)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656379
Yuan SBesson FTalpin J(2024)End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoTComputer Aided Verification10.1007/978-3-031-65627-9_16(325-347)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65627-9_16
Tan YHeule MMyreen M(2023)Verified Propagation Redundancy and Compositional UNSAT Checking in CakeMLInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00690-y25:2(167-184)Online publication date: 27-Feb-2023
https://doi.org/10.1007/s10009-022-00690-y
Pit-Claudel CPhilipoom JJamner DErbsen AChlipala AJhala RDillig I(2022)Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level codeProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523706(918-933)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523706
Vanhems FRusu VNowak DGrimaud G(2022)A Formal Correctness Proof for an EDF Scheduler Implementation2022 IEEE 28th Real-Time and Embedded Technology and Applications Symposium (RTAS)10.1109/RTAS54340.2022.00030(281-292)Online publication date: May-2022
https://doi.org/10.1109/RTAS54340.2022.00030
Yuan SBesson FTalpin JHym SZandberg KBaccelli E(2022)End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllersComputer Aided Verification10.1007/978-3-031-13188-2_15(293-316)Online publication date: 6-Aug-2022
https://doi.org/10.1007/978-3-031-13188-2_15
Monniaux DBoulmé S(2022)The Trusted Computing Base of the CompCert Verified CompilerProgramming Languages and Systems10.1007/978-3-030-99336-8_8(204-233)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99336-8_8
Paraskevopoulou ZLi JAppel A(2021)Compositional optimizations for CertiCoqProceedings of the ACM on Programming Languages10.1145/34735915:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473591
Tanaka ALindley SMogensen T(2021)Coq to C translation with partial evaluationProceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3441296.3441394(14-31)Online publication date: 18-Jan-2021
https://dl.acm.org/doi/10.1145/3441296.3441394
Annenkov DMilo MNielsen JSpitters BHriţcu CPopescu A(2021)Extracting smart contracts tested and verified in CoqProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3437992.3439934(105-121)Online publication date: 17-Jan-2021
https://dl.acm.org/doi/10.1145/3437992.3439934
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents