Abstract
MCQC is a compiler for extracting verified systems programs to low-level assembly, with no runtime or garbage collection requirements and an emphasis on performance. MCQC targets the Gallina functional language used in the Coq proof assistant. MCQC translates pure and recursive functions into C++17, while compiling monadic effectful functions to imperative C++ system calls. With a few memory and performance optimizations, MCQC combines verifiability with memory and runtime performance. By handling effectful and pure functions separately MCQC can generate executable verified code directly from Gallina, reducing the effort of implementing and executing verified systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Amani, S., et al.: Cogent: verifying high-assurance file system implementations. ACM SIGOPS Oper. Syst. Rev. 50(2), 175–188 (2016)
Anand, A., et al.: Certicoq: a verified compiler for coq. In: The Third International Workshop on Coq for Programming Languages (CoqPL) (2017)
Barras, B., et al.: The Coq proof assistant reference manual: Version 6.1. Ph.D. thesis, Inria (1997)
Bhargavan, K., et al.: Everest: towards a verified, drop-in replacement of https. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 71. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)
Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N.: Using crash hoare logic for certifying the FSCQ file system. In: Proceedings of the 25th Symposium on Operating Systems Principles, pp. 18–37. ACM (2015)
Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of haskell programs. ACM SIGPLAN Not. 46(4), 53–64 (2011)
Cock, D.: Bitfields and tagged unions in C: verification through automatic generation. VERIFY 8, 44–55 (2008)
Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 207–212. ACM (1982)
Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic-with proofs, without compromises. In: Simple High-Level Code for Cryptographic Arithmetic-With Proofs, Without Compromises, p. 0. IEEE
Gu, L., Vaynberg, A., Ford, B., Shao, Z., Costanzo, D.: Certikos: a certified kernel for secure cloud computing. In: Proceedings of the Second Asia-Pacific Workshop on Systems, p. 3. ACM (2011)
Ioannidis, E.: Extracting and optimizing low-level bytecode from high-level verified coq (2019)
Jones, S.P., Hall, C., Hammond, K., Partain, W., Wadler, P.: The glasgow haskell compiler: a technical overview. In: Proceedings of the UK Joint Framework for Information Technology (JFIT) Technical Conference, vol. 93 (1993)
Josuttis, N.M.: C++ Templates: The Complete Guide. Addison-Wesley Professional, Boston (2003)
Klein, G., et al.: sel4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207–220. ACM (2009)
Lattner, C.: LLVM and clang: Next generation compiler technology. In: The BSD Conference, pp. 1–2 (2008)
Leroy, X., et al.: The compcert verified compiler. Documentation and user’s manual, INRIA Paris-Rocquencourt (2012)
Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359–369. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69407-6_39
Liskov, B., Shrira, L.: Promises: linguistic support for efficient asynchronous procedure calls in distributed systems, vol. 23. ACM (1988)
Magalhães, J.P., Dijkstra, A., Jeuring, J., Löh, A.: A generic deriving mechanism for haskell. ACM SIGPLAN Not. 45(11), 37–48 (2010)
Mullen, E., Pernsteiner, S., Wilcox, J.R., Tatlock, Z., Grossman, D.: Œuf: minimizing the coq extraction TCB. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 172–185. ACM (2018)
Wadler, P.: A prettier printer. In: The Fun of Programming, Cornerstones of Computing, pp. 223–243 (2003)
Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 60–76. ACM (1989)
Wilcox, J.R., et al.: Verdi: a framework for implementing and formally verifying distributed systems. In: ACM SIGPLAN Notices, vol. 50, pp. 357–368. ACM (2015)
Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 214–227. ACM (1999)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Ioannidis, E., Kaashoek, F., Zeldovich, N. (2019). Extracting and Optimizing Formally Verified Code for Systems Programming. In: Badger, J., Rozier, K. (eds) NASA Formal Methods. NFM 2019. Lecture Notes in Computer Science(), vol 11460. Springer, Cham. https://doi.org/10.1007/978-3-030-20652-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-20652-9_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-20651-2
Online ISBN: 978-3-030-20652-9
eBook Packages: Computer ScienceComputer Science (R0)