{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:08:21Z","timestamp":1784200101157,"version":"3.55.0"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2120642, 2120696, 2154964, 2155235, 2327336"],"award-info":[{"award-number":["2120642, 2120696, 2154964, 2155235, 2327336"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    Cryptographic\n                    <jats:italic toggle=\"yes\">library<\/jats:italic>\n                    developers take care to ensure their library does not leak secrets even when there are (inevitably) exploitable vulnerabilities in the\n                    <jats:italic toggle=\"yes\">applications<\/jats:italic>\n                    the library is linked against. To do so, they choose some class of application vulnerabilities to defend against and hardcode protections against those vulnerabilities in the library code. A single set of choices is a poor fit for all contexts: a chosen protection could impose unnecessary overheads in contexts where those attacks are impossible, and an ignored protection could render the library insecure in contexts where the attack is feasible.\n                  <\/jats:p>\n                  <jats:p>\n                    We introduce\n                    <jats:sc>RoboCop<\/jats:sc>\n                    , a new methodology and toolchain for building secure\n                    <jats:italic toggle=\"yes\">and<\/jats:italic>\n                    efficient applications from cryptographic libraries, via four contributions. First, we present an operational semantics that describes the behavior of a (cryptographic) library executing in the context of a potentially vulnerable application so that we can precisely specify what different attackers can observe. Second, we use our semantics to define a novel security property,\n                    <jats:italic toggle=\"yes\">Robust Constant Time<\/jats:italic>\n                    (RCT), that defines when a cryptographic library is\n                    <jats:italic toggle=\"yes\">secure in the context<\/jats:italic>\n                    of a vulnerable application. Crucially, our definition is parameterized by an attacker model, allowing us to factor out the classes of attackers that a library may wish to secure against. This refactoring yields our third contribution: a compiler that can synthesize bespoke cryptographic libraries with security tailored to the specific application context against which the library will be linked, guaranteeing that the library is RCT in that context. Finally, we present an empirical evaluation that shows the\n                    <jats:sc>RoboCop<\/jats:sc>\n                    compiler can automatically generate code to efficiently protect a wide range (over 500) of cryptographic library primitives against three classes of attacks: read gadgets (due to application memory safety vulnerabilities), speculative read gadgets (due to application speculative execution vulnerabilities), and concurrent observations (due to application threads), with performance overhead generally under 2% for protections from read gadgets and under 4% for protections from speculative read gadgets, thus freeing library developers from making one-size-fits-all choices between security and performance.\n                  <\/jats:p>","DOI":"10.1145\/3729310","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1491-1515","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Robust Constant-Time Cryptography"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-5519-245X","authenticated-orcid":false,"given":"Matthew","family":"Kolosick","sequence":"first","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0846-8639","authenticated-orcid":false,"given":"Basavesh Ammanaghatta","family":"Shivakumar","sequence":"additional","affiliation":[{"name":"MPI-SP, MPI-SP, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-7306-5689","authenticated-orcid":false,"given":"Sunjay","family":"Cauligi","sequence":"additional","affiliation":[{"name":"MPI-SP, MPI-SP, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3411-9678","authenticated-orcid":false,"given":"Marco","family":"Patrignani","sequence":"additional","affiliation":[{"name":"University of Trento, Trento, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4795-0236","authenticated-orcid":false,"given":"Marco","family":"Vassena","sequence":"additional","affiliation":[{"name":"Utrecht University, Utrecht, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1802-9421","authenticated-orcid":false,"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7041-7464","authenticated-orcid":false,"given":"Deian","family":"Stefan","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Mart\u00edn Abadi. 1999. Secrecy by Typing in Security Protocols. J. ACM 46 5 (Sept. 1999) 749-786. https:\/\/doi.org\/10.1145\/324133.32426610.1145\/324133.324266","DOI":"10.1145\/324133.324266"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Carmine Abate Roberto Blanco Deepak Garg Catalin Hritcu Marco Patrignani and Jeremy Thibault. 2019. Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In 2019 IEEE 32nd Computer Security Foundations Symposium (CSF) (2019-06). IEEE 256-25615. https:\/\/doi.org\/10.1109\/CSF.2019.0002510.1109\/CSF.2019.00025","DOI":"10.1109\/CSF.2019.00025"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Erdem Alkim Paulo S. L. M.Barreto Nina Bindel Juliane Kr\u00e4mer Patrick Longa and Jefferson E.Ricardini. 2020. The Lattice-Based Digital Signature Scheme qTESLA. In Applied Cryptography and Network Security Mauro Conti Jianying Zhou Emiliano Casalicchio and Angelo Spognardi (Eds.). Springer International Publishing 441-460. https: \/\/doi.org\/10.1007\/978-3-030-57808-4_2210.1007\/978-3-030-57808-4_22","DOI":"10.1007\/978-3-030-57808-4_22"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","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. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS '17). Association for Computing Machinery New York NY USA 1807-1823. https:\/\/doi.org\/10.1145\/3133956.313407810.1145\/3133956.3134078","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_3_2_6_2","unstructured":"OpenSSL Project Authors. 2023. OpenSSL. OpenSSL Project.https:\/\/www.openssl.org\/"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Manuel Barbosa Gilles Barthe Karthik Bhargavan Bruno Blanchet Cas Cremers Kevin Liao and Bryan Parno. 2021. SoK: Computer-Aided Cryptography. In 2021 IEEE Symposium on Security and Privacy (SP) (2021-05). IEEE 777-795. https:\/\/doi.org\/10.1109\/SP40001.2021.0000810.1109\/SP40001.2021.00008 ISSN: 2375-1207.","DOI":"10.1109\/SP40001.2021.00008"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","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. Proc. ACM Program. Lang. 4 POPL Article 7 (2019) 30 pages. https:\/\/doi.org\/10.1145\/337107510.1145\/3371075","DOI":"10.1145\/3371075"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Sunjay Cauligi Benjamin Gr\u00e9goire Adrien Koutsos Kevin Liao Tiago Oliveira Swarn Priya Tamara Rezk and Peter Schwabe. 2021. High-Assurance Cryptography in the Spectre Era. In 2021 IEEE Symposium on Security and Privacy (SP). IEEE 1884-1901. https:\/\/doi.org\/10.1109\/SP40001.2021.0004610.1109\/SP40001.2021.00046 ISSN: 2375-1207.","DOI":"10.1109\/SP40001.2021.00046"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Benjamin Gr\u00e9goire and Vincent Laporte. 2018. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic \u201cConstant-Time\u201c. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF) (2018-07). IEEE 328-343. https:\/\/doi.org\/10.1109\/CSF.2018.0003110.1109\/CSF.2018.00031 ISSN: 2374-8303.","DOI":"10.1109\/CSF.2018.00031"},{"key":"e_1_3_2_11_2","unstructured":"Daniel J. Bernstein. 2005. Cache-timing attacks on AES. Technical Report. The University of Illinois at Chicago. https:\/\/api.semanticscholar.org\/CorpusID:2217245"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Daniel J. Bernstein. 2008. The Salsa20 Family of Stream Ciphers. In New Stream Cipher Designs: The eSTREAM Finalists (Lecture Notes in Computer Science) Matthew Robshaw and Olivier Billet (Eds.). Springer 84-97. https: \/\/doi.org\/10.1007\/978-3-540-68351-3_810.1007\/978-3-540-68351-3_8","DOI":"10.1007\/978-3-540-68351-3_8"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Nathan Burow Scott A. Carr Joseph Nash Per Larsen Michael Franz Stefan Brunthaler and Mathias Payer. 2017. Control-Flow Integrity: Precision Security and Performance. Comput. Surveys 50 (April 2017) 16:1-16:33. https:\/\/doi.org\/10.1145\/305492410.1145\/3054924","DOI":"10.1145\/3054924"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Nathan Burow Xinping Zhang and Mathias Payer. 2019. SoK: Shining Light on Shadow Stacks. In 2019 IEEE Symposium on Security and Privacy (SP) (2019-05). IEEE 985-999. https:\/\/doi.org\/10.1109\/SP.2019.0007610.1109\/SP.2019.00076 ISSN: 2375-1207.","DOI":"10.1109\/SP.2019.00076"},{"key":"e_1_3_2_15_2","unstructured":"Claudio Canella Jo Vaan Bulck Michael Schwarz Moritz Lipp Benjamin voan Berg Philipp Ortner Frank Piessens Dmitry Evtyushkin and Daniel Gruss. 2019. A Systematic Evaluation of Transient Execution Attacks and Defenses. USENIX Association 249-266. https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/canella"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Sunjay Cauligi Craig Disselkoen Klaus v. Gleissenthall Dean Tullsen Deian Stefan Tamara Rezk and Gilles Barthe. 2020. Constant-time foundations for the new spectre era. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (2020-06-11) (PLDI 2020). Association for Computing Machinery 913-926. https:\/\/doi.org\/10.1145\/3385412.338597010.1145\/3385412.3385970","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Sunjay Cauligi Craig Disselkoen Daniel Moghimi Gilles Barthe and Deian Stefan. 2022. SoK: Practical Foundations for Software Spectre Defenses. In 2022 IEEE Symposium on Security and Privacy (SP) (2022-05). IEEE 666-680. https:\/\/doi.org\/10.1109\/SP46214.2022.983370710.1109\/SP46214.2022.9833707 ISSN: 2375-1207.","DOI":"10.1109\/SP46214.2022.9833707"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Sunjay Cauligi Gary Soeller Brian Johannesmeyer Fraser Brown Riad S. Wahby John Renner Benjamin Gregoire Gilles Barthe Ranjit Jhala and Deian Stefan. 2019. FaCT: A DSL for timing-sensitive computation. In Programming Language Design and Implementation (PLDI). ACM SIGPLAN. https:\/\/doi.org\/10.1145\/3314221.331460510.1145\/3314221.3314605","DOI":"10.1145\/3314221.3314605"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Kevin Cheang Cameron Rasmussen Sanjit Seshia and Pramod Subramanyan. 2019. A Formal Approach to Secure Speculation. In 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). IEEE 288-28815. https:\/\/doi.org\/10.1109\/CSF.2019.0002710.1109\/CSF.2019.00027","DOI":"10.1109\/CSF.2019.00027"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Robert J. Colvin and Kirsten Winter. 2020. An Abstract Semantics of Speculative Execution for Reasoning About Security Vulnerabilities. In Formal Methods. FM 2019 International Workshops Emil Sekerinski Nelma Moreira Jos\u00e9 N. Oliveira Daniel Ratiu Riccardo Guidotti Marie Farrell Matt Luckcuck Diego Marmsoler Jos\u00e9 Campos Troy Astarte Laure Gonnord Antonio Cerone Luis Couto Brijesh Dongol Martin Kutrib Pedro Monteiro and David Delmas (Eds.). Springer International Publishing 323-341. https:\/\/doi.org\/10.1007\/978-3-030-54997-8_2110.1007\/978-3-030-54997-8_21","DOI":"10.1007\/978-3-030-54997-8_21"},{"key":"e_1_3_2_21_2","unstructured":"Intel Corporation. 2018. Complex Shadow-Stack Updates Intel \u00ae Control-flow Enforcement Technology Specification. Technical Report. https:\/\/software.intel.com\/sites\/default\/files\/managed\/4d\/2a\/control-flow-enforcement-technologypreview.pdf"},{"key":"e_1_3_2_22_2","unstructured":"Intel Corporation. 2018. CVE-2017-5715. Available from NIST NVD CVE-ID CVE-2017-5715. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2017-5715"},{"key":"e_1_3_2_23_2","unstructured":"Intel Corporation. 2018. CVE-2017-5753. Available from NIST NVD CVE-ID CVE-2017-5753. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2017-5753"},{"key":"e_1_3_2_24_2","unstructured":"Intel Corporation. 2018. CVE-2018-3639. Available from NIST NVD CVE-ID CVE-2018-3639. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2018-3639"},{"key":"e_1_3_2_25_2","unstructured":"Intel Corporation. 2023. Intel \u00ae and IA-32 Architectures Software Developer\u2019s Manual. Technical Report. https:\/\/www.intel.com\/content\/www\/us\/en\/content-details\/774476\/intel-64-and-ia-32-architectures-software-developer-s-manual-volume-1-basic-architecture.html"},{"key":"e_1_3_2_26_2","unstructured":"Frank Denis. 2023. libsodium. libsodium. https:\/\/doc.libsodium.org\/"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Craig Disselkoen Radha Jagadeesan Alan Jeffrey and James Riely. 2019. The Code That Never Ran: Modeling Attacks on Speculative Evaluation. In 2019 IEEE Symposium on Security and Privacy (SP). IEEE 1238-1255. https:\/\/doi.org\/10.1109\/SP.2019.0004710.1109\/SP.2019.00047 ISSN: 2375-1207.","DOI":"10.1109\/SP.2019.00047"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Xaver Fabian Marco Guarnieri and Marco Patrignani. 2022. Automatic Detection of Speculative Execution Combinations. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (CCS '22). Association for Computing Machinery New York NY USA 965-978. https:\/\/doi.org\/10.1145\/3548606.356055510.1145\/3548606.3560555","DOI":"10.1145\/3548606.3560555"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"C\u00e9dric Fournet Andrew D.Gordon and Sergio Maffeis. 2007. A Type Discipline for Authorization Policies. ACM Trans. Program. Lang. Syst. 29 5 Article 25 (Aug. 2007). https:\/\/doi.org\/10.1145\/1275497.127550010.1145\/1275497.1275500","DOI":"10.1145\/1275497.1275500"},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","unstructured":"Andrew D.Gordon and Alan Jeffrey. 2003. Authenticity by Typing for Security Protocols. 7. Comput. Secur. 11 4 (July 2003) 451-519. http:\/\/dl.acm.org\/citation.cfm?id=959088.959090","DOI":"10.3233\/JCS-2003-11402"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Roberto Guanciale Musard Balliu and Mads Dam. 2020. InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. ACM 1853-1869. https:\/\/doi.org\/10.1145\/3372297.341724610.1145\/3372297.3417246","DOI":"10.1145\/3372297.3417246"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Marco Guarnieri Boris K\u00f6pf Jan Reineke and Pepe Vila. 2021. Hardware-Software Contracts for Secure Speculation. In 42nd IEEE Symposium on Security and Privacy SP 2021 San Francisco CA USA 24-27 May 2021. IEEE 1868-1883. https:\/\/doi.org\/10.1109\/SP40001.2021.0003610.1109\/SP40001.2021.00036","DOI":"10.1109\/SP40001.2021.00036"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Marco Guarnieri Boris K\u00f6pf Jos\u00e9 F. Morales Jan Reineke and Andr\u00e9s S\u00e1nchez. 2020. Spectector: Principled Detection of Speculative Information Flows. In 2020 IEEE Symposium on Security and Privacy (SP) (2020-05). IEEE 1-19. https:\/\/doi.org\/10.1109\/SP40000.2020.0001110.1109\/SP40000.2020.00011 ISSN: 2375-1207.","DOI":"10.1109\/SP40000.2020.00011"},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","unstructured":"Merve G\u00fclmez Thomas Nyman Christoph Baumann and Jan Tobias M\u00fchlberg. 2023. Friend or Foe Inside? Exploring In-Process Isolation to Maintain Memory Safety for Unsafe Rust. arXiv preprint arXiv:2306.08127 (2023).","DOI":"10.1109\/SecDev56634.2023.00020"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Enes G\u00f6ktas Kaveh Razavi Georgios Portokalidis Herbert Bos and Cristiano Giuffrida. 2020. Speculative Probing: Hacking Blind in the Spectre Era. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security (2020-11-02) (CCS '20). Association for Computing Machinery 1871-1885. https:\/\/doi.org\/10.1145\/3372297.341728910.1145\/3372297.3417289","DOI":"10.1145\/3372297.3417289"},{"key":"e_1_3_2_36_2","unstructured":"Mohammad Hedayati Spyridoula Gravani Ethan Johnson John Criswell Michael L Scott Kai Shen and Mike Marty. 2019. Hodor: Intra-process isolation for high-throughput data plane libraries. In 2019 USENIX Annual Technical Conference USENIX ATC 2019 Renton WA USA July 10-12 2019. USENIX Association."},{"key":"e_1_3_2_37_2","unstructured":"Jann Horn. 2018. Speculative execution variant 4: speculative store bypass. https:\/\/project-zero.issues.chromium.org\/issues\/42450580"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Xuancheng Jin Xuangan Xiao Songlin Jia Wang Gao Hang Zhang Dawu Gu Siqi Ma Zhiyun Qian and Juanru Li. 2021. Annotating Tracking and Protecting Cryptographic Secrets with CryptoMPK. IEEE Computer Society 473-488. https:\/\/doi.org\/10.1109\/SP46214.2022.983365010.1109\/SP46214.2022.9833650 ISSN: 2375-1207.","DOI":"10.1109\/SP46214.2022.9833650"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2017. RustBelt: securing the foundations of the Rust programming language. Proc. ACM Program. Lang. 2 POPL (2017). https:\/\/doi.org\/10.1145\/315815410.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Paul Kirth Mitchel Dickerson Stephen Crane Per Larsen Adrian Dabrowski David Gens Yeoul Na Stijn Volckaert and Michael Franz. 2022. PKRU-safe: automatically locking down the heap between safe and unsafe languages. In Proceedings of the Seventeenth European Conference on Computer Systems. Association for Computing Machinery New York NY USA 132-148. https:\/\/doi.org\/10.1145\/3492321.351958210.1145\/3492321.3519582","DOI":"10.1145\/3492321.3519582"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"Paul Kocher Jann Horn Anders Fogh Daniel Genkin Daniel Gruss Werner Haas Mike Hamburg Moritz Lipp Stefan Mangard Thomas Prescher Michael Schwarz and Yuval Yarom. 2019. Spectre Attacks: Exploiting Speculative Execution. In 2019 IEEE Symposium on Security and Privacy (SP) (2019-05). IEEE 1-19. https:\/\/doi.org\/10.1109\/SP.2019.0000210.1109\/SP.2019.00002 ISSN: 2375-1207.","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_3_2_42_2","unstructured":"Esmaeil Mohammadian Koruyeh Khaled N.Khasawneh Chengyu Song and Nael Abu-Ghazaleh. 2018. Spectre Returns! Speculation Attacks using the Return Stack Buffer. USENIX Association. https:\/\/www.usenix.org\/conference\/woot18\/presentation\/koruyeh"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Chris Lattner and Vikram S. Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In 2nd IEEE \/ ACM International Symposium on Code Generation and Optimization (CGO 2004). IEEE Computer Society 75-88. https:\/\/doi.org\/10.1109\/CGO.2004.128166510.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Xavier Leroy. 2009. A Formally Verified Compiler Back-end. Journal of Automated Reasoning 43 4 (2009) 363-446. https:\/\/doi.org\/10.1007\/s10817-009-9155-410.1007\/s10817-009-9155-4","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","unstructured":"Giorgi Maisuradze and Christian Rossow. 2018. ret2spec: Speculative Execution Using Return Stack Buffers. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (2018-10-15) (CCS '18). Association for Computing Machinery 2109-2122. https:\/\/doi.org\/10.1145\/3243734.324376110.1145\/3243734.3243761","DOI":"10.1145\/3243734.3243761"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Andrea Mambretti Alexandra Sandulescu Alessandro Sorniotti William Robertson Engin Kirda and Anil Kurmus. 2021. Bypassing memory safety mechanisms through speculative control flow hijacks. In 2021 IEEE European Symposium on Security and Privacy (EuroS&P) (2021-09). IEEE 633-649. https:\/\/doi.org\/10.1109\/EuroSP51992.2021.0004810.1109\/EuroSP51992.2021.00048","DOI":"10.1109\/EuroSP51992.2021.00048"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"DavidMolnar Matt Piotrowski David Schultz and David A. Wagner. 2005. The Program Counter Security Model: Automatic Detection and Removal of Control-Flow Side Channel Attacks. In Information Security and Cryptology ICISC 2005 (Lecture Notes in Computer Science Vol. 3935) Dongho Won and Seungjoo Kim (Eds.). Springer 156-168. https:\/\/doi.org\/10.1007\/11734727_1410.1007\/11734727_14","DOI":"10.1007\/11734727_14"},{"key":"e_1_3_2_48_2","unstructured":"Nicholas Mosier Hamed Nemati John C.Mitchell and Caroline Trippel.2023. Serberus: Protecting Cryptographic Code from Spectres at Compile-Time. ArXiv abs\/2309.05174 (2023). https:\/\/api.semanticscholar.org\/CorpusID:261682113"},{"key":"e_1_3_2_49_2","unstructured":"Shravan Narayan Craig Disselkoen Daniel Moghimi Sunjay Cauligi Evan Johnson Zhao Gang Anjo VahldiekOberwagner Ravi Sahita Hovav Shacham Dean Tullsen and Deian Stefan. 2021. Swivel: Hardening WebAssembly against Spectre. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association 1433-1450. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/narayan"},{"key":"e_1_3_2_50_2","unstructured":"Santiago Arranz Olmos Gilles Barthe Ruben Gonzalez Benjamin Gr\u00e9goire Vincent Laporte Jean-Christophe Lechenet Tiago Oliveira and Peter Schwabe. 2023. High-assurance zeroization. Cryptology ePrint Archive Paper 2023\/1713. https:\/\/eprint.iacr.org\/2023\/1713"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","unstructured":"Marco Patrignani Amal Ahmed and Dave Clarke. 2019. Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work. ACM Comput. Surv. 51 6 Article 125 (feb 2019) 36 pages. https:\/\/doi.org\/10.1145\/328098410.1145\/3280984","DOI":"10.1145\/3280984"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","unstructured":"Marco Patrignani and SamBlackshear. 2023. Robust Safety for Move. In 2023 IEEE 36th Computer Security Foundations Symposium (CSF). IEEE Computer Society Los Alamitos CA USA 308-323. https:\/\/doi.org\/10.1109\/CSF57540.2023.0004510.1109\/CSF57540.2023.00045","DOI":"10.1109\/CSF57540.2023.00045"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","unstructured":"Marco Patrignani and Marco Guarnieri. 2021. Exorcising Spectres with Secure Compilers. In Proceedings of the 2021 ACM SIGSAC Conference on Computer Communications Security (CCS '21). Association for Computing Machinery New York NY USA 445-461. https:\/\/doi.org\/10.1145\/3460120.348453410.1145\/3460120.3484534","DOI":"10.1145\/3460120.3484534"},{"key":"e_1_3_2_54_2","unstructured":"Colin Percival. 2014. Zeroing buffers is insufficient. https:\/\/www.daemonology.net\/blog\/2014-09-06-zeroing-buffers-isinsufficient.html"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","unstructured":"Hern\u00e1n Ponce-de Leon and Johannes Kinder. 2022. Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks. In 2022 IEEE Symposium on Security and Privacy (SP). IEEE 235-248. https:\/\/doi.org\/10.1109\/SP46214.2022.983377410.1109\/SP46214.2022.9833774ISSN: 2375-1207.","DOI":"10.1109\/SP46214.2022.9833774"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","unstructured":"Jonathan Protzenko Jean-Karim Zinzindohou\u00e9 Aseem Rastogi Tahina Ramananandro Peng Wang Santiago ZanellaB\u00e9guelin Antoine Delignat-Lavaud C\u0103t\u0103lin Hri\u0163cu Karthikeyan Bhargavan C\u00e9dric Fournet and Nikhil Swamy. 2017. Verified Low-Level Programming Embedded in F*. Proc. ACM Program. Lang. 1 ICFP Article 17 (aug 2017) 29 pages. https:\/\/doi.org\/10.1145\/311026110.1145\/3110261","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","unstructured":"Elijah Rivera Samuel Mergendahl Howard E.Shrobe Hamed Okhravi and Nathan Burow. 2021. Keeping Safe Rust Safe with Galeed. In ACSAC '21: Annual Computer Security Applications Conference. ACM 824-836. https:\/\/doi.org\/10.1145\/3485832.348590310.1145\/3485832.3485903","DOI":"10.1145\/3485832.3485903"},{"key":"e_1_3_2_58_2","unstructured":"RustCrypto. 2023. Zeroize. RustCrypto. https:\/\/docs.rs\/zeroize\/1.7.0\/zeroize\/"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","unstructured":"Michael Sammler Deepak Garg Derek Dreyer and Tadeusz Litak. 2020. The high-level benefits of low-level sandboxing. PACMPL 4 POPL (2020) 32:1-32:32. https:\/\/doi.org\/10.1145\/337110010.1145\/3371100","DOI":"10.1145\/3371100"},{"key":"e_1_3_2_60_2","unstructured":"David Schrammel Samuel Weiser Richard Sadek and Stefan Mangard. 2022. Jenny: Securing Syscalls for PKU-based Memory Isolation Systems. In 31st USENIX Security Symposium USENIX Security 2022 Kevin R. B. Butler and Kurt Thomas (Eds.). USENIX Association 936-952. https:\/\/www.usenix.org\/conference\/usenixsecurity22\/presentation\/schrammel"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","unstructured":"Basavesh Ammanaghatta Shivakumar Jack Barnes Gilles Barthe Sunjay Cauligi Chitchanok Chuengsatiansup Daniel Genkin Sioli O\u2019Connell Peter Schwabe Rui Qi Sim and Yuval Yarom. 2023. Spectre Declassified: Reading from the Right Place at the Wrong Time. In 2023 IEEE Symposium on Security and Privacy (SP) (2023-05). IEEE 1753-1770. https:\/\/doi.org\/10.1109\/SP46215.2023.1017935510.1109\/SP46215.2023.10179355 ISSN: 2375-1207.","DOI":"10.1109\/SP46215.2023.10179355"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","unstructured":"David Swasey Deepak Garg and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. Proc. ACM Program. Lang. 1 OOPSLA 89:1-89:26. https:\/\/doi.org\/10.1145\/313391310.1145\/3133913","DOI":"10.1145\/3133913"},{"key":"e_1_3_2_63_2","unstructured":"The LLVM Foundation. 2021. Control Flow Integrity Clang 12 documentation. https:\/\/clang.llvm.org\/docsControlFlowIntegrity.html"},{"key":"e_1_3_2_64_2","unstructured":"Reini Urban. 2019. libsodium_memzero with memory barrier \u2022 Issue #802 \u2022 jedisct1\/libsodium. https:\/\/github.com\/jedisct1\/libsodium\/issues\/802"},{"key":"e_1_3_2_65_2","unstructured":"Anjo Vahldiek-Oberwagner Eslam Elnikety Nuno O. Duarte Michael Sammler Peter Druschel and Deepak Garg. 2019. ERIM: Secure Efficient In-process Isolation with Protection Keys (MPK). In 28th USENIX Security Symposium USENIX Security 2019 Nadia Heninger and Patrick Traynor (Eds.). USENIX Association 1221-1238. https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/vahldiek-oberwagner"},{"key":"e_1_3_2_66_2","unstructured":"VAMPIRE. 2021. SUPERCOP: System for Unified Performance Evaluation Related to Cryptographic Operations and Primitives. https:\/\/bench.cr.yp.to\/supercop.html"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","unstructured":"Marco Vassena Craig Disselkoen Klaus voan Gleissenthall Sunjay Cauligi Rami G\u00f6khan K\u0131c\u0131 Ranjit Jhala Dean Tullsen and Deian Stefan. 2021. Automatically eliminating speculative leaks from cryptographic code with blade. Proc. ACM Program. Lang. 5 (2021) 49:1-49:30. Issue POPL. https:\/\/doi.org\/10.1145\/343433010.1145\/3434330","DOI":"10.1145\/3434330"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","unstructured":"Alexios Voulimeneas Jonas Vinck Ruben Mechelinck and Stijn Volckaert. 2022. You shall not (by)pass!: practical secure and fast PKU-based sandboxing. In EuroSys '22: Seventeenth European Conference on Computer Systems Rennes France April 5-8 2022 Y\u00e9rom-David Bromberg Anne-Marie Kermarrec and Christos Kozyrakis (Eds.). ACM 266-282. https:\/\/doi.org\/10.1145\/3492321.351956010.1145\/3492321.3519560","DOI":"10.1145\/3492321.3519560"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","unstructured":"Conrad Watt John Renner Natalie Popescu Sunjay Cauligi and Deian Stefan. 2019. CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem. Proc. ACM Program. Lang. 3 POPL Article 77 (jan 2019) 29 pages. https:\/\/doi.org\/10.1145\/329039010.1145\/3290390","DOI":"10.1145\/3290390"},{"key":"e_1_3_2_70_2","unstructured":"Johannes Wikner and Kaveh Razavi. 2022. RETBLEED: Arbitrary Speculative Code Execution with Return Instructions. USENIX Association 3825-3842. https:\/\/www.usenix.org\/conference\/usenixsecurity22\/presentation\/wikner"},{"key":"e_1_3_2_71_2","unstructured":"Zhaomo Yang Brian Johannesmeyer Anders Trier Olesen Sorin Lerner and Kirill Levchenko. 2017. Dead Store Elimination (Still) Considered Harmful. USENIX Association 1025-1040. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/yang"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","unstructured":"Hosein Yavarzadeh Mohammadkazem Taram Shravan Narayan Deian Stefan and Dean M. Tullsen. 2023. Half&Half: Demystifying Intel\u2019s Directional Branch Predictors for Fast Secure Partitioned Execution. In 44th IEEE Symposium on Security and Privacy SP 2023 San Francisco CA USA May 21-25 2023. IEEE 1220-1237. https:\/\/doi.org\/10.1109\/SP46215.2023.1017941510.1109\/SP46215.2023.10179415","DOI":"10.1109\/SP46215.2023.10179415"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729310","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729310","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:09:36Z","timestamp":1784196576000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729310"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":71,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729310"],"URL":"https:\/\/doi.org\/10.1145\/3729310","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}