{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T03:48:27Z","timestamp":1780717707872,"version":"3.54.1"},"reference-count":78,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-22-PECY-0006"],"award-info":[{"award-number":["ANR-22-PECY-0006"]}],"id":[{"id":"10.13039\/501100001665","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":[[2023,8,30]]},"abstract":"<jats:p>For all the successes in verifying low-level, efficient, security-critical code, little has been said or studied about the structure, architecture and engineering of such large-scale proof developments.<\/jats:p>\n          <jats:p>We present the design, implementation and evaluation of a set of language-based techniques that allow the programmer to modularly write and verify code at a high level of abstraction, while retaining control over the compilation process and producing high-quality, zero-overhead, low-level code suitable for integration into mainstream software.<\/jats:p>\n          <jats:p>We implement our techniques within the F proof assistant, and specifically its shallowly-embedded Low toolchain that compiles to C. Through our evaluation, we establish that our techniques were critical in scaling the popular HACL library past 100,000 lines of verified source code, and brought about significant gains in proof engineer productivity.<\/jats:p>\n          <jats:p>The exposition of our methodology converges on one final, novel case study: the streaming API, a finicky API that has historically caused many bugs in high-profile software. Using our approach, we manage to capture the streaming semantics in a generic way, and apply it \u201cfor free\u201d to over a dozen use-cases. Six of those have made it into the reference implementation of the Python programming language, replacing the previous CVE-ridden code.<\/jats:p>","DOI":"10.1145\/3607844","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"385-416","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3297-9156","authenticated-orcid":false,"given":"Son","family":"Ho","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2642-543X","authenticated-orcid":false,"given":"Aymeric","family":"Fromherz","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7347-3050","authenticated-orcid":false,"given":"Jonathan","family":"Protzenko","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00028"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980024.2872404"},{"key":"e_1_2_1_5_1","volume-title":"3rd International Workshop on Coq for Programming Languages (CoqPL).","author":"Anand Abhishek","year":"2017","unstructured":"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 3rd International Workshop on Coq for Programming Languages (CoqPL)."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Transactions on Programming Languages and Systems (TOPLAS) April https:\/\/doi.org\/10.1145\/2701415 10.1145\/2701415","DOI":"10.1145\/2701415"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Jean-Philippe Aumasson Samuel Neves Zooko Wilcox-O\u2019Hearn and Christian Winnerlein. 2013. BLAKE2: Simpler Smaller Fast as MD5. In Applied Cryptography and Network Security. 119\u2013135. https:\/\/doi.org\/10.1007\/978-3-642-38980-1_8 10.1007\/978-3-642-38980-1_8","DOI":"10.1007\/978-3-642-38980-1_8"},{"key":"e_1_2_1_9_1","unstructured":"R. Barnes and K. Bhargavan. 2019. Hybrid Public Key Encryption. IRTF Internet-Draft. draft-irtf-cfrg-hpke-02"},{"key":"e_1_2_1_10_1","unstructured":"David Benjamin. 2016. poly1305-x86.pl produces incorrect output. https:\/\/mta.openssl.org\/pipermail\/openssl-dev\/2016-March\/006161"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2831143.2831157"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11502760_3"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11745853_14"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.1"},{"key":"e_1_2_1_15_1","unstructured":"Cliff L. Biffle. 2010. NaCl\/x86 appears to leave return addresses unaligned when returning through the springboard. https:\/\/bugs.chromium.org\/p\/nativeclient\/issues\/detail?id=245"},{"key":"e_1_2_1_16_1","unstructured":"Hanno B\u00f6ck. 2016. Wrong results with Poly1305 functions. https:\/\/mta.openssl.org\/pipermail\/openssl-dev\/2016-March\/006413"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/3241189.3241261"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_1_19_1","unstructured":"Bugzilla. 2019. Crash in Hacl Chacha20Poly1305_128 aead_encrypt & Hacl Chacha20Poly1305_128 aead_decrypt. https:\/\/bugzilla.mozilla.org\/show_bug.cgi?id=1605369"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500592"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_1_23_1","unstructured":"Jason A. Donenfeld. 2018. new 25519 measurements of formally verified implementations. http:\/\/moderncrypto.org\/mail-archive\/curves\/2018\/000972.html"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Morris J Dworkin. 2015. SHA-3 standard: Permutation-based hash and extendable-output functions.","DOI":"10.6028\/NIST.FIPS.202"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00005"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290376"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473590"},{"key":"e_1_2_1_29_1","unstructured":"Paul Futz. 2015. C Preprocessor tricks tips and idioms. https:\/\/github.com\/pfultz2\/Cloak\/wiki\/C-Preprocessor-tricks -tips -and-idioms"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026928"},{"key":"e_1_2_1_32_1","unstructured":"Shay Gueron. 2012. Intel \u00ae Advanced Encryption Standard (AES) New Instructions Set. https:\/\/software.intel.com\/sites\/default\/files\/article\/165683\/aes-wp-2012-09-22-v01.pdf"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ITNG.2014.31"},{"key":"e_1_2_1_34_1","unstructured":"Haskell-crypto. 2022. cryptonite. https:\/\/github.com\/haskell-crypto\/cryptonite"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","unstructured":"Son Ho Aymeric Fromherz and Jonathan Protzenko. 2023. Modularity Code Specialization and Zero-Cost Abstractions for Program Verification. https:\/\/doi.org\/10.5281\/zenodo.8161357 10.5281\/zenodo.8161357","DOI":"10.5281\/zenodo.8161357"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833621"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236773"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535841"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9437-1"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_12"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512670"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30556-9_27"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_49_1","unstructured":"MITRE. 2013. CVE-2014-0160.. http:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2014-0160"},{"key":"e_1_2_1_50_1","unstructured":"MITRE. 2018. CVE-2017-5715. Systems with microprocessors utilizing speculative execution and indirect branch prediction may allow unauthorized disclosure of information to an attacker with local user access via a side-channel analysis.. http:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2017-5715"},{"key":"e_1_2_1_51_1","unstructured":"MITRE. 2018. CVE-2017-5753. Systems with microprocessors utilizing speculative execution and branch prediction may allow unauthorized disclosure of information to an attacker with local user access via a side-channel analysis.. http:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2017-5753"},{"key":"e_1_2_1_52_1","unstructured":"Nicky Mouha. 2022. SHA-3 Buffer Overflow. https:\/\/mouha.be\/sha-3-buffer-overflow\/"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2018.2847247"},{"key":"e_1_2_1_54_1","unstructured":"NIST. 2012. Federal Information Processing Standards Publication 180-4: Secure hash standard (SHS)."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1601.05520"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-72565-9_9"},{"key":"e_1_2_1_57_1","unstructured":"OpenSSL. 2016. Chase overflow bit on x86 and ARM platforms. GitHub commit dc3c5067cd90f3f2159e5d53c57b92730c687d7e."},{"key":"e_1_2_1_58_1","unstructured":"OpenSSL. 2016. Don\u2019t break carry chains. GitHub commit 4b8736a22e758c371bc2f8b3534dc0c274acf42c."},{"key":"e_1_2_1_59_1","unstructured":"OpenSSL. 2016. Don\u2019t loose [sic] 59-th bit. GitHub commit bbe9769ba66ab2512678a87b0d9b266ba970db05."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523706"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_7"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3423352"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","unstructured":"Jonathan Protzenko Jean-Karim Zinzindohou\u00e9 Aseem Rastogi Tahina Ramananandro Peng Wang Santiago Zanella-B\u00e9guelin Antoine Delignat-Lavaud Catalin Hritcu Karthikeyan Bhargavan C\u00e9dric Fournet and Nikhil Swamy. 2017. Verified Low-Level Programming Embedded in F*. PACMPL Sept. https:\/\/doi.org\/10.1145\/3110261 10.1145\/3110261","DOI":"10.1145\/3110261"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.5555\/3361338.3361440"},{"key":"e_1_2_1_66_1","unstructured":"Aseem Rastogi Guido Mart\u00ednez Aymeric Fromherz Tahina Ramananandro and Nikhil Swamy. 2021. Programming and Proving with Indexed Effects. https:\/\/www.fstar-lang.org\/papers\/indexedeffects\/"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000045"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_2_1_69_1","unstructured":"M-J. Saarinen and J-P. Aumasson. 2015. The BLAKE2 Cryptographic Hash and Message Authentication Code (MAC). IETF RFC 7693."},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523708"},{"key":"e_1_2_1_73_1","unstructured":"Forrest Voight. 2012. CVE-2012-2459 (block merkle calculation exploit). https:\/\/bitcointalk.org\/?topic=102395"},{"key":"e_1_2_1_74_1","unstructured":"Guido Vranken. 2019. CryptoFuzz. https:\/\/bugs.chromium.org\/p\/oss-fuzz\/issues\/detail?id=14822#c3"},{"key":"e_1_2_1_75_1","unstructured":"The Wall Street Journal. 2023. Provable Security for Modern Applications. https:\/\/partners.wsj.com\/aws\/reinventing-with-the-cloud\/provable-security-for-modern-applications\/"},{"key":"e_1_2_1_76_1","unstructured":"Henry S Warren. 2013. Hacker\u2019s delight. Pearson Education."},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159877"},{"key":"e_1_2_1_78_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\/3607844","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607844","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:06Z","timestamp":1750178226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607844"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":78,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607844"],"URL":"https:\/\/doi.org\/10.1145\/3607844","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}