{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:19:53Z","timestamp":1750220393931,"version":"3.41.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS-1801534, CNS-1956032, CNS-1942851, CNS-1816282, CCF-1723571"],"award-info":[{"award-number":["CNS-1801534, CNS-1956032, CNS-1942851, CNS-1816282, CCF-1723571"]}],"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":[[2021,10,20]]},"abstract":"<jats:p>The high-profile Spectre attack and its variants have revealed that speculative execution may leave secret-dependent footprints in the cache, allowing an attacker to learn confidential data. However, existing static side-channel detectors either ignore speculative execution, leading to false negatives, or lack a precise cache model, leading to false positives. In this paper, somewhat surprisingly, we show that it is challenging to develop a speculation-aware static analysis with precise cache models: a combination of existing works does not necessarily catch all cache side channels. Motivated by this observation, we present a new semantic definition of security against cache-based side-channel attacks, called Speculative-Aware noninterference (SANI), which is applicable to a variety of attacks and cache models. We also develop SpecSafe to detect the violations of SANI. Unlike other speculation-aware symbolic executors, SpecSafe employs a novel program transformation so that SANI can be soundly checked by speculation-unaware side-channel detectors. SpecSafe is shown to be both scalable and accurate on a set of moderately sized benchmarks, including commonly used cryptography libraries.<\/jats:p>","DOI":"10.1145\/3485506","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["SpecSafe: detecting cache side channels in a speculative world"],"prefix":"10.1145","volume":"5","author":[{"given":"Robert","family":"Brotzman","sequence":"first","affiliation":[{"name":"Pennsylvania State University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Danfeng","family":"Zhang","sequence":"additional","affiliation":[{"name":"Pennsylvania State University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mahmut Taylan","family":"Kandemir","sequence":"additional","affiliation":[{"name":"Pennsylvania State University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gang","family":"Tan","sequence":"additional","affiliation":[{"name":"Pennsylvania State University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/648255.752713"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/3241094.3241100"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2206282"},{"key":"e_1_2_2_4_1","unstructured":"Daniel J. Bernstein. 2005. Cache-timing attacks on AES. cr.yp.to\/papers.html#cachetiming  Daniel J. Bernstein. 2005. Cache-timing attacks on AES. cr.yp.to\/papers.html#cachetiming"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11894063_16"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/3154768.3154779"},{"volume-title":"Detecting and Mitigating Cache-Based Side-Channels. Ph. D. Dissertation","author":"Brotzman Robert","key":"e_1_2_2_7_1","unstructured":"Robert Brotzman . 2021. Detecting and Mitigating Cache-Based Side-Channels. Ph. D. Dissertation . Pennsylvania State University . Robert Brotzman. 2021. Detecting and Mitigating Cache-Based Side-Channels. Ph. D. Dissertation. Pennsylvania State University."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00022"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/3361338.3361356"},{"key":"e_1_2_2_10_1","unstructured":"Chandler Carruth. 2019. Speculative Load Hardening. https:\/\/llvm.org\/docs\/SpeculativeLoadHardening.html  Chandler Carruth. 2019. Speculative Load Hardening. https:\/\/llvm.org\/docs\/SpeculativeLoadHardening.html"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385970"},{"volume-title":"32nd IEEE Computer Security Foundations Symposium (CSF). 288\u201328815","author":"Cheang K.","key":"e_1_2_2_12_1","unstructured":"K. Cheang , C. Rasmussen , S. Seshia , and P. Subramanyan . 2019. A Formal Approach to Secure Speculation . In 32nd IEEE Computer Security Foundations Symposium (CSF). 288\u201328815 . K. Cheang, C. Rasmussen, S. Seshia, and P. Subramanyan. 2019. A Formal Approach to Secure Speculation. In 32nd IEEE Computer Security Foundations Symposium (CSF). 288\u201328815."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00074"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2017.38"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/2534766.2534804"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062388"},{"volume-title":"Security Policies and Security Models. In IEEE Symp. on Security and Privacy (S&P). 11\u201320","author":"Joseph","key":"e_1_2_2_17_1","unstructured":"Joseph A. Goguen and Jose Meseguer. 1982 . Security Policies and Security Models. In IEEE Symp. on Security and Privacy (S&P). 11\u201320 . Joseph A. Goguen and Jose Meseguer. 1982. Security Policies and Security Models. In IEEE Symp. on Security and Privacy (S&P). 11\u201320."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3065913.3065915"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417246"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00011"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.22"},{"key":"e_1_2_2_22_1","unstructured":"Jann Horn. 2018. Issue 1528: speculative execution variant 4: speculative store bypass. https:\/\/bugs.chromium.org\/p\/project-zero\/issues\/detail?id=1528 Accessed: 2020-1-21  Jann Horn. 2018. Issue 1528: speculative execution variant 4: speculative store bypass. https:\/\/bugs.chromium.org\/p\/project-zero\/issues\/detail?id=1528 Accessed: 2020-1-21"},{"key":"e_1_2_2_23_1","unstructured":"Intel. 2018. Bounds Check Bypass. https:\/\/software.intel.com\/security-software-guidance\/software-guidance\/bounds-check-bypass  Intel. 2018. Bounds Check Bypass. https:\/\/software.intel.com\/security-software-guidance\/software-guidance\/bounds-check-bypass"},{"key":"e_1_2_2_24_1","unstructured":"Intel. 2018. Intel Analysis of Speculative Execution Side Channels. https:\/\/newsroom.intel.com\/wp-content\/uploads\/sites\/11\/2018\/01\/Intel-Analysis-of-Speculative-Execution-Side-Channels.pdf  Intel. 2018. Intel Analysis of Speculative Execution Side Channels. https:\/\/newsroom.intel.com\/wp-content\/uploads\/sites\/11\/2018\/01\/Intel-Analysis-of-Speculative-Execution-Side-Channels.pdf"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00083"},{"key":"e_1_2_2_26_1","unstructured":"Paul Kocher. 2018. Spectre Mitigations in Microsoft\u2019s C\/C++ Compiler. https:\/\/www.paulkocher.com\/doc\/MicrosoftCompilerSpectreMitigation.html  Paul Kocher. 2018. Spectre Mitigations in Microsoft\u2019s C\/C++ Compiler. https:\/\/www.paulkocher.com\/doc\/MicrosoftCompilerSpectreMitigation.html"},{"key":"e_1_2_2_27_1","volume-title":"Spectre Attacks: Exploiting Speculative Execution. In 40th IEEE Symposium on Security and Privacy (S&P\u201919)","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\u201919) . 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\u201919)."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/646764.703989"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/646761.706156"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/3307423.3307426"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/977395.977673"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.43"},{"key":"e_1_2_2_33_1","volume-title":"EM: ElectroMagnetic Side-Channel Attacks on a Complex System-on-Chip. In Cryptographic Hardware and Embedded Systems \u2013 CHES","author":"Longo J.","year":"2015","unstructured":"J. Longo , E. De Mulder , D. Page , and M. Tunstall . 2015 . SoC It to EM: ElectroMagnetic Side-Channel Attacks on a Complex System-on-Chip. In Cryptographic Hardware and Embedded Systems \u2013 CHES 2015, Tim G\u00fcneysu and Helena Handschuh (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 620\u2013640. isbn:978-3-662-48324-4 J. Longo, E. De Mulder, D. Page, and M. Tunstall. 2015. SoC It to EM: ElectroMagnetic Side-Channel Attacks on a Complex System-on-Chip. In Cryptographic Hardware and Embedded Systems \u2013 CHES 2015, Tim G\u00fcneysu and Helena Handschuh (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 620\u2013640. isbn:978-3-662-48324-4"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243761"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11734727_14"},{"key":"e_1_2_2_36_1","volume-title":"You Shall Not Bypass: Employing data dependencies to prevent Bounds Check Bypass. ArXiv, abs\/1805.08506","author":"Oleksenko Oleksii","year":"2018","unstructured":"Oleksii Oleksenko , Bohdan Trach , Tobias Reiher , Mark Silberstein , and Christof Fetzer . 2018. You Shall Not Bypass: Employing data dependencies to prevent Bounds Check Bypass. ArXiv, abs\/1805.08506 ( 2018 ). Oleksii Oleksenko, Bohdan Trach, Tobias Reiher, Mark Silberstein, and Christof Fetzer. 2018. You Shall Not Bypass: Employing data dependencies to prevent Bounds Check Bypass. ArXiv, abs\/1805.08506 (2018)."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/3489212.3489296"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/11605805_1"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1653662.1653687"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-60876-1_1"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/2724966.2725064"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3152701.3152706"},{"key":"e_1_2_2_43_1","article-title":"oo7: Low-overhead defense against spectre attacks via program analysis","author":"Wang Guanhua","year":"2019","unstructured":"Guanhua Wang , Sudipta Chattopadhyay , Ivan Gotovchits , Tulika Mitra , and Abhik Roychoudhury . 2019 . oo7: Low-overhead defense against spectre attacks via program analysis . IEEE Transactions on Software Engineering. Guanhua Wang, Sudipta Chattopadhyay, Ivan Gotovchits, Tulika Mitra, and Abhik Roychoudhury. 2019. oo7: Low-overhead defense against spectre attacks via program analysis. IEEE Transactions on Software Engineering.","journal-title":"IEEE Transactions on Software Engineering."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/3361338.3361384"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/3241189.3241209"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/2362793.2362802"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134016"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046660.2046670"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00042"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/2671225.2671271"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382230"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485506","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485506","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485506","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485506"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":51,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485506"],"URL":"https:\/\/doi.org\/10.1145\/3485506","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}