{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,5]],"date-time":"2026-03-05T15:47:01Z","timestamp":1772725621082,"version":"3.50.1"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"name":"NSF","award":["CNS-1514435"],"award-info":[{"award-number":["CNS-1514435"]}]},{"name":"ONR","award":["N000141512750"],"award-info":[{"award-number":["N000141512750"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>\n            We introduce Blade, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. Blade is built on the insight that to stop leaks via speculative execution, it suffices to\n            <jats:italic>cut<\/jats:italic>\n            the dataflow from expressions that speculatively introduce secrets (\n            <jats:italic>sources<\/jats:italic>\n            ) to those that leak them through the cache (\n            <jats:italic>sinks<\/jats:italic>\n            ), rather than prohibit speculation altogether. We formalize this insight in a\n            <jats:italic>static type system<\/jats:italic>\n            that (1) types each expression as either\n            <jats:italic>transient<\/jats:italic>\n            , i.e., possibly containing speculative secrets or as being\n            <jats:italic>stable<\/jats:italic>\n            , and (2) prohibits speculative leaks by requiring that all\n            <jats:italic>sink<\/jats:italic>\n            expressions are stable. Blade relies on a new abstract primitive,\n            <jats:bold>protect<\/jats:bold>\n            , to halt speculation at fine granularity. We formalize and implement\n            <jats:bold>protect<\/jats:bold>\n            using existing architectural mechanisms, and show how Blade\u2019s type system can automatically synthesize a\n            <jats:italic>minimal<\/jats:italic>\n            number of\n            <jats:bold>protect<\/jats:bold>\n            s to provably eliminate speculative leaks. We implement Blade in the Cranelift WebAssembly compiler and evaluate our approach by repairing several verified, yet vulnerable WebAssembly implementations of cryptographic primitives. We find that Blade can fix existing programs that leak via speculation\n            <jats:italic>automatically<\/jats:italic>\n            , without user intervention, and\n            <jats:italic>efficiently<\/jats:italic>\n            even when using fences to implement\n            <jats:bold>protect<\/jats:bold>\n            .\n          <\/jats:p>","DOI":"10.1145\/3434330","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":47,"title":["Automatically eliminating speculative leaks from cryptographic code with blade"],"prefix":"10.1145","volume":"5","author":[{"given":"Marco","family":"Vassena","sequence":"first","affiliation":[{"name":"CISPA, Germany"}]},{"given":"Craig","family":"Disselkoen","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]},{"given":"Klaus von","family":"Gleissenthall","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Amsterdam, Netherlands"}]},{"given":"Sunjay","family":"Cauligi","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]},{"given":"Rami G\u00f6khan","family":"K\u0131c\u0131","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]},{"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]},{"given":"Dean","family":"Tullsen","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]},{"given":"Deian","family":"Stefan","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Constraint-based program analysis","author":"Aiken Alex","unstructured":"Alex Aiken . 1996. Constraint-based program analysis . In Static Analysis, Radhia Cousot and David A. Schmidt (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 1-1. Alex Aiken. 1996. Constraint-based program analysis. In Static Analysis, Radhia Cousot and David A. Schmidt (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1-1."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_2_1_3_1","unstructured":"Intel. 2020. An Optimized Mitigation Approach for Load Value Injection. https:\/\/software.intel.com\/security-softwareguidance\/insights\/optimized-mitigation-approach-load-value-injection.  Intel. 2020. An Optimized Mitigation Approach for Load Value Injection. https:\/\/software.intel.com\/security-softwareguidance\/insights\/optimized-mitigation-approach-load-value-injection."},{"key":"e_1_2_1_4_1","volume-title":"Speculative Bufer Overflows: Attacks and Defenses. CoRR abs\/","author":"Kiriansky Vladimir","year":"1807","unstructured":"Vladimir Kiriansky and Carl Waldspurger . 2018. Speculative Bufer Overflows: Attacks and Defenses. CoRR abs\/ 1807 .03757 ( 2018 ). arXiv: 1807.03757 http:\/\/arxiv.org\/abs\/ 1807.03757 Vladimir Kiriansky and Carl Waldspurger. 2018. Speculative Bufer Overflows: Attacks and Defenses. CoRR abs\/ 1807.03757 ( 2018 ). arXiv: 1807.03757 http:\/\/arxiv.org\/abs\/ 1807.03757"},{"key":"e_1_2_1_5_1","volume-title":"Spectre Attacks: Exploiting Speculative Execution. In 40th IEEE Symposium on Security and Privacy (S&P'19)","author":"Kocher Paul","year":"2019","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 40th IEEE Symposium on Security and Privacy (S&P'19) . 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 40th IEEE Symposium on Security and Privacy (S&P'19)."},{"key":"e_1_2_1_6_1","first-page":"3","volume-title":"Proceedings of the 12th USENIX Conference on Ofensive Technologies (Baltimore, MD, USA) ( WOOT'18). USENIX Association","author":"Koruyeh Esmaeil Mohammadian","year":"2018","unstructured":"Esmaeil Mohammadian Koruyeh , Khaled N. Khasawneh , Chengyu Song , and Nael Abu-Ghazaleh . 2018 . Spectre Returns! Speculation Attacks Using the Return Stack Bufer . In Proceedings of the 12th USENIX Conference on Ofensive Technologies (Baltimore, MD, USA) ( WOOT'18). USENIX Association , Berkeley, CA, USA , 3 - 3 . http:\/\/dl.acm.org\/citation.cfm?id= 3307423. 3307426 Esmaeil Mohammadian Koruyeh, Khaled N. Khasawneh, Chengyu Song, and Nael Abu-Ghazaleh. 2018. Spectre Returns! Speculation Attacks Using the Return Stack Bufer. In Proceedings of the 12th USENIX Conference on Ofensive Technologies (Baltimore, MD, USA) ( WOOT'18). USENIX Association, Berkeley, CA, USA, 3-3. http:\/\/dl.acm.org\/citation.cfm?id= 3307423. 3307426"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.1993.246638"},{"key":"e_1_2_1_8_1","volume-title":"27th USENIX Security Symposium (USENIX Security 18)","author":"Lipp Moritz","year":"2018","unstructured":"Moritz Lipp , Michael Schwarz , Daniel Gruss , Thomas Prescher , Werner Haas , Anders Fogh , Jann Horn , Stefan Mangard , Paul Kocher , Daniel Genkin , Yuval Yarom , and Mike Hamburg . 2018 . Meltdown: Reading Kernel Memory from User Space . In 27th USENIX Security Symposium (USENIX Security 18) . Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown: Reading Kernel Memory from User Space. In 27th USENIX Security Symposium (USENIX Security 18)."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243761"},{"key":"e_1_2_1_10_1","volume-title":"Spectre is here to stay: An analysis of side-channels and speculative execution. CoRR abs\/","author":"McIlroy Ross","year":"1902","unstructured":"Ross McIlroy , Jaroslav Sevc\u00edk , Tobias Tebbi , Ben L. Titzer , and Toon Verwaest . 2019. Spectre is here to stay: An analysis of side-channels and speculative execution. CoRR abs\/ 1902 .05178 ( 2019 ). arXiv: 1902.05178 http:\/\/arxiv.org\/abs\/ 1902.05178 Ross McIlroy, Jaroslav Sevc\u00edk, Tobias Tebbi, Ben L. Titzer, and Toon Verwaest. 2019. Spectre is here to stay: An analysis of side-channels and speculative execution. CoRR abs\/ 1902.05178 ( 2019 ). arXiv: 1902.05178 http:\/\/arxiv.org\/abs\/ 1902.05178"},{"key":"e_1_2_1_11_1","volume-title":"Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing. Principles of Secure Compilation (PriSC).","author":"McMullen Tyler","year":"2020","unstructured":"Tyler McMullen . 2020 . Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing. Principles of Secure Compilation (PriSC). Tyler McMullen. 2020. Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing. Principles of Secure Compilation (PriSC)."},{"key":"e_1_2_1_12_1","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Moghimi Daniel","year":"2020","unstructured":"Daniel Moghimi , Moritz Lipp , Berk Sunar , and Michael Schwarz . 2020 . Medusa: Microarchitectural Data Leakage via Automated Attack Synthesis . In 29th USENIX Security Symposium (USENIX Security 20) . USENIX Association, Boston, MA. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/moghimi-medusa Daniel Moghimi, Moritz Lipp, Berk Sunar, and Michael Schwarz. 2020. Medusa: Microarchitectural Data Leakage via Automated Attack Synthesis. In 29th USENIX Security Symposium (USENIX Security 20). USENIX Association, Boston, MA. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/moghimi-medusa"},{"key":"e_1_2_1_13_1","unstructured":"Mozilla Wiki 2018. Security\/Sandbox. https:\/\/wiki.mozilla.org\/Security\/Sandbox.  Mozilla Wiki 2018. Security\/Sandbox. https:\/\/wiki.mozilla.org\/Security\/Sandbox."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2004.1310740"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542504"},{"key":"e_1_2_1_16_1","volume-title":"Flow logics for constraint based analysis","author":"Nielson Hanne Riis","unstructured":"Hanne Riis Nielson and Flemming Nielson . 1998. Flow logics for constraint based analysis . In Compiler Construction, Kai Koskimies (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 109-127. Hanne Riis Nielson and Flemming Nielson. 1998. Flow logics for constraint based analysis. In Compiler Construction, Kai Koskimies (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 109-127."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11605805_1"},{"key":"e_1_2_1_18_1","unstructured":"Andrew Pardoe. 2018. Spectre mitigations in MSVC. https:\/\/devblogs.microsoft.com\/cppblog\/spectre-mitigations-in-msvc\/.  Andrew Pardoe. 2018. Spectre mitigations in MSVC. https:\/\/devblogs.microsoft.com\/cppblog\/spectre-mitigations-in-msvc\/."},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Jonathan Protzenko Benjamin Beurdouche Denis Merigoux and Karthikeyan Bhargavan. 2019. Formally Verified Cryptographic Web Applications in WebAssembly. In Security and Privacy.  Jonathan Protzenko Benjamin Beurdouche Denis Merigoux and Karthikeyan Bhargavan. 2019. Formally Verified Cryptographic Web Applications in WebAssembly. In Security and Privacy.","DOI":"10.1109\/SP.2019.00064"},{"key":"e_1_2_1_20_1","volume-title":"Site Isolation: Process Separation for Web Sites within the Browser. In USENIX Security Symposium.","author":"Reis Charles","year":"2019","unstructured":"Charles Reis , Alexander Moshchuk , and Nasko Oskov . 2019 . Site Isolation: Process Separation for Web Sites within the Browser. In USENIX Security Symposium. Charles Reis, Alexander Moshchuk, and Nasko Oskov. 2019. Site Isolation: Process Separation for Web Sites within the Browser. In USENIX Security Symposium."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2020.24271"},{"key":"e_1_2_1_22_1","volume-title":"Security Analysis of Processor Instruction Set Architecture for Enforcing Control-Flow Integrity. In International Workshop on Hardware and Architectural Support for Security and Privacy (HASP).","author":"Shanbhogue Vedvyas","year":"2019","unstructured":"Vedvyas Shanbhogue , Deepak Gupta , and Ravi Sahita . 2019 . Security Analysis of Processor Instruction Set Architecture for Enforcing Control-Flow Integrity. In International Workshop on Hardware and Architectural Support for Security and Privacy (HASP). Vedvyas Shanbhogue, Deepak Gupta, and Ravi Sahita. 2019. Security Analysis of Processor Instruction Set Architecture for Enforcing Control-Flow Integrity. In International Workshop on Hardware and Architectural Support for Security and Privacy (HASP)."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304060"},{"key":"e_1_2_1_24_1","unstructured":"Vadim Tkachenko. 2018. 20-30 % Performance Hit from the Spectre Bug Fix on Ubuntu. https:\/\/www.percona.com\/blog\/2018\/01\/23\/20-30-performance-hit-spectre-bug-fix-ubuntu\/.  Vadim Tkachenko. 2018. 20-30 % Performance Hit from the Spectre Bug Fix on Ubuntu. https:\/\/www.percona.com\/blog\/2018\/01\/23\/20-30-performance-hit-spectre-bug-fix-ubuntu\/."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-009-9049-y"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00089"},{"key":"e_1_2_1_27_1","volume-title":"Ranjit Jhala, Dean Tullsen, and Deian Stefan.","author":"Vassena Marco","year":"2020","unstructured":"Marco Vassena , Craig Disselkoen , Klaus V. Gleissenthall , Sunjay Cauligi , Rami G\u00f6khan Kici , Ranjit Jhala, Dean Tullsen, and Deian Stefan. 2020 . Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade. CoRR abs\/ 2005.00294 ( 2020 ). arXiv: 2005.00294 https:\/\/arxiv.org\/abs\/ 2005.00294 Marco Vassena, Craig Disselkoen, Klaus V. Gleissenthall, Sunjay Cauligi, Rami G\u00f6khan Kici, Ranjit Jhala, Dean Tullsen, and Deian Stefan. 2020. Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade. CoRR abs\/ 2005.00294 ( 2020 ). arXiv: 2005.00294 https:\/\/arxiv.org\/abs\/ 2005.00294"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/996893.996869"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"key":"e_1_2_1_30_1","volume-title":"oo7: Lowoverhead Defense against Spectre Attacks via Binary Analysis. CoRR abs\/","author":"Wang Guanhua","year":"1807","unstructured":"Guanhua Wang , Sudipta Chattopadhyay , Ivan Gotovchits , Tulika Mitra , and Abhik Roychoudhury . 2018. oo7: Lowoverhead Defense against Spectre Attacks via Binary Analysis. CoRR abs\/ 1807 .05843 ( 2018 ). arXiv: 1807.05843 http:\/\/arxiv.org\/abs\/ 1807.05843 Guanhua Wang, Sudipta Chattopadhyay, Ivan Gotovchits, Tulika Mitra, and Abhik Roychoudhury. 2018. oo7: Lowoverhead Defense against Spectre Attacks via Binary Analysis. CoRR abs\/ 1807.05843 ( 2018 ). arXiv: 1807.05843 http:\/\/arxiv.org\/abs\/ 1807.05843"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290390"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314647"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00042"},{"key":"e_1_2_1_34_1","first-page":"719","volume-title":"23rd USENIX Security Symposium (USENIX Security 14)","author":"Yarom Yuval","year":"2014","unstructured":"Yuval Yarom and Katrina Falkner . 2014 . FLUSH+RELOAD: A High Resolution, Low Noise, L3 Cache Side-Channel Attack . In 23rd USENIX Security Symposium (USENIX Security 14) . USENIX Association, San Diego, CA , 719 - 732 . https: \/\/www.usenix.org\/conference\/usenixsecurity14\/technical-sessions\/presentation\/yarom Yuval Yarom and Katrina Falkner. 2014. FLUSH+RELOAD: A High Resolution, Low Noise, L3 Cache Side-Channel Attack. In 23rd USENIX Security Symposium (USENIX Security 14). USENIX Association, San Diego, CA, 719-732. https: \/\/www.usenix.org\/conference\/usenixsecurity14\/technical-sessions\/presentation\/yarom"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358274"},{"key":"e_1_2_1_36_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\/3434330","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434330","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434330","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:47Z","timestamp":1750195907000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434330"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":36,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434330"],"URL":"https:\/\/doi.org\/10.1145\/3434330","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}