{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:24:10Z","timestamp":1770294250891,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,30]],"date-time":"2020-10-30T00:00:00Z","timestamp":1604016000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["683032 - CIRCUS"],"award-info":[{"award-number":["683032 - CIRCUS"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,30]]},"DOI":"10.1145\/3372297.3423352","type":"proceedings-article","created":{"date-parts":[[2021,3,4]],"date-time":"2021-03-04T16:20:42Z","timestamp":1614874842000},"page":"899-918","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms)"],"prefix":"10.1145","author":[{"given":"Marina","family":"Polubelova","sequence":"first","affiliation":[{"name":"Inria Paris, Paris, France"}]},{"given":"Karthikeyan","family":"Bhargavan","sequence":"additional","affiliation":[{"name":"Inria Paris, Paris, France"}]},{"given":"Jonathan","family":"Protzenko","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}]},{"given":"Benjamin","family":"Beurdouche","sequence":"additional","affiliation":[{"name":"Inria Paris & Mozilla, Paris, France"}]},{"given":"Aymeric","family":"Fromherz","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}]},{"given":"Natalia","family":"Kulatova","sequence":"additional","affiliation":[{"name":"Inria Paris, Paris, France"}]},{"given":"Santiago","family":"Zanella-B\u00e9guelin","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2020,11,2]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"2012. Federal Information Processing Standards Publication 180-4: Secure hashstandard (SHS). NIST.  2012. Federal Information Processing Standards Publication 180-4: Secure hashstandard (SHS). NIST."},{"key":"e_1_3_2_2_2_1","unstructured":"2015. ChaCha20 and Poly1305 for IETF Protocols. IETF RFC 7539.  2015. ChaCha20 and Poly1305 for IETF Protocols. IETF RFC 7539."},{"key":"e_1_3_2_2_3_1","unstructured":"2017. BLAKE2b NEON suffers poor performance on ARMv8\/Aarch64 withCortex-A57. https:\/\/github.com\/weidai11\/cryptopp\/issues\/367.  2017. BLAKE2b NEON suffers poor performance on ARMv8\/Aarch64 withCortex-A57. https:\/\/github.com\/weidai11\/cryptopp\/issues\/367."},{"key":"e_1_3_2_2_4_1","unstructured":"2017. On the dangers of Intel's frequency scaling. https:\/\/blog.cloudflare.com\/on-the-dangers-of-intels-frequency-scaling\/.  2017. On the dangers of Intel's frequency scaling. https:\/\/blog.cloudflare.com\/on-the-dangers-of-intels-frequency-scaling\/."},{"key":"e_1_3_2_2_5_1","unstructured":"2020. eBACS: ECRYPT Benchmarking of Cryptographic Systems ? SUPERCOP. https:\/\/bench.cr.yp.to\/supercop.html.  2020. eBACS: ECRYPT Benchmarking of Cryptographic Systems ? SUPERCOP. https:\/\/bench.cr.yp.to\/supercop.html."},{"key":"e_1_3_2_2_6_1","unstructured":"2020. WebAssembly 128-bit packed SIMD Extension. https:\/\/github.com\/WebAssembly\/simd\/blob\/master\/proposals\/simd\/SIMD.md W3C.  2020. WebAssembly 128-bit packed SIMD Extension. https:\/\/github.com\/WebAssembly\/simd\/blob\/master\/proposals\/simd\/SIMD.md W3C."},{"key":"e_1_3_2_2_7_1","volume-title":"Jasmin: High-Assurance and High-Speed Cryptography. https:\/\/doi.org\/10.1145\/3133956.3134078","author":"Almeida Jos\u00e9 Bacelar","year":"2017","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Arthur Blot , Benjamin Gr\u00e9goire , Vincent Laporte , Tiago Oliveira , Hugo Pacheco , Benedikt Schmidt , and Pierre-Yves Strub . 2017 . Jasmin: High-Assurance and High-Speed Cryptography. https:\/\/doi.org\/10.1145\/3133956.3134078 10.1145\/3133956.3134078 Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Gr\u00e9goire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-Assurance and High-Speed Cryptography. https:\/\/doi.org\/10.1145\/3133956.3134078"},{"key":"e_1_3_2_2_8_1","volume-title":"The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. In IEEE Symposium on Security and Privacy. 965--982","author":"Almeida Jos\u00e9 Bacelar","year":"2020","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Benjamin Gr\u00e9 goire, Adrien Koutsos , Vincent Laporte , Tiago Oliveira , and Pierre-Yves Strub . 2020 . The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. In IEEE Symposium on Security and Privacy. 965--982 . Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Gr\u00e9 goire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, and Pierre-Yves Strub. 2020. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. In IEEE Symposium on Security and Privacy. 965--982."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Bacelar Almeida Manuel Barbosa Gilles Barthe Laporte Vincent and Oliveira Tiago. 2019. Certified Compilers in Supercop: Extended x86 Instructions and Constant-Time Verification. (2019).  Jos\u00e9 Bacelar Almeida Manuel Barbosa Gilles Barthe Laporte Vincent and Oliveira Tiago. 2019. Certified Compilers in Supercop: Extended x86 Instructions and Constant-Time Verification. (2019).","DOI":"10.1007\/978-3-030-65277-7_6"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Jean-Philippe Aumasson Samuel Neves Zooko Wilcox-O'Hearn and Christian Winnerlein. 2013. BLAKE2: Simpler Smaller Fast as MD5. In Applied Cryptography and Network Security. 119--135.  Jean-Philippe Aumasson Samuel Neves Zooko Wilcox-O'Hearn and Christian Winnerlein. 2013. BLAKE2: Simpler Smaller Fast as MD5. In Applied Cryptography and Network Security. 119--135.","DOI":"10.1007\/978-3-642-38980-1_8"},{"key":"e_1_3_2_2_13_1","unstructured":"R. Barnes B. Beurdouche J. Millican E. Omara K. Cohn-Gordon and R. Robert. 2020. The Messaging Layer Security (MLS) Protocol. IETF Internet-Draft draft-ietf-mls-protocol-09.  R. Barnes B. Beurdouche J. Millican E. Omara K. Cohn-Gordon and R. Robert. 2020. The Messaging Layer Security (MLS) Protocol. IETF Internet-Draft draft-ietf-mls-protocol-09."},{"key":"e_1_3_2_2_14_1","unstructured":"R. Barnes and K. Bhargavan. 2019. Hybrid Public Key Encryption. IRTF Internet-Draft draft-irtf-cfrg-hpke-02.  R. Barnes and K. Bhargavan. 2019. Hybrid Public Key Encryption. IRTF Internet-Draft draft-irtf-cfrg-hpke-02."},{"key":"e_1_3_2_2_15_1","volume-title":"Proceedings of the ACM on Programming Languages","volume":"4","author":"Barthe Gilles","year":"2019","unstructured":"Gilles Barthe , Sandrine Blazy , Benjamin Gr\u00e9goire , R\u00e9mi Hutin , Vincent Laporte , David Pichardie , and Alix Trieu . 2019 . Formal verification of a constant-time preserving C compiler . Proceedings of the ACM on Programming Languages , Vol. 4 , POPL (2019), 1--30. Gilles Barthe, Sandrine Blazy, Benjamin Gr\u00e9goire, R\u00e9mi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. 2019. Formal verification of a constant-time preserving C compiler. Proceedings of the ACM on Programming Languages, Vol. 4, POPL (2019), 1--30."},{"key":"e_1_3_2_2_16_1","unstructured":"David Benjamin. 2016. poly1305-x86.pl produces incorrect output. https:\/\/mta.openssl.org\/pipermail\/openssl-dev\/2016-March\/006161.  David Benjamin. 2016. poly1305-x86.pl produces incorrect output. https:\/\/mta.openssl.org\/pipermail\/openssl-dev\/2016-March\/006161."},{"key":"e_1_3_2_2_17_1","volume-title":"Verified Correctness and Security of OpenSSL HMAC. In USENIX Security Symposium. 207--221","author":"Beringer Lennart","unstructured":"Lennart Beringer , Adam Petcher , Katherine Q. Ye , and Andrew W. Appel . 2015 . Verified Correctness and Security of OpenSSL HMAC. In USENIX Security Symposium. 207--221 . Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015. Verified Correctness and Security of OpenSSL HMAC. In USENIX Security Symposium. 207--221."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11502760_3"},{"key":"e_1_3_2_2_19_1","volume-title":"Bernstein and Peter Schwabe","author":"Daniel","year":"2012","unstructured":"Daniel J. Bernstein and Peter Schwabe . 2012 . NEON Crypto. In Cryptographic Hardware and Embedded Systems (CHES) . 320--339. Daniel J. Bernstein and Peter Schwabe. 2012. NEON Crypto. In Cryptographic Hardware and Embedded Systems (CHES). 320--339."},{"key":"e_1_3_2_2_20_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_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_2_23_1","unstructured":"Jason A. Donenfeld. 2018. kBench9000 - simple kernel land cycle counter. https:\/\/git.zx2c4.com\/kbench9000\/about\/.  Jason A. Donenfeld. 2018. kBench9000 - simple kernel land cycle counter. https:\/\/git.zx2c4.com\/kbench9000\/about\/."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Morris J. Dworkin. 2001. SP 800--38A 2001 Edition. Recommendation for Block Cipher Modes of Operation: Methods and Techniques. NIST.  Morris J. Dworkin. 2001. SP 800--38A 2001 Edition. Recommendation for Block Cipher Modes of Operation: Methods and Techniques. NIST.","DOI":"10.6028\/NIST.SP.800-38a"},{"key":"e_1_3_2_2_25_1","volume-title":"Without Compromises. In 2019 IEEE Symposium on Security and Privacy, SP 2019","author":"Erbsen Andres","year":"2019","unstructured":"Andres Erbsen , Jade Philipoom , Jason Gross , Robert Sloan , and Adam Chlipala . 2019 . Simple High-Level Code for Cryptographic Arithmetic - With Proofs , Without Compromises. In 2019 IEEE Symposium on Security and Privacy, SP 2019 , San Francisco, CA, USA, May 19--23 , 2019. IEEE, 1202--1219. Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. In 2019 IEEE Symposium on Security and Privacy, SP 2019, San Francisco, CA, USA, May 19--23, 2019. IEEE, 1202--1219."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290376"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3354199"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.4236\/jis.2012.34039"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236773"},{"key":"e_1_3_2_2_30_1","unstructured":"Xavier Leroy Sandrine Blazy Daniel K\"astner Bernhard Schommer Markus Pister and Christian Ferdinand. 2016. CompCert -- A Formally Verified Optimizing Compiler. In Embedded Real Time Software and Systems (ERTS). SEE.  Xavier Leroy Sandrine Blazy Daniel K\"astner Bernhard Schommer Markus Pister and Christian Ferdinand. 2016. CompCert -- A Formally Verified Optimizing Compiler. In Embedded Real Time Software and Systems (ERTS). SEE."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00064"},{"key":"e_1_3_2_2_34_1","volume-title":"2020 IEEE Symposium on Security and Privacy (SP). 634--653","author":"Protzenko Jonathan","year":"2019","unstructured":"Jonathan Protzenko , Bryan Parno , Aymeric Fromherz , Chris Hawblitzel , Marina Polubelova , Karthikeyan Bhargavan , Benjamin Beurdouche , Joonwon Choi , Antoine Delignat-Lavaud , C\u00e9dric Fournet , 2019 b. Evercrypt: A fast, verified, cross-platform cryptographic provider . In 2020 IEEE Symposium on Security and Privacy (SP). 634--653 . Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, C\u00e9dric Fournet, et al. 2019 b. Evercrypt: A fast, verified, cross-platform cryptographic provider. In 2020 IEEE Symposium on Security and Privacy (SP). 634--653."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_2_36_1","unstructured":"E. Rescorla K. Oku N. Sullivan and C.A. Wood. 2020. Encrypted Server Name Indication for TLS 1.3. IETF Internet-Draft draft-ietf-tls-esni-06.  E. Rescorla K. Oku N. Sullivan and C.A. Wood. 2020. Encrypted Server Name Indication for TLS 1.3. IETF Internet-Draft draft-ietf-tls-esni-06."},{"key":"e_1_3_2_2_37_1","unstructured":"M-J. Saarinen and J-P. Aumasson. 2015. The BLAKE2 Cryptographic Hash and Message Authentication Code (MAC). IETF RFC 7693.  M-J. Saarinen and J-P. Aumasson. 2015. The BLAKE2 Cryptographic Hash and Message Authentication Code (MAC). IETF RFC 7693."},{"key":"e_1_3_2_2_38_1","volume-title":"Template Meta-Programming for Haskell (Haskell '02)","author":"Sheard Tim","year":"2002","unstructured":"Tim Sheard and Simon Peyton Jones . 2002 . Template Meta-Programming for Haskell (Haskell '02) . 1--16. Tim Sheard and Simon Peyton Jones. 2002. Template Meta-Programming for Haskell (Haskell '02). 1--16."},{"key":"e_1_3_2_2_39_1","volume-title":"IEEE European Symposium on Security and Privacy. 1--15","author":"Simon Laurent","unstructured":"Laurent Simon , David Chisnall , and Ross J. Anderson . 2018. What You Get is What You C: Controlling Side Effects in Mainstream C Compilers . In IEEE European Symposium on Security and Privacy. 1--15 . Laurent Simon, David Chisnall, and Ross J. Anderson. 2018. What You Get is What You C: Controlling Side Effects in Mainstream C Compilers. In IEEE European Symposium on Security and Privacy. 1--15."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2016.125"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"event":{"name":"CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security","location":"Virtual Event USA","acronym":"CCS '20","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372297.3423352","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372297.3423352","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:20Z","timestamp":1750197740000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372297.3423352"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,30]]},"references-count":40,"alternative-id":["10.1145\/3372297.3423352","10.1145\/3372297"],"URL":"https:\/\/doi.org\/10.1145\/3372297.3423352","relation":{},"subject":[],"published":{"date-parts":[[2020,10,30]]},"assertion":[{"value":"2020-11-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}