{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:59:47Z","timestamp":1750309187331,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T00:00:00Z","timestamp":1704758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Concordium Blockchain Research Center","award":[""],"award-info":[{"award-number":[""]}]},{"name":"Villum Investigator grant","award":["25804"],"award-info":[{"award-number":["25804"]}]},{"name":"Center for Basic Research in Program Verification (CPV)","award":[""],"award-info":[{"award-number":[""]}]},{"name":"the VILLUM Foundation","award":[""],"award-info":[{"award-number":[""]}]},{"name":"German Federal Ministry of Education and Research BMBF","award":["16KISK038"],"award-info":[{"award-number":["16KISK038"]}]},{"name":"Deutsche Forschungsgemeinschaft (DFG, German Research Founda- tion)","award":["EXC 2092 CASA - 390781972"],"award-info":[{"award-number":["EXC 2092 CASA - 390781972"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,1,9]]},"DOI":"10.1145\/3636501.3636961","type":"proceedings-article","created":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T19:39:27Z","timestamp":1704829167000},"page":"30-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography"],"prefix":"10.1145","author":[{"given":"Philipp G.","family":"Haselwarter","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"given":"Benjamin Salling","family":"Hvass","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"given":"Lasse Letager","family":"Hansen","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"given":"Th\u00e9o","family":"Winterhalter","sequence":"additional","affiliation":[{"name":"Inria, Palaiseau, France"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Germany"}]},{"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2024,1,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Th\u00e9o Winterhalter, C\u0103t\u0103lin Hri\u0163cu, Kenji Maillard, and Bas Spitters.","author":"Abate Carmine","year":"2021","unstructured":"Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Th\u00e9o Winterhalter, C\u0103t\u0103lin Hri\u0163cu, Kenji Maillard, and Bas Spitters. 2021. SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. https:\/\/eprint.iacr.org\/2021\/397"},{"key":"e_1_3_2_1_2_1","unstructured":"AbsInt. [n. d.]. Factsheet: CompCert C Compiler. Available at. https:\/\/www.absint.com\/factsheets\/factsheet_compcert_c_web.pdf"},{"key":"e_1_3_2_1_3_1","unstructured":"Reynald Affeldt Cyril Cohen Marie Kerjean Assia Mahboubi Damien Rouhling Kazuhiko Sakaguchi and Pierre-Yves Strub. 2021. mathcomp-analysis. Analysis library compatible with Mathematical Components. https:\/\/github.com\/math-comp\/analysis"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_3_2_1_5_1","volume-title":"The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. In 2020 IEEE Symposium on Security and Privacy (SP). 965\u2013982","author":"Almeida Jos\u00e9 Bacelar","year":"2020","unstructured":"Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Gr\u00e9goire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, and Pierre-Yves Strub. 2020. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. In 2020 IEEE Symposium on Security and Privacy (SP). 965\u2013982."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560689"},{"key":"e_1_3_2_1_7_1","first-page":"1393","article-title":"SoK: Computer-Aided Cryptography","volume":"2019","author":"Barbosa Manuel","year":"2019","unstructured":"Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. 2019. SoK: Computer-Aided Cryptography. IACR Cryptol. ePrint Arch., 2019 (2019), 1393. https:\/\/eprint.iacr.org\/2019\/1393","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"e_1_3_2_1_8_1","unstructured":"Manuel Barbossa Fran\u00e7ois Dupressoir Benjamin Gr\u00e9goire Vincent Laporte Pierre-Yves Strub and Tiago Oliveira. 2022. EasyCrypt and Jasmin Tutorial. https:\/\/formosa-crypto.gitlab.io\/news\/2022-06-07\/sibenik \u0160ibenik"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Benjamin Gr\u00e9goire and Santiago Zanella B\u00e9guelin. 2009. Formal certification of code-based cryptographic proofs. In POPL. 90\u2013101.","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-019-09341-z"},{"key":"e_1_3_2_1_13_1","unstructured":"Mihir Bellare and Phillip Rogaway. 2004. Code-Based Game-Playing Proofs and the Security of Triple Encryption. IACR Cryptol. ePrint Arch. 331. http:\/\/eprint.iacr.org\/2004\/331"},{"volume-title":"Verified Correctness and Security of OpenSSL HMAC. In 24th USENIX Security Symposium. USENIX Association, 207\u2013221","author":"Beringer Lennart","key":"e_1_3_2_1_14_1","unstructured":"Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015. Verified Correctness and Security of OpenSSL HMAC. In 24th USENIX Security Symposium. USENIX Association, 207\u2013221. https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/beringer"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-04762-7_1"},{"key":"e_1_3_2_1_16_1","volume-title":"Vale: Verifying High-Performance Cryptographic Assembly Code. In 26th USENIX Security Symposium, USENIX Security 2017","author":"Bond Barry","year":"2017","unstructured":"Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath T. V. Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In 26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16-18, 2017., Engin Kirda and Thomas Ristenpart (Eds.). USENIX Association, 917\u2013934. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03332-3_9"},{"key":"e_1_3_2_1_18_1","volume-title":"Creusot: A Foundry for the Deductive Verification of Rust Programs","author":"Denis Xavier","year":"2022","unstructured":"Xavier Denis, Jacques-Henri Jourdan, and Claude March\u00e9. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. In Formal Methods and Software Engineering, Adrian Riesco and Min Zhang (Eds.). Springer, 90\u2013105. isbn:978-3-031-17244-1"},{"key":"e_1_3_2_1_19_1","unstructured":"Jason A. Donenfeld. [n. d.]. WireGuard: Formal Verification. Available at. https:\/\/www.wireguard.com\/formal-verification\/"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Morris Dworkin Elaine Barker James Nechvatal James Foti Lawrence Bassham E. Roback and James Dray. 2001. Advanced Encryption Standard (AES). https:\/\/doi.org\/10.6028\/NIST.FIPS.197 10.6028\/NIST.FIPS.197","DOI":"10.6028\/NIST.FIPS.197"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","unstructured":"A. Erbsen J. Philipoom J. Gross R. Sloan and A. Chlipala. 2019. Simple High-Level Code for Cryptographic Arithmetic - With Proofs Without Compromises. In IEEE S&P. https:\/\/doi.org\/10.1109\/SP.2019.00005 10.1109\/SP.2019.00005","DOI":"10.1109\/SP.2019.00005"},{"key":"e_1_3_2_1_22_1","volume-title":"Wood","author":"Faz-Hernandez Armando","year":"2022","unstructured":"Armando Faz-Hernandez, Sam Scott, Nick Sullivan, Riad S. Wahby, and Christopher A. Wood. 2022. Hashing to Elliptic Curves. Internet Engineering Task Force. https:\/\/datatracker.ietf.org\/doc\/draft-irtf-cfrg-hash-to-curve\/16\/ Work in Progress"},{"key":"e_1_3_2_1_23_1","unstructured":"Shay Gueron. 2012. White Paper: Intel\u00ae Advanced Encryption Standard (AES) New Instructions Set. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/tool\/intel-advanced-encryption-standard-aes-instructions-set.html"},{"key":"e_1_3_2_1_24_1","unstructured":"Shai Halevi. 2005. A plausible approach to computer-aided cryptographic proofs. IACR Cryptol. ePrint Arch. 181. http:\/\/eprint.iacr.org\/2005\/181"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3594735"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_1_27_1","volume-title":"Bas Spitters, Manuel Barbosa, Antoine S\u00e9r\u00e9, and Pierre-Yves Strub.","author":"Kiefer Franziskus","year":"2023","unstructured":"Franziskus Kiefer, Karthikeyan Bhargavan, Lucas Franceschino, Denis Merigoux, Lasse Letager Hansen, Bas Spitters, Manuel Barbosa, Antoine S\u00e9r\u00e9, and Pierre-Yves Strub. 2023. HACSPEC: a gateway to high-assurance cryptography. In RWC23."},{"key":"e_1_3_2_1_28_1","volume-title":"ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress.","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert \u2013 a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00018"},{"key":"e_1_3_2_1_30_1","unstructured":"Assia Mahboubi and Enrico Tassi. 2021. Mathematical components. Online book. https:\/\/math-comp.github.io\/mcb\/"},{"key":"e_1_3_2_1_31_1","unstructured":"Denis Merigoux Franziskus Kiefer and Karthikeyan Bhargavan. 2021. hacspec: succinct executable verifiable specifications for high-assurance cryptography embedded in Rust. Inria. https:\/\/hal.inria.fr\/hal-03176482"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"e_1_3_2_1_34_1","unstructured":"Jonathan Protzenko and Bryan Parno. 2019. EverCrypt cryptographic provider offers developers greater security assurances. Microsoft Research Blog. https:\/\/www.microsoft.com\/en-us\/research\/blog\/evercrypt-cryptographic-provider-offers-developers-greater-security-assurances\/"},{"key":"e_1_3_2_1_35_1","unstructured":"Mikkel Milo Rasmus Holdsbjerg-Larsen Bas Spitters. 2022. A Verified Pipeline from a Specification Language to Optimized Safe Rust. CoqPL. https:\/\/cs.au.dk\/~spitters\/CoqPL22.pdf"},{"key":"e_1_3_2_1_36_1","unstructured":"Mike Rosulek. 2021. The Joy of Cryptography. Online textbook. http:\/\/web.engr.oregonstate.edu\/~rosulekm\/crypto\/"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00023"},{"key":"e_1_3_2_1_38_1","unstructured":"Victor Shoup. 2004. Sequences of games: a tool for taming complexity in security proofs. IACR Cryptol. ePrint Arch. 332. http:\/\/eprint.iacr.org\/2004\/332"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2018.00009"},{"key":"e_1_3_2_1_40_1","unstructured":"Juriaan van Drunen. 2021. Calling Jasmin from Rust. https:\/\/gitlab.com\/Jur\/jasminify"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133974"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"event":{"name":"CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"London UK","acronym":"CPP '24"},"container-title":["Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636961","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3636501.3636961","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:11Z","timestamp":1750287251000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636961"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,9]]},"references-count":42,"alternative-id":["10.1145\/3636501.3636961","10.1145\/3636501"],"URL":"https:\/\/doi.org\/10.1145\/3636501.3636961","relation":{},"subject":[],"published":{"date-parts":[[2024,1,9]]},"assertion":[{"value":"2024-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}