{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:32:13Z","timestamp":1767929533987,"version":"3.49.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Department of the Navy, Office of Naval Research","award":["N00014-18-1-2892"],"award-info":[{"award-number":["N00014-18-1-2892"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>High-performance cryptographic libraries often mix code written in a high-level language with code written in assembly. To support formally verifying the correctness and security of such hybrid programs, this paper presents an embedding of a subset of x64 assembly language in F* that allows efficient verification of both assembly and its interoperation with C code generated from F*. The key idea is to use the computational power of a dependent type system's type checker to run a verified verification-condition generator during type checking. This allows the embedding to customize the verification condition sent by the type checker to an SMT solver. By combining our proof-by-reflection style with SMT solving, we demonstrate improved automation for proving the correctness of assembly-language code. This approach has allowed us to complete the first-ever proof of correctness of an optimized implementation of AES-GCM, a cryptographic routine used by 90% of secure Internet traffic.<\/jats:p>","DOI":"10.1145\/3290376","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["A verified, efficient embedding of a verifiable assembly language"],"prefix":"10.1145","volume":"3","author":[{"given":"Aymeric","family":"Fromherz","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Nick","family":"Giannarakis","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}]},{"given":"Chris","family":"Hawblitzel","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research, India"}]},{"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Proceedings of the International Conference on Cryptographic Hardware and Embedded Systems (CHES).","author":"Acii\u00e7mez Onur","year":"2010","unstructured":"Onur Acii\u00e7mez , Billy Bob Brumley , and Philipp Grabher . 2010 . New Results on Instruction Cache Attacks . In Proceedings of the International Conference on Cryptographic Hardware and Embedded Systems (CHES). Onur Acii\u00e7mez, Billy Bob Brumley, and Philipp Grabher. 2010. New Results on Instruction Cache Attacks. In Proceedings of the International Conference on Cryptographic Hardware and Embedded Systems (CHES)."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009867"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.44"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11502760_3"},{"key":"e_1_2_2_7_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_8_1","volume-title":"Proceedings of the USENIX Security Symposium.","author":"Brumley David","year":"2003","unstructured":"David Brumley and Dan Boneh . 2003 . Remote Timing Attacks Are Practical . In Proceedings of the USENIX Security Symposium. David Brumley and Dan Boneh. 2003. Remote Timing Attacks Are Practical. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_2_2_10_1","unstructured":"Adam Chlipala. 2017. Certified Programming with Dependent Types. http:\/\/adam.chlipala.net\/cpdt\/ .   Adam Chlipala. 2017. Certified Programming with Dependent Types. http:\/\/adam.chlipala.net\/cpdt\/ ."},{"key":"e_1_2_2_11_1","unstructured":"Coq Development Team. 2015. The Coq Proof Assistant Reference Manual version 8.5. https:\/\/coq.inria.fr\/distrib\/current\/ refman\/ .  Coq Development Team. 2015. The Coq Proof Assistant Reference Manual version 8.5. https:\/\/coq.inria.fr\/distrib\/current\/ refman\/ ."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_2_2_13_1","volume-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).","author":"de Moura L.","unstructured":"L. de Moura and N. Bj\u00f8rner . 2008. Z3: An efficient SMT solver . In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). L. de Moura and N. Bj\u00f8rner. 2008. Z3: An efficient SMT solver. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)."},{"key":"e_1_2_2_14_1","volume-title":"Without Compromises. In Proceedings of the IEEE Symposium on Security and Privacy.","author":"Erbsen A.","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 Proceedings of the IEEE Symposium on Security and Privacy. A. Erbsen, J. Philipoom, J. Gross, R. Sloan, and A. Chlipala. 2019. Simple High-Level Code for Cryptographic Arithmetic -With Proofs, Without Compromises. In Proceedings of the IEEE Symposium on Security and Privacy."},{"key":"e_1_2_2_15_1","unstructured":"Jean-Christophe Filli\u00e2tre. 2011. Deductive Program Verification. https:\/\/www.lri.fr\/~filliatr\/hdr\/memoire.pdf .  Jean-Christophe Filli\u00e2tre. 2011. Deductive Program Verification. https:\/\/www.lri.fr\/~filliatr\/hdr\/memoire.pdf ."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/648254.752700"},{"key":"e_1_2_2_17_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy.","author":"Goguen J. A.","unstructured":"J. A. Goguen and J. Meseguer . 1982. Security Policies and Security Models . In Proceedings of the IEEE Symposium on Security and Privacy. J. A. Goguen and J. Meseguer. 1982. Security Policies and Security Models. In Proceedings of the IEEE Symposium on Security and Privacy."},{"key":"e_1_2_2_18_1","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"Gordon Michael J. C.","unstructured":"Michael J. C. Gordon . 1989. Current Trends in Hardware Verification and Automated Theorem Proving . Springer-Verlag New York, Inc. , New York, NY, USA , Chapter Mechanizing Programming Logics in Higher Order Logic, 387\u2013439. http:\/\/dl.acm.org\/citation.cfm?id=106971.107122 Michael J. C. Gordon. 1989. Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag New York, Inc., New York, NY, USA, Chapter Mechanizing Programming Logics in Higher Order Logic, 387\u2013439. http:\/\/dl.acm.org\/citation.cfm?id=106971.107122"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_2_2_20_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX Association","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels . In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX Association , Berkeley, CA, USA, 653\u2013669. http: \/\/dl.acm.org\/citation.cfm?id=3026877.3026928 Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX Association, Berkeley, CA, USA, 653\u2013669. http: \/\/dl.acm.org\/citation.cfm?id=3026877.3026928"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_2_22_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 .  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_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_2"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/38.2.131"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505897"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/646761.706156"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_2_28_1","unstructured":"Xavier Leroy Sandrine Blazy Daniel K\u00e4stner Bernhard Schommer Markus Pister and Christian Ferdinand. 2016. CompCert \u2013 A Formally Verified Optimizing Compiler. In Embedded Real Time Software and Systems (ERTS). SEE.  Xavier Leroy Sandrine Blazy Daniel K\u00e4stner Bernhard Schommer Markus Pister and Christian Ferdinand. 2016. CompCert \u2013 A Formally Verified Optimizing Compiler. In Embedded Real Time Software and Systems (ERTS). SEE."},{"key":"e_1_2_2_29_1","volume-title":"Proceedings of the USENIX Security Symposium.","author":"Masti Ramya Jayaram","year":"2015","unstructured":"Ramya Jayaram Masti , Devendra Rai , Aanjhan Ranganathan , Christian M\u00fcller , Lothar Thiele , and Srdjan Capkun . 2015 . Thermal Covert Channels on Multi-core Platforms . In Proceedings of the USENIX Security Symposium. Ramya Jayaram Masti, Devendra Rai, Aanjhan Ranganathan, Christian M\u00fcller, Lothar Thiele, and Srdjan Capkun. 2015. Thermal Covert Channels on Multi-core Platforms. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30556-9_27"},{"key":"e_1_2_2_31_1","unstructured":"Mozilla. 2018. Measurement Dashboard. https:\/\/mzl.la\/2ug9YCH .  Mozilla. 2018. Measurement Dashboard. https:\/\/mzl.la\/2ug9YCH ."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_5"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_35_1","unstructured":"NIST. 2001. Announcing the Advanced Encryption Standard (AES). Federal Information Processing Standards Publication 197.  NIST. 2001. Announcing the Advanced Encryption Standard (AES). Federal Information Processing Standards Publication 197."},{"key":"e_1_2_2_36_1","unstructured":"NIST. 2007. Recommendation for Block Cipher Modes of Operation: Galois\/Counter Mode (GCM) and GMAC. NIST Special Publication 800-38D.  NIST. 2007. Recommendation for Block Cipher Modes of Operation: Galois\/Counter Mode (GCM) and GMAC. NIST Special Publication 800-38D."},{"key":"e_1_2_2_37_1","unstructured":"OpenSSL. 2016a. Chase overflow bit on x86 and ARM platforms. GitHub commit dc3c5067cd90f3f2159e5d53c57b92730c687d7e.  OpenSSL. 2016a. Chase overflow bit on x86 and ARM platforms. GitHub commit dc3c5067cd90f3f2159e5d53c57b92730c687d7e."},{"key":"e_1_2_2_38_1","unstructured":"OpenSSL. 2016b. Don\u2019t break carry chains. GitHub commit 4b8736a22e758c371bc2f8b3534dc0c274acf42c.  OpenSSL. 2016b. Don\u2019t break carry chains. GitHub commit 4b8736a22e758c371bc2f8b3534dc0c274acf42c."},{"key":"e_1_2_2_39_1","unstructured":"OpenSSL. 2016c. Don\u2019t loose {sic} 59-th bit. GitHub commit bbe9769ba66ab2512678a87b0d9b266ba970db05.  OpenSSL. 2016c. Don\u2019t loose {sic} 59-th bit. GitHub commit bbe9769ba66ab2512678a87b0d9b266ba970db05."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062347"},{"key":"e_1_2_2_41_1","unstructured":"Colin Percival. 2005. Cache Missing for Fun and Profit. BSDCan. https:\/\/www.daemonology.net\/papers\/htt.pdf .  Colin Percival. 2005. Cache Missing for Fun and Profit. BSDCan. https:\/\/www.daemonology.net\/papers\/htt.pdf ."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_2_2_45_1","doi-asserted-by":"crossref","unstructured":"Eric Rescorla. 2018. The Transport Layer Security (TLS) Protocol Version 1.3 Draft 28. https:\/\/tools.ietf.org\/html\/ draft- ietf- tls- tls13- 28 .  Eric Rescorla. 2018. The Transport Layer Security (TLS) Protocol Version 1.3 Draft 28. https:\/\/tools.ietf.org\/html\/ draft- ietf- tls- tls13- 28 .","DOI":"10.17487\/RFC8446"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103723"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134076"},{"key":"e_1_2_2_50_1","volume-title":"Proceedings of the International Conference on Cryptographic Hardware and Embedded Systems (CHES).","author":"Yarom Yuval","year":"2010","unstructured":"Yuval Yarom , Daniel Genkin , and Nadia Heninger . 2010 . CacheBleed: A Timing Attack on OpenSSL Constant Time RSA . In Proceedings of the International Conference on Cryptographic Hardware and Embedded Systems (CHES). Yuval Yarom, Daniel Genkin, and Nadia Heninger. 2010. CacheBleed: A Timing Attack on OpenSSL Constant Time RSA. In Proceedings of the International Conference on Cryptographic Hardware and Embedded Systems (CHES)."},{"key":"e_1_2_2_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\/3290376","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290376","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290376"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":49,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290376"],"URL":"https:\/\/doi.org\/10.1145\/3290376","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}