{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T10:08:27Z","timestamp":1781258907704,"version":"3.54.1"},"reference-count":77,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T00:00:00Z","timestamp":1503964800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2017,8,29]]},"abstract":"<jats:p>We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a dependently- typed variant of ML aimed at program verification. Departing from ML, Low* does not involve any garbage collection or implicit heap allocation; instead, it has a structured memory model \u00e0 la CompCert, and it provides the control required for writing efficient low-level security-critical code.<\/jats:p>\n          <jats:p>By virtue of typing, any Low* program is memory safe. In addition, the programmer can make full use of the verification power of F* to write high-level specifications and verify the functional correctness of Low* code using a combination of SMT automation and sophisticated manual proofs. At extraction time, specifications and proofs are erased, and the remaining code enjoys a predictable translation to C. We prove that this translation preserves semantics and side-channel resistance.<\/jats:p>\n          <jats:p>We provide a new compiler back-end from Low* to C and, to evaluate our approach, we implement and verify various cryptographic algorithms, constructions, and tools for a total of about 28,000 lines of code. We show that our Low* code delivers performance competitive with existing (unverified) C cryptographic libraries, suggesting our approach may be applicable to larger-scale low-level software.<\/jats:p>","DOI":"10.1145\/3110261","type":"journal-article","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T18:19:41Z","timestamp":1504030781000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":83,"title":["Verified low-level programming embedded in F*"],"prefix":"10.1145","volume":"1","author":[{"given":"Jonathan","family":"Protzenko","sequence":"first","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Karim","family":"Zinzindohou\u00e9","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tahina","family":"Ramananandro","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peng","family":"Wang","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Santiago","family":"Zanella-B\u00e9guelin","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antoine","family":"Delignat-Lavaud","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Karthikeyan","family":"Bhargavan","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9dric","family":"Fournet","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2008\u20132017. The Sodium crypto library (libsodium). (2008\u20132017). https:\/\/www.gitbook.com\/book\/jedisct1\/libsodium\/details  2008\u20132017. The Sodium crypto library (libsodium). (2008\u20132017). https:\/\/www.gitbook.com\/book\/jedisct1\/libsodium\/details"},{"key":"e_1_2_2_2_1","unstructured":"2010\u20132017. The Rust Programming Language. (2010\u20132017). https:\/\/www.rust- lang.org  2010\u20132017. The Rust Programming Language. (2010\u20132017). https:\/\/www.rust- lang.org"},{"key":"e_1_2_2_3_1","volume-title":"ChaCha20\/Poly1305 heap-buffer-overflow. (Nov","year":"2016","unstructured":"2016. CVE-2016-7054 : ChaCha20\/Poly1305 heap-buffer-overflow. (Nov . 2016 ). http:\/\/cve.mitre.org\/cgi- bin\/cvename.cgi? name=CVE- 2016- 7054 2016. CVE-2016-7054: ChaCha20\/Poly1305 heap-buffer-overflow. (Nov. 2016). http:\/\/cve.mitre.org\/cgi- bin\/cvename.cgi? name=CVE- 2016- 7054"},{"key":"e_1_2_2_4_1","unstructured":"2017. Common Weakness Enumeration (CWE-190: Integer Overflow or Wraparound). (2017). https:\/\/cwe.mitre.org\/data\/ definitions\/190.html  2017. Common Weakness Enumeration (CWE-190: Integer Overflow or Wraparound). (2017). https:\/\/cwe.mitre.org\/data\/ definitions\/190.html"},{"key":"e_1_2_2_5_1","unstructured":"2017. Common Weakness Enumeration (CWE-415: Double Free). (2017). http:\/\/cwe.mitre.org\/data\/definitions\/415.html  2017. Common Weakness Enumeration (CWE-415: Double Free). (2017). http:\/\/cwe.mitre.org\/data\/definitions\/415.html"},{"key":"e_1_2_2_6_1","unstructured":"2017. Common Weakness Enumeration (CWE-416: Use After Free). (2017). http:\/\/cwe.mitre.org\/data\/definitions\/416.html  2017. Common Weakness Enumeration (CWE-416: Use After Free). (2017). http:\/\/cwe.mitre.org\/data\/definitions\/416.html"},{"key":"e_1_2_2_7_1","unstructured":"J. Afek and A. Sharabani. 2007. Dangling Pointer \u2013 Smashing The Pointer For Fun And Profit. BlackHat USA. (July 2007).  J. Afek and A. Sharabani. 2007. Dangling Pointer \u2013 Smashing The Pointer For Fun And Profit. BlackHat USA. (July 2007)."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.42"},{"key":"e_1_2_2_10_1","volume-title":"FSE","author":"Almeida Jos\u00e9 Bacelar","year":"2016","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , and Fran\u00e7ois Dupressoir . 2016 a. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. In Fast Software Encryption - 23rd International Conference , FSE 2016. 163\u2013184. Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and Fran\u00e7ois Dupressoir. 2016a. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. In Fast Software Encryption - 23rd International Conference, FSE 2016. 163\u2013184."},{"key":"e_1_2_2_11_1","first-page":"53","article-title":"Verifying ConstantTime Implementations. In 25th USENIX Security Symposium","volume":"16","author":"Almeida Jos\u00e9 Bacelar","year":"2016","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Fran\u00e7ois Dupressoir , and Michael Emmi . 2016 b. Verifying ConstantTime Implementations. In 25th USENIX Security Symposium , USENIX Security 16. 53 \u2013 70 . Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Fran\u00e7ois Dupressoir, and Michael Emmi. 2016b. Verifying ConstantTime Implementations. In 25th USENIX Security Symposium, USENIX Security 16. 53\u201370.","journal-title":"USENIX Security"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Nada Amin and Tiark Rompf. 2017. LMS-Verify: Abstraction without Regret for Verified Systems Programming. To appear in 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201917). (2017). https: \/\/www.cs.purdue.edu\/homes\/rompf\/papers\/amin- draft2016b.pdf  Nada Amin and Tiark Rompf. 2017. LMS-Verify: Abstraction without Regret for Verified Systems Programming. To appear in 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201917). (2017). https: \/\/www.cs.purdue.edu\/homes\/rompf\/papers\/amin- draft2016b.pdf","DOI":"10.1145\/3009837.3009867"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_2_2_15_1","volume-title":"System-level Noninterference for Constant-time Cryptography. In 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS","author":"Barthe Gilles","year":"2014","unstructured":"Gilles Barthe , Gustavo Betarte , Juan Diego Campo , Carlos Daniel Luna , and David Pichardie . 2014 . System-level Noninterference for Constant-time Cryptography. In 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS 2014. 1267\u20131279. Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, and David Pichardie. 2014. System-level Noninterference for Constant-time Cryptography. In 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS 2014. 1267\u20131279."},{"key":"e_1_2_2_16_1","unstructured":"David Benjamin. 2016. poly1305-x86.pl produces incorrect output. https:\/\/mta.openssl.org\/pipermail\/openssl- dev\/ 2016- March\/006161 . (2016).  David Benjamin. 2016. poly1305-x86.pl produces incorrect output. https:\/\/mta.openssl.org\/pipermail\/openssl- dev\/ 2016- March\/006161 . (2016)."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/582419.582421"},{"key":"e_1_2_2_18_1","volume-title":"24th USENIX Security Symposium (USENIX Security 15)","author":"Beringer Lennart","year":"2015","unstructured":"Lennart Beringer , Adam Petcher , Q Ye Katherine , and Andrew W Appel . 2015 . Verified correctness and security of OpenSSL HMAC . In 24th USENIX Security Symposium (USENIX Security 15) . 207\u2013221. Lennart Beringer, Adam Petcher, Q Ye Katherine, and Andrew W Appel. 2015. Verified correctness and security of OpenSSL HMAC. In 24th USENIX Security Symposium (USENIX Security 15). 207\u2013221."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11502760_3"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11745853_14"},{"key":"e_1_2_2_21_1","volume-title":"New stream cipher designs","author":"Bernstein Daniel J","unstructured":"Daniel J Bernstein . 2008. The Salsa20 family of stream ciphers . In New stream cipher designs . Springer , 84\u201397. Daniel J Bernstein. 2008. The Salsa20 family of stream ciphers. In New stream cipher designs. Springer, 84\u201397."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33481-8_9"},{"key":"e_1_2_2_23_1","volume-title":"International Conference on Cryptology and Information Security in Latin America, LATINCRYPT","author":"Bernstein Daniel J","year":"2014","unstructured":"Daniel J Bernstein , Bernard Van Gastel , Wesley Janssen , Tanja Lange , Peter Schwabe , and Sjaak Smetsers . 2014 . TweetNaCl: A crypto library in 100 tweets . In International Conference on Cryptology and Information Security in Latin America, LATINCRYPT 2014. 64\u201383. Daniel J Bernstein, Bernard Van Gastel, Wesley Janssen, Tanja Lange, Peter Schwabe, and Sjaak Smetsers. 2014. TweetNaCl: A crypto library in 100 tweets. In International Conference on Cryptology and Information Security in Latin America, LATINCRYPT 2014. 64\u201383."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.14"},{"key":"e_1_2_2_25_1","volume-title":"Santiago Zanella B\u00e9guelin, and Jean Karim Zinzindohoue","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan , Antoine Delignat-Lavaud , C\u00e9dric Fournet , Markulf Kohlweiss , Jianyang Pan , Jonathan Protzenko , Aseem Rastogi , Nikhil Swamy , Santiago Zanella B\u00e9guelin, and Jean Karim Zinzindohoue . 2017 . Implementing and Proving the TLS 1.3 Record Layer. IEEE Security &amp; Privacy ( 2017). Karthikeyan Bhargavan, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella B\u00e9guelin, and Jean Karim Zinzindohoue. 2017. Implementing and Proving the TLS 1.3 Record Layer. IEEE Security &amp; Privacy (2017)."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.37"},{"key":"e_1_2_2_27_1","volume-title":"Advances in Cryptology\u2013CRYPTO","author":"Bhargavan Karthikeyan","year":"2014","unstructured":"Karthikeyan Bhargavan , C\u00e9dric Fournet , Markulf Kohlweiss , Alfredo Pironti , Pierre-Yves Strub , and Santiago ZanellaB\u00e9guelin . 2014. Proving the TLS handshake secure (as it is) . In Advances in Cryptology\u2013CRYPTO 2014 . Springer , 235\u2013255. Karthikeyan Bhargavan, C\u00e9dric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, and Santiago ZanellaB\u00e9guelin. 2014. Proving the TLS handshake secure (as it is). In Advances in Cryptology\u2013CRYPTO 2014. Springer, 235\u2013255."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_2_2_30_1","unstructured":"Hanno B\u00f6ck. 2016. Wrong results with Poly1305 functions. https:\/\/mta.openssl.org\/pipermail\/openssl- dev\/2016- March\/ 006413 . (2016).  Hanno B\u00f6ck. 2016. Wrong results with Poly1305 functions. https:\/\/mta.openssl.org\/pipermail\/openssl- dev\/2016- March\/ 006413 . (2016)."},{"key":"e_1_2_2_32_1","volume-title":"Proceedings of the USENIX Security Symposium.","author":"Bond Barry","year":"2017","unstructured":"Barry Bond , Chris Hawblitzel , Manos Kapritsos , K. Rustan M. Leino , Jacob R. Lorch , Bryan Parno , Ashay Rane , Srinath Setty , and Laure Thompson . 2017 . Vale: Verifying High-Performance Cryptographic Assembly Code . In Proceedings of the USENIX Security Symposium. Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660370"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_35"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_39_1","volume-title":"Exploit for CVS double free() for Linux pserver. (Feb","author":"Dobrovitski I.","year":"2003","unstructured":"I. Dobrovitski . 2003. Exploit for CVS double free() for Linux pserver. (Feb . 2003 ). http:\/\/archives.neohapsis.com\/archives\/ fulldisclosure\/2003- q1\/0545.html I. Dobrovitski. 2003. Exploit for CVS double free() for Linux pserver. (Feb. 2003). http:\/\/archives.neohapsis.com\/archives\/ fulldisclosure\/2003- q1\/0545.html"},{"key":"e_1_2_2_41_1","volume-title":"Part one: Verifying s2n HMAC with SAW. Galois Blog. (Sept","author":"Dodds Joey","year":"2016","unstructured":"Joey Dodds . 2016. Part one: Verifying s2n HMAC with SAW. Galois Blog. (Sept . 2016 ). https:\/\/galois.com\/blog\/2016\/09\/ specifying- hmac- in- cryptol\/ Joey Dodds. 2016. Part one: Verifying s2n HMAC with SAW. Galois Blog. (Sept. 2016). https:\/\/galois.com\/blog\/2016\/09\/ specifying- hmac- in- cryptol\/"},{"key":"e_1_2_2_42_1","volume-title":"Here Come The \u2295 Ninjas.","author":"Duong Thai","year":"2011","unstructured":"Thai Duong and Juliano Rizzo . 2011. Here Come The \u2295 Ninjas. Available at http:\/\/nerdoholic.org\/uploads\/dergln\/beast_ part2\/ssl_jun21.pdf . ( May 2011 ). Thai Duong and Juliano Rizzo. 2011. Here Come The \u2295 Ninjas. Available at http:\/\/nerdoholic.org\/uploads\/dergln\/beast_ part2\/ssl_jun21.pdf . (May 2011)."},{"key":"e_1_2_2_43_1","unstructured":"Anthony Green. 2014. The libffi home page. (2014). http:\/\/sourceware.org\/libffi  Anthony Green. 2014. The libffi home page. (2014). http:\/\/sourceware.org\/libffi"},{"key":"e_1_2_2_44_1","volume-title":"Bridging the Gap: Automatic Verified Abstraction of C. In 3rd International Conference on Interactive Theorem Proving, ITP 2012 (Lecture Notes in Computer Science)","volume":"7406","author":"Greenaway David","year":"2012","unstructured":"David Greenaway , June Andronick , and Gerwin Klein . 2012 . Bridging the Gap: Automatic Verified Abstraction of C. In 3rd International Conference on Interactive Theorem Proving, ITP 2012 (Lecture Notes in Computer Science) , Vol. 7406 . Springer, 99\u2013115. David Greenaway, June Andronick, and Gerwin Klein. 2012. Bridging the Gap: Automatic Verified Abstraction of C. In 3rd International Conference on Interactive Theorem Proving, ITP 2012 (Lecture Notes in Computer Science), Vol. 7406. Springer, 99\u2013115."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594296"},{"key":"e_1_2_2_46_1","unstructured":"Heartbleed. 2014. The Heartbleed Bug. http:\/\/heartbleed.com\/ . (2014).  Heartbleed. 2014. The Heartbleed Bug. http:\/\/heartbleed.com\/ . (2014)."},{"key":"e_1_2_2_47_1","volume-title":"Department of Computer Science, KU Leuven - University of Leuven, Belgium.","author":"Jacobs Bart","year":"2014","unstructured":"Bart Jacobs , Jan Smans , and Frank Piessens . 2014. The VeriFast Program Verifier: A Tutorial. iMinds-DistriNet , Department of Computer Science, KU Leuven - University of Leuven, Belgium. ( 2014 ). https:\/\/people.cs.kuleuven.be\/~bart.jacobs\/ verifast\/tutorial.pdf Bart Jacobs, Jan Smans, and Frank Piessens. 2014. The VeriFast Program Verifier: A Tutorial. iMinds-DistriNet, Department of Computer Science, KU Leuven - University of Leuven, Belgium. (2014). https:\/\/people.cs.kuleuven.be\/~bart.jacobs\/ verifast\/tutorial.pdf"},{"key":"e_1_2_2_48_1","volume-title":"USENIX Annual Technical Conference, General Track. 275\u2013288","author":"Jim Trevor","year":"2002","unstructured":"Trevor Jim , J Gregory Morrisett , Dan Grossman , Michael W Hicks , James Cheney , and Yanling Wang . 2002 . Cyclone: A Safe Dialect of C .. In USENIX Annual Technical Conference, General Track. 275\u2013288 . Trevor Jim, J Gregory Morrisett, Dan Grossman, Michael W Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A Safe Dialect of C.. In USENIX Annual Technical Conference, General Track. 275\u2013288."},{"key":"e_1_2_2_49_1","volume-title":"24th USENIX Security Symposium (USENIX Security 15)","author":"Kaloper-Mer\u0161injak David","year":"2015","unstructured":"David Kaloper-Mer\u0161injak , Hannes Mehnert , Anil Madhavapeddy , and Peter Sewell . 2015 . Not-quite-so-broken TLS: Lessons in re-engineering a security protocol specification and implementation . In 24th USENIX Security Symposium (USENIX Security 15) . 223\u2013238. David Kaloper-Mer\u0161injak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. 2015. Not-quite-so-broken TLS: Lessons in re-engineering a security protocol specification and implementation. In 24th USENIX Security Symposium (USENIX Security 15). 223\u2013238."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68697-5_9"},{"key":"e_1_2_2_53_1","unstructured":"Xavier Leroy. 2004\u20132016. The CompCert C verified compiler. http:\/\/compcert.inria.fr\/ . (2004\u20132016).  Xavier Leroy. 2004\u20132016. The CompCert C verified compiler. http:\/\/compcert.inria.fr\/ . (2004\u20132016)."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_55_1","unstructured":"Xavier Leroy Andrew W. Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2. Research report RR-7987. INRIA. http:\/\/hal.inria.fr\/hal- 00703441  Xavier Leroy Andrew W. Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2. Research report RR-7987. INRIA. http:\/\/hal.inria.fr\/hal- 00703441"},{"key":"e_1_2_2_56_1","volume-title":"Types for proofs and programs","author":"Letouzey Pierre","unstructured":"Pierre Letouzey . 2002. A new extraction for Coq . In Types for proofs and programs . Springer , 200\u2013219. Pierre Letouzey. 2002. A new extraction for Coq. In Types for proofs and programs. Springer, 200\u2013219."},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_2_59_1","volume-title":"IFIP Congress. 21\u201328","author":"McCarthy John","year":"1962","unstructured":"John McCarthy . 1962 . Towards a Mathematical Science of Computation . In IFIP Congress. 21\u201328 . John McCarthy. 1962. Towards a Mathematical Science of Computation. In IFIP Congress. 21\u201328."},{"key":"e_1_2_2_60_1","volume-title":"Everest: VERifiEd Secure Transport. https:\/\/project- everest.github.io\/ .","author":"Research Microsoft","year":"2016","unstructured":"Microsoft Research and INRIA. 2016 . Everest: VERifiEd Secure Transport. https:\/\/project- everest.github.io\/ . (2016). Microsoft Research and INRIA. 2016. Everest: VERifiEd Secure Transport. https:\/\/project- everest.github.io\/ . (2016)."},{"key":"e_1_2_2_61_1","unstructured":"Bodo M\u00f6ller Thai Duong and Krzysztof Kotowicz. 2014. This POODLE Bites: Exploiting The SSL 3.0 Fallback. Available at https:\/\/www.openssl.org\/~bodo\/ssl- poodle.pdf . (2014).  Bodo M\u00f6ller Thai Duong and Krzysztof Kotowicz. 2014. This POODLE Bites: Exploiting The SSL 3.0 Fallback. Available at https:\/\/www.openssl.org\/~bodo\/ssl- poodle.pdf . (2014)."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/11734727_14"},{"key":"e_1_2_2_63_1","doi-asserted-by":"crossref","unstructured":"Yoav Nir and Adam Langley. 2015. ChaCha20 and Poly1305 for IETF Protocols. IETF RFC 7539. (2015).  Yoav Nir and Adam Langley. 2015. ChaCha20 and Poly1305 for IETF Protocols. IETF RFC 7539. (2015).","DOI":"10.17487\/RFC7539"},{"key":"e_1_2_2_64_1","unstructured":"OpenSSL library. 1998\u20132017. OpenSSL: Cryptography and SSL\/TLS Toolkit. (1998\u20132017). https:\/\/www.openssl.org\/  OpenSSL library. 1998\u20132017. OpenSSL: Cryptography and SSL\/TLS Toolkit. (1998\u20132017). https:\/\/www.openssl.org\/"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2004.36"},{"key":"e_1_2_2_66_1","unstructured":"Jonathan Protzenko. 2017. The KreMLin compiler. (2017). https:\/\/www.github.com\/FStarLang\/kremlin  Jonathan Protzenko. 2017. The KreMLin compiler. (2017). https:\/\/www.github.com\/FStarLang\/kremlin"},{"key":"e_1_2_2_67_1","volume-title":"The CRIME Attack. (September","author":"Rizzo Julian","year":"2012","unstructured":"Julian Rizzo and Thai Duong . 2012. The CRIME Attack. (September 2012 ). Julian Rizzo and Thai Duong. 2012. The CRIME Attack. (September 2012)."},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978411"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.5555\/3081770.3081788"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_73_1","unstructured":"Robert \u015awi\u0119cki. 2016. ChaCha20\/Poly1305 heap-buffer-overflow. CVE-2016-7054. (2016).  Robert \u015awi\u0119cki. 2016. ChaCha20\/Poly1305 heap-buffer-overflow. CVE-2016-7054. (2016)."},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.13"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2016.125"},{"key":"e_1_2_2_78_1","volume-title":"2nd USENIX Workshop on Electronic Commerce, WOEC","author":"Wagner David","year":"1996","unstructured":"David Wagner and Bruce Schneier . 1996 . Analysis of the SSL 3.0 Protocol . In 2nd USENIX Workshop on Electronic Commerce, WOEC 1996. 29\u201340. David Wagner and Bruce Schneier. 1996. Analysis of the SSL 3.0 Protocol. In 2nd USENIX Workshop on Electronic Commerce, WOEC 1996. 29\u201340."},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_34"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462164"},{"key":"e_1_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.28"},{"key":"e_1_2_2_84_1","doi-asserted-by":"crossref","unstructured":"Jean-Karim Zinzindohou\u00e9 Karthikeyan Bhargavan and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. (2017). https:\/\/www.github.com\/mitls\/hacl- star  Jean-Karim Zinzindohou\u00e9 Karthikeyan Bhargavan and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. (2017). https:\/\/www.github.com\/mitls\/hacl- star","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\/3110261","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110261","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:44Z","timestamp":1750221524000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110261"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,29]]},"references-count":77,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2017,8,29]]}},"alternative-id":["10.1145\/3110261"],"URL":"https:\/\/doi.org\/10.1145\/3110261","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,29]]},"assertion":[{"value":"2017-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}