{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,26]],"date-time":"2026-04-26T07:12:14Z","timestamp":1777187534115,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,30]],"date-time":"2017-10-30T00:00:00Z","timestamp":1509321600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ONR","award":["N000141210914"],"award-info":[{"award-number":["N000141210914"]}]},{"name":"ONR","award":["N000141512750"],"award-info":[{"award-number":["N000141512750"]}]},{"name":"C\u00e1tedra PT-FLAD em Smart Cities & Smart Governance"},{"name":"Google Chrome University"},{"name":"North Portugal Regional Operational Programme (NORTE 2020)","award":["NORTE- 01-0145-FEDER- 000020"],"award-info":[{"award-number":["NORTE- 01-0145-FEDER- 000020"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,30]]},"DOI":"10.1145\/3133956.3134078","type":"proceedings-article","created":{"date-parts":[[2017,10,27]],"date-time":"2017-10-27T12:48:18Z","timestamp":1509108498000},"page":"1807-1823","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":88,"title":["Jasmin"],"prefix":"10.1145","author":[{"given":"Jos\u00e9 Bacelar","family":"Almeida","sequence":"first","affiliation":[{"name":"INESC TEC and Universidade do Minho, Braga, Portugal"}]},{"given":"Manuel","family":"Barbosa","sequence":"additional","affiliation":[{"name":"INESC TEC and FCUP Universidade do Porto, Porto, Portugal"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}]},{"given":"Arthur","family":"Blot","sequence":"additional","affiliation":[{"name":"ENS Lyon, Lyon, France"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[{"name":"Inria Sophia-Antipolis, Valbonne, France"}]},{"given":"Vincent","family":"Laporte","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}]},{"given":"Tiago","family":"Oliveira","sequence":"additional","affiliation":[{"name":"INESC TEC and FCUP Universidade do Porto, Porto, Portugal"}]},{"given":"Hugo","family":"Pacheco","sequence":"additional","affiliation":[{"name":"INESC TEC and Universidade do Minho, Braga, Portugal"}]},{"given":"Benedikt","family":"Schmidt","sequence":"additional","affiliation":[{"name":"Google Inc., Mountain View, CA, USA"}]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique, Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2017,10,30]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Lucky Thirteen: Breaking the TLS and DTLS Record Protocols IEEE Symposium on Security and Privacy, SP","author":"Nadhem","year":"2013","unstructured":"Nadhem J. AlFardan and Kenneth G. Paterson 2013. Lucky Thirteen: Breaking the TLS and DTLS Record Protocols IEEE Symposium on Security and Privacy, SP 2013. IEEE Computer Society, 526--540."},{"key":"e_1_3_2_2_2_1","volume-title":"ACM CCS 13, Ahmad-Reza Sadeghi, Virgil D","author":"Almeida Jos\u00e9 Bacelar","unstructured":"Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and Franc cois Dupressoir 2013. Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. In ACM CCS 13, Ahmad-Reza Sadeghi, Virgil D. Gligor, and Moti Yung (Eds.). ACM Press, 1217--1230."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-52993-5_9"},{"key":"e_1_3_2_2_4_1","volume-title":"Verifying Constant-time Implementations. In 25th USENIX Security Symposium (USENIX Security 16)","author":"Bacelar Almeida Jose Carlos","year":"2016","unstructured":"Jose Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Franc cois Dupressoir, and Michael Emmi 2016. Verifying Constant-time Implementations. In 25th USENIX Security Symposium (USENIX Security 16). USENIX Association, Austin, TX. https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/almeida"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_2_6_1","volume-title":"Program logics for certified compilers","author":"Appel Andrew W","unstructured":"Andrew W Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program logics for certified compilers. Cambridge University Press."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_2_8_1","volume-title":"Carlos Daniel Luna, and David Pichardie.","author":"Barthe Gilles","year":"2014","unstructured":"Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, and David Pichardie. 2014. System-level Non-interference for Constant-time Cryptography ACM CCS 14, Gail-Joon Ahn, Moti Yung, and Ninghui Li (Eds.). ACM Press, 1267--1279."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_6"},{"key":"e_1_3_2_2_10_1","volume-title":"Verified Correctness and Security of OpenSSL HMAC 24th USENIX Security Symposium, USENIX Security 15","author":"Beringer Lennart","year":"2015","unstructured":"Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel 2015. Verified Correctness and Security of OpenSSL HMAC 24th USENIX Security Symposium, USENIX Security 15, Washington, D.C., USA, August 12--14, 2015., Jaeyeon Jung and Thorsten Holz (Eds.). USENIX Association, 207--221. https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/beringer"},{"key":"e_1_3_2_2_11_1","unstructured":"Dan Bernstein. Writing high-speed software. (????). http:\/\/cr.yp.to\/qhasm.html"},{"key":"e_1_3_2_2_12_1","unstructured":"Daniel J. Bernstein. 2005. Cache-timing attacks on AES. (2005). shownotehttp:\/\/cr.yp.to\/antiforgery\/cachetiming-20050414.pdf."},{"key":"e_1_3_2_2_13_1","volume-title":"Moti Yung","author":"Bernstein Daniel J.","unstructured":"Daniel J. Bernstein. 2006. Curve25519: New Diffie-Hellman Speed Records PKC 2006 (LNCS), Moti Yung, Yevgeniy Dodis, Aggelos Kiayias, and Tal Malkin (Eds.), Vol. Vol. 3958. Springer, Heidelberg, 207--228."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23951-9_9"},{"key":"e_1_3_2_2_15_1","unstructured":"Dan Berstein and Peter Schwabe 2015. gfverif: fast and easy verification of finite-field arithmetic. (2015). http:\/\/gfverif.cryptojedi.org\/"},{"key":"e_1_3_2_2_16_1","volume-title":"Santiago Zanella B\u00e9guelin, and Jean Karim Zinzindohou\u00e9","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Catalin Hritcu, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Peng Wang, Santiago Zanella B\u00e9guelin, and Jean Karim Zinzindohou\u00e9. 2017. Verified Low-Level Programming Embedded in F. CoRR Vol. abs\/1703.00053 (2017). http:\/\/arxiv.org\/abs\/1703.00053"},{"key":"e_1_3_2_2_17_1","volume-title":"Vale: Verifying High-Performance Cryptographic Assembly Code 26th USENIX Security Symposium (USENIX Security 17)","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 26th USENIX Security Symposium (USENIX Security 17). USENIX Association, Vancouver, BC. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond"},{"key":"e_1_3_2_2_18_1","volume-title":"Orr Dunkelman (Ed.)","author":"Brumley Billy Bob","unstructured":"Billy Bob Brumley, Manuel Barbosa, Dan Page, and Frederik Vercauteren 2012. Practical Realisation and Elimination of an ECC-Related Software Bug Attack CT-RSA 2012 (LNCS), Orr Dunkelman (Ed.), Vol. Vol. 7178. Springer, Heidelberg, 171--186."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660370"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/SPW.2015.33"},{"key":"e_1_3_2_2_22_1","unstructured":"Andres Erbsen Jade Philipoom Jason Gross Robert Sloan and Adam Chlipala 2017. Systematic Synthesis of Elliptic Curve Cryptography Implementations. (2017). https:\/\/people.csail.mit.edu\/jgross\/personal-website\/papers\/2017-fiat-crypto-pldi-draft.pdf"},{"key":"e_1_3_2_2_24_1","unstructured":"Darrel Hankerson Alfred Menezes and Scott Vanstone. 2004. Guide to elliptic curve cryptography. (2004)."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48965-0_36"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--17511--4_20"},{"key":"e_1_3_2_2_28_1","volume-title":"POPL","author":"Leroy Xavier","year":"2006","unstructured":"Xavier Leroy. 2006. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006. ACM, 42--54."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_2_30_1","first-page":"2014","article-title":"(published 2015). Boolector 2.0 system description","volume":"9","author":"Niemetz Aina","year":"2014","unstructured":"Aina Niemetz, Mathias Preiner, and Armin Biere 2014 (published 2015). Boolector 2.0 system description. Journal on Satisfiability, Boolean Modeling and Computation Vol. 9 (2014 (published 2015)), 53--58.","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/330249.330250"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892230"},{"key":"e_1_3_2_2_34_1","volume-title":"Appel","author":"Ye Katherine","year":"2017","unstructured":"Katherine Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, and Andrew W. Appel 2017. Verified correctness and security of mbedTLS HMAC-DRBG ACM CCS 2017."},{"key":"e_1_3_2_2_35_1","first-page":"536","article-title":"HACL*: A Verified Modern Cryptographic Library","volume":"2017","author":"Zinzindohou\u00e9 Jean Karim","year":"2017","unstructured":"Jean Karim Zinzindohou\u00e9, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. IACR Cryptology ePrint Archive Vol. 2017 (2017), 536. http:\/\/eprint.iacr.org\/2017\/536","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.28"}],"event":{"name":"CCS '17: 2017 ACM SIGSAC Conference on Computer and Communications Security","location":"Dallas Texas USA","acronym":"CCS '17","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133956.3134078","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134078","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134078","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:03Z","timestamp":1750212663000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133956.3134078"}},"subtitle":["High-Assurance and High-Speed Cryptography"],"short-title":[],"issued":{"date-parts":[[2017,10,30]]},"references-count":35,"alternative-id":["10.1145\/3133956.3134078","10.1145\/3133956"],"URL":"https:\/\/doi.org\/10.1145\/3133956.3134078","relation":{},"subject":[],"published":{"date-parts":[[2017,10,30]]},"assertion":[{"value":"2017-10-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}