{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T03:52:20Z","timestamp":1768535540311,"version":"3.49.0"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T00:00:00Z","timestamp":1598832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2020,8,31]]},"abstract":"<jats:p>We introduce an unusual approach for implementing cryptographic arithmetic in short high-level code with machinechecked proofs of functional correctness. We further demonstrate that simple partial evaluation is sufficient to transform such initial code into highly competitive C code, breaking the decades-old pattern that the only fast implementations are those whose instruction-level steps were written out by hand.<\/jats:p>\n          <jats:p>These techniques were used to build an elliptic-curve library that achieves competitive performance for a wide range of prime fields and multiple CPU architectures, showing that implementation and proof effort scales with the number and complexity of conceptually different algorithms, not their use cases. As one outcome, we present the first verified highperformance implementation of P-256, the most widely used elliptic curve. Implementations from our library were included in BoringSSL to replace existing specialized code, for inclusion in several large deployments for Chrome, Android, and CloudFlare.<\/jats:p>\n          <jats:p>This is an abridged version of the full paper originally presented in IEEE S&amp;P 2019 [10]. We have omitted most proof-engineering details in favor of a focus on the system's functional capabilities.<\/jats:p>","DOI":"10.1145\/3421473.3421477","type":"journal-article","created":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T13:31:19Z","timestamp":1598880679000},"page":"23-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Simple High-Level Code For Cryptographic Arithmetic"],"prefix":"10.1145","volume":"54","author":[{"given":"Andres","family":"Erbsen","sequence":"first","affiliation":[{"name":"MIT CSAIL"}]},{"given":"Jade","family":"Philipoom","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]},{"given":"Jason","family":"Gross","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]},{"given":"Robert","family":"Sloan","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}]}],"member":"320","published-online":{"date-parts":[[2020,8,31]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Web browsers by version (global marketshare). https:\/\/clicky.com\/marketshare\/global\/ web-browsers\/versions.  Web browsers by version (global marketshare). https:\/\/clicky.com\/marketshare\/global\/ web-browsers\/versions."},{"key":"e_1_2_1_2_1","unstructured":"David Benjamin. in personal communication about TLS connections initiated by Chrome 2017.  David Benjamin. in personal communication about TLS connections initiated by Chrome 2017."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11745853_14"},{"key":"e_1_2_1_4_1","unstructured":"Daniel J. Bernstein and Tanja Lange. eBACS: ECRYPT benchmarking of cryptographic systems. 2017. 28  Daniel J. Bernstein and Tanja Lange. eBACS: ECRYPT benchmarking of cryptographic systems. 2017. 28"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660370"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00005"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026928"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Shay Gueron and Vlad Krasnov. Fast prime field elliptic curve cryptography with 256 bit primes 2013.  Shay Gueron and Vlad Krasnov. Fast prime field elliptic curve cryptography with 256 bit primes 2013.","DOI":"10.1007\/s13389-014-0090-x"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2685048.2685062"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/3291168.3291192"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_2_1_19_1","first-page":"172","volume-title":"Revised Selected Papers","author":"Oliveira Thomaz","year":"2018"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026879"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/3291168.3291190"},{"key":"e_1_2_1_22_1","unstructured":"The Coq Development Team. The Coq proof assistant version 8.10.0 October 2019. 29  The Coq Development Team. The Coq proof assistant version 8.10.0 October 2019. 29"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.28"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3421473.3421477","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3421473.3421477","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:21Z","timestamp":1750268961000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3421473.3421477"}},"subtitle":["With Proofs, Without Compromises"],"short-title":[],"issued":{"date-parts":[[2020,8,31]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,8,31]]}},"alternative-id":["10.1145\/3421473.3421477"],"URL":"https:\/\/doi.org\/10.1145\/3421473.3421477","relation":{},"ISSN":["0163-5980"],"issn-type":[{"value":"0163-5980","type":"print"}],"subject":[],"published":{"date-parts":[[2020,8,31]]},"assertion":[{"value":"2020-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}