HTTP/2 200 date: Wed, 04 Feb 2026 00:33:37 GMT content-type: application/json content-length: 5155 access-control-expose-headers: Link access-control-allow-headers: X-Requested-With, Accept, Accept-Encoding, Accept-Charset, Accept-Language, Accept-Ranges, Cache-Control access-control-allow-origin: * vary: Accept-Encoding content-encoding: gzip server: Jetty(9.4.40.v20210413) x-rate-limit: 5 x-rate-limit-interval: 1s x-concurrency-limit: 1 x-api-pool: public permissions-policy: interest-cohort=() {"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T20:54:59Z","timestamp":1767992099539,"version":"3.49.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-2130671,CCF- 2217064,CCF-2313023,CCF-1521584,2141064"],"award-info":[{"award-number":["CNS-2130671,CCF- 2217064,CCF-2313023,CCF-1521584,2141064"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of functional programs including compilers for C-like and functional languages. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Connecting these components is a minimalistic specification style based on functional programs and assertions over simple objects, omnisemantics for program execution, and basic separation logic for memory layout. This design enables us to bring the components together in a top-level correctness theorem that can be audited without understanding or trusting the internal interfaces and tools. Our case study is a simple cryptographic server for flipping of a bit of state through public-key authenticated network messages, and its proof shows total functional correctness including static bounds on memory usage. This paper also describes our experiences with the specific verification tools we build upon, along with detailed analysis of reasons behind the widely varying levels of productivity we experienced between combinations of tools and tasks.<\/jats:p>","DOI":"10.1145\/3656446","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1704-1729","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Foundational Integration Verification of a Cryptographic Server"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9854-7500","authenticated-orcid":false,"given":"Andres","family":"Erbsen","sequence":"first","affiliation":[{"name":"Google, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0709-8218","authenticated-orcid":false,"given":"Jade","family":"Philipoom","sequence":"additional","affiliation":[{"name":"Google, Berlin, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0700-3514","authenticated-orcid":false,"given":"Dustin","family":"Jamner","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-6360-904X","authenticated-orcid":false,"given":"Ashley","family":"Lin","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8369-9117","authenticated-orcid":false,"given":"Samuel","family":"Gruetter","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1900-3901","authenticated-orcid":false,"given":"Cl\u00e9ment","family":"Pit-Claudel","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359661"},{"key":"e_1_3_1_6_1","first-page":"503","volume-title":"In 16th USENIX Symposium on Operating SystemsDesign andlmplementation (OSDI22). USENIX Association","author":"Athalye Anish","year":"2022","unstructured":"Anish Athalye, M. Frans Kaashoek, and Nickolai Zeldovich. 2022. Verifying Hardware Security Modules with Information- Preserving Refinement. In 16th USENIX Symposium on Operating SystemsDesign andlmplementation (OSDI22). USENIX Association, Carlsbad, CA, 503-519. https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/athalye"},{"key":"e_1_3_1_7_1","first-page":"207","article-title":"Verified Correctness and Security of OpenSSL HMAC","author":"Beringer Lennart","year":"2015","unstructured":"Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015. Verified Correctness and Security of OpenSSL HMAC. In Proceedings of the 24th USENIX Conference on Security Symposium (Washington, D.C.) (SEC\u201915). USENIX Association, USA, 207-221.","journal-title":"In Proceedings of the 24th USENIX Conference on Security Symposium (Washington, D.C.) (SEC\u201915)."},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243131"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192406"},{"key":"e_1_3_1_10_1","article-title":"Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)","author":"Bourgeat Thomas","year":"2023","unstructured":"Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andrew Wright, and Adam Chlipala. 2023. Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). In ICFP\u201923: Proceedings of the 28th ACM SIGPLAN International Conference on Functional Programming (Seattle, WA, USA). http:\/\/adam.chlipala.net\/papers\/RiscvICFP23\/","journal-title":"In ICFP\u201923: Proceedings of the 28th ACM SIGPLAN International Conference on Functional Programming (Seattle, WA, USA)."},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579834"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660370"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_3_1_17_1","volume-title":"Ph.D. Dissertation. Massachusetts Institute of Technology.","author":"Erbsen Andres","year":"2022","unstructured":"Andres Erbsen. 2022.Foundational Integration Verification of Diverse Software and Hardware Components. Ph.D. Dissertation. Massachusetts Institute of Technology. http:\/\/adam.chlipala.net\/theses\/andreser.pdf"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/sp.2019.00005"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Andres Erbsen Jade Philipoom Dustin Jamner Ashley Lin Samuel Gruetter Adam Chlipala and Clement Pit-Claudel. 2024. Foundational Integration Verification of a Cryptographic Server. https:\/\/doi.org\/10.5281\/zenodo.10807084 10.5281\/zenodo.10807084","DOI":"10.5281\/zenodo.10807084"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_1_22_1","first-page":"527","volume-title":"Springer International Publishing, Cham","author":"Fulton Nathan","year":"2015","unstructured":"Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Volp, and Andre Platzer. 2015. KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. In Automated Deduction - CADE-25, Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham, 527-538."},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2022.17"},{"key":"e_1_3_1_24_1","first-page":"653","article-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sjoberg, and David Costanzo 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Savannah, GA, USA) (OSDI\u201916). USENIX Association, USA, 653-669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu","journal-title":"In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Savannah, GA, USA) (OSDI\u201916)."},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3068608"},{"key":"e_1_3_1_26_1","first-page":"165","volume-title":"In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI14)","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014.Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI14). USENIX Association, Broomfield, CO, 165-181. https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833621"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498685"},{"key":"e_1_3_1_29_1","first-page":"323","article-title":"Proving Confidentiality inaFile System Using DISKSEC","author":"Ileri Atalay","year":"2018","unstructured":"Atalay Ileri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2018. Proving Confidentiality inaFile System Using DISKSEC. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Carlsbad, CA, USA) (OSDI\u201918). USENIX Association, USA, 323-338.","journal-title":"In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Carlsbad, CA, USA) (OSDI\u201918)."},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung David Swasey Filip Sieczkowski Kasper Svendsen Aaron Turon Lars Birkedal and Derek Dreyer. 2015.Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Mumbai India) (POPL \u201915). Association for Computing Machinery New York NY USA 637-650. https:\/\/doi.org\/10.1145\/2676726.2676980 10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_3_1_32_1","doi-asserted-by":"crossref","unstructured":"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 (San Diego California USA) (POPL \u201914). Association for Computing Machinery New York NY USA 179-191. https:\/\/www.cse.chalmers.se\/~myreen\/popl14.pdf 10.1145\/2535838.2535841.","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314622"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682100023X"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523706"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_7"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00023"},{"key":"e_1_3_1_42_1","first-page":"1","volume-title":"In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16).","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016.Push-Button Verification of File Systems via Crash Refinement. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). USENIX Association, Savannah, GA, 1-16. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/sigurbjarnarson"},{"key":"e_1_3_1_43_1","first-page":"287","article-title":"Nickel: A Framework for Design and Verification of Information Flow Control Systems","author":"Sigurbjarnarson Helgi","year":"2018","unstructured":"Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. 2018. Nickel: A Framework for Design and Verification of Information Flow Control Systems. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Carlsbad, CA, USA) (OSDV18). USENIX Association, USA, 287-305. https:\/\/unsat.cs.washington.edu\/papers\/sigurbjarnarson-nickel.pdf","journal-title":"In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Carlsbad, CA, USA) (OSDV18)."},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360562"},{"key":"e_1_3_1_45_1","volume-title":"Master\u2019s thesis.","author":"Berg Stefan van den","year":"2020","unstructured":"Stefan van den Berg. 2020.RISC-V implementation of the NaCl-library. Master\u2019s thesis. https:\/\/pure.tue.nl\/ws\/portalfiles\/portal\/169647601\/Berg_S._ES_CSE.pdf"},{"key":"e_1_3_1_46_1","unstructured":"Andrew Waterman and Krste Asanovic. 2019.The RISC-V Instruction Set Manual. https:\/\/riscv.org\/specifications\/."},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","unstructured":"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. SIGPLAN Not. 50 6 (June 2015) 357-368. https:\/\/doi.org\/10.1145\/2813885.2737958 10.1145\/2813885.2737958","DOI":"10.1145\/2813885.2737958"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133974"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359647"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.32"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656446","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656446","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:41:04Z","timestamp":1751661664000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656446"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":50,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656446"],"URL":"https:\/\/doi.org\/10.1145\/3656446","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}