{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T16:30:32Z","timestamp":1773246632304,"version":"3.50.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2020,6,1]],"date-time":"2020-06-01T00:00:00Z","timestamp":1590969600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Prime Minister\u2019s Office"},{"name":"National Cybersecurity R8D Program","award":["NRF2014NCR-NCR001-21"],"award-info":[{"award-number":["NRF2014NCR-NCR001-21"]}]},{"name":"National Cybersecurity R8D Directorate"},{"DOI":"10.13039\/501100001321","name":"National Research Foundation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001321","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2020,7,31]]},"abstract":"<jats:p>\n            Spectre-style attacks disclosed in early 2018 expose data leakage scenarios via cache side channels. Specifically, speculatively executed paths due to branch mis-prediction may bring secret data into the cache, which are then exposed via cache side channels even after the speculative execution is squashed. Symbolic execution is a well-known test generation method to cover program paths at the level of the application software. In this article, we extend symbolic execution with modeling of cache and speculative execution. Our tool KLEE\n            <jats:sc>SPECTRE<\/jats:sc>\n            , built on top of the KLEE symbolic execution engine, can thus provide a testing engine to check for data leakage through the cache side channel as shown via Spectre attacks. Our symbolic cache model can verify whether the sensitive data leakage due to speculative execution can be observed by an attacker at a given program point. Our experiments show that KLEE\n            <jats:sc>SPECTRE<\/jats:sc>\n            can effectively detect data leakage along speculatively executed paths and our cache model can make the leakage detection more precise.\n          <\/jats:p>","DOI":"10.1145\/3385897","type":"journal-article","created":{"date-parts":[[2020,6,1]],"date-time":"2020-06-01T16:19:41Z","timestamp":1591028381000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["KLEESpectre"],"prefix":"10.1145","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1393-5326","authenticated-orcid":false,"given":"Guanhua","family":"Wang","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore"}]},{"given":"Sudipta","family":"Chattopadhyay","sequence":"additional","affiliation":[{"name":"Singapore University of Technology and Design, Singapore"}]},{"given":"Arnab Kumar","family":"Biswas","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}]},{"given":"Tulika","family":"Mitra","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7127-1137","authenticated-orcid":false,"given":"Abhik","family":"Roychoudhury","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2020,6]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Shun Yan Cheung. 2010. Level-compressed Patricia tries. Retrieved from https:\/\/www.nada.kth.se\/snilsson\/publications\/Dynamic-trie-compression-implementation\/.  Shun Yan Cheung. 2010. Level-compressed Patricia tries. Retrieved from https:\/\/www.nada.kth.se\/snilsson\/publications\/Dynamic-trie-compression-implementation\/."},{"key":"e_1_2_1_2_1","unstructured":"Intel. 2017. Intel Xeon Gold 6126 Processor. Retrieved from https:\/\/ark.intel.com\/products\/120483\/Intel-Xeon-Gold-6126-Processor-19-25M-Cache-2-60-GHz-.  Intel. 2017. Intel Xeon Gold 6126 Processor. Retrieved from https:\/\/ark.intel.com\/products\/120483\/Intel-Xeon-Gold-6126-Processor-19-25M-Cache-2-60-GHz-."},{"key":"e_1_2_1_3_1","unstructured":"uClibc. 2018. Retrieved from http:\/\/www.uclibc.org.  uClibc. 2018. Retrieved from http:\/\/www.uclibc.org."},{"key":"e_1_2_1_4_1","volume-title":"Billy Bob Brumley, and Philipp Grabher","author":"Ac\u0131i\u00e7mez Onur","year":"2010","unstructured":"Onur Ac\u0131i\u00e7mez , Billy Bob Brumley, and Philipp Grabher . 2010 . New results on instruction cache attacks. In Cryptographic Hardware and Embedded Systems (CHES\u201910), Stefan Mangard and Fran\u00e7ois-Xavier Standaert (Eds.). Springer , Berlin, 110--124. Onur Ac\u0131i\u00e7mez, Billy Bob Brumley, and Philipp Grabher. 2010. New results on instruction cache attacks. In Cryptographic Hardware and Embedded Systems (CHES\u201910), Stefan Mangard and Fran\u00e7ois-Xavier Standaert (Eds.). Springer, Berlin, 110--124."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062378"},{"key":"e_1_2_1_6_1","volume-title":"InSpectre: Breaking and fixing microarchitectural vulnerabilities by formal analysis. Arxiv Preprint Arxiv:1911.00868","author":"Balliu Musard","year":"2019","unstructured":"Musard Balliu , Mads Dam , and Roberto Guanciale . 2019. InSpectre: Breaking and fixing microarchitectural vulnerabilities by formal analysis. Arxiv Preprint Arxiv:1911.00868 ( 2019 ). Musard Balliu, Mads Dam, and Roberto Guanciale. 2019. InSpectre: Breaking and fixing microarchitectural vulnerabilities by formal analysis. Arxiv Preprint Arxiv:1911.00868 (2019)."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00022"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 8th USENIX conference on Operating systems design and implementation(OSDI\u201908)","volume":"8","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , Dawson Engle . 2008 . KLEE: Unassisted and automatic generation of high coverage tests for complex systems programs . In Proceedings of the 8th USENIX conference on Operating systems design and implementation(OSDI\u201908) , Vol. 8 . 209\u2013224. Cristian Cadar, Daniel Dunbar, Dawson Engle. 2008. KLEE: Unassisted and automatic generation of high coverage tests for complex systems programs. In Proceedings of the 8th USENIX conference on Operating systems design and implementation(OSDI\u201908), Vol. 8. 209\u2013224."},{"key":"e_1_2_1_9_1","volume-title":"Michael Schwarz, Moritz Lipp, Benjamin von","author":"Canella Claudio","year":"2018","unstructured":"Claudio Canella , Jo Van Bulck , Michael Schwarz, Moritz Lipp, Benjamin von Berg , Philipp Ortner , Frank Piessens, Dmitry Evtyushkin, and Daniel Gruss. 2018 . A systematic evaluation of transient execution attacks and defenses. Arxiv. Org E-Print Archive (2018). Claudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp, Benjamin von Berg, Philipp Ortner, Frank Piessens, Dmitry Evtyushkin, and Daniel Gruss. 2018. A systematic evaluation of transient execution attacks and defenses. Arxiv. Org E-Print Archive (2018)."},{"key":"e_1_2_1_10_1","unstructured":"Chandler Carruth. 2018. Speculative Load Hardening. Retrieved from https:\/\/docs.google.com\/document\/d\/1wwcfv3UV9ZnZVcGiGuoITT_61e_Ko3TmoCS3uXLcJR0.  Chandler Carruth. 2018. Speculative Load Hardening. Retrieved from https:\/\/docs.google.com\/document\/d\/1wwcfv3UV9ZnZVcGiGuoITT_61e_Ko3TmoCS3uXLcJR0."},{"key":"e_1_2_1_11_1","volume-title":"Deian Stefan, Tamara Rezk, and Gilles Barthe.","author":"Cauligi Sunjay","year":"2019","unstructured":"Sunjay Cauligi , Craig Disselkoen , Klaus v Gleissenthall , Deian Stefan, Tamara Rezk, and Gilles Barthe. 2019 . Towards constant-time foundations for the new spectre era. Arxiv Preprint Arxiv :1910.01755 (2019). Sunjay Cauligi, Craig Disselkoen, Klaus v Gleissenthall, Deian Stefan, Tamara Rezk, and Gilles Barthe. 2019. Towards constant-time foundations for the new spectre era. Arxiv Preprint Arxiv:1910.01755 (2019)."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2858402"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00027"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134058"},{"key":"e_1_2_1_15_1","unstructured":"Microsoft Community. 2018. C++ Developer Guidance for Speculative Execution Side Channels. Retrieved from https:\/\/docs.microsoft.com\/en-us\/cpp\/security\/developer-guidance-speculative-execution.  Microsoft Community. 2018. C++ Developer Guidance for Speculative Execution Side Channels. Retrieved from https:\/\/docs.microsoft.com\/en-us\/cpp\/security\/developer-guidance-speculative-execution."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00047"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062388"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2756550"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296957.3173204"},{"key":"e_1_2_1_20_1","volume-title":"International Conference on Computer Aided Verification (CAV\u201907)","author":"Ganesh Vijay","unstructured":"Vijay Ganesh and David L. Dill . 2007. A decision procedure for bit-vectors and arrays . In International Conference on Computer Aided Verification (CAV\u201907) . Springer, 519--531. Vijay Ganesh and David L. Dill. 2007. A decision procedure for bit-vectors and arrays. In International Conference on Computer Aided Verification (CAV\u201907). Springer, 519--531."},{"key":"e_1_2_1_21_1","volume-title":"28th USENIX Security Symposium (USENIX Security\u201919)","author":"Gleissenthall Klaus","year":"2019","unstructured":"Klaus v Gleissenthall , Rami G\u00f6khan K\u0131c\u0131 , Deian Stefan , and Ranjit Jhala . 2019 . IODINE: Verifying constant-time execution of hardware . In 28th USENIX Security Symposium (USENIX Security\u201919) . 1411--1428. Klaus v Gleissenthall, Rami G\u00f6khan K\u0131c\u0131, Deian Stefan, and Ranjit Jhala. 2019. IODINE: Verifying constant-time execution of hardware. In 28th USENIX Security Symposium (USENIX Security\u201919). 1411--1428."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/263580.263631"},{"key":"e_1_2_1_23_1","volume-title":"SPECTECTOR: Principled detection of speculative information flows. Arxiv Preprint Arxiv:1812.08639","author":"Guarnieri Marco","year":"2018","unstructured":"Marco Guarnieri , Boris K\u00f6pf , Jos\u00e9 F. Morales , Jan Reineke , and Andr\u00e9s S\u00e1nchez . 2018 . SPECTECTOR: Principled detection of speculative information flows. Arxiv Preprint Arxiv:1812.08639 (2018). Marco Guarnieri, Boris K\u00f6pf, Jos\u00e9 F. Morales, Jan Reineke, and Andr\u00e9s S\u00e1nchez. 2018. SPECTECTOR: Principled detection of speculative information flows. Arxiv Preprint Arxiv:1812.08639 (2018)."},{"key":"e_1_2_1_24_1","volume-title":"SpecuSym: Speculative symbolic execution for cache timing leak detection. Arxiv Preprint Arxiv:1911.00507","author":"Guo Shengjian","year":"2019","unstructured":"Shengjian Guo , Yueqi Chen , Peng Li , Yueqiang Cheng , Huibo Wang , Meng Wu , and Zhiqiang Zuo . 2019. SpecuSym: Speculative symbolic execution for cache timing leak detection. Arxiv Preprint Arxiv:1911.00507 ( 2019 ). Shengjian Guo, Yueqi Chen, Peng Li, Yueqiang Cheng, Huibo Wang, Meng Wu, and Zhiqiang Zuo. 2019. SpecuSym: Speculative symbolic execution for cache timing leak detection. Arxiv Preprint Arxiv:1911.00507 (2019)."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04694-0_6"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00083"},{"key":"e_1_2_1_28_1","unstructured":"Paul Kocher. 2018. Spectre Mitigations in Microsoft\u2019s C\/C++ Compiler. Retrieved from https:\/\/www.paulkocher.com\/doc\/MicrosoftCompilerSpectreMitigation.html.  Paul Kocher. 2018. Spectre Mitigations in Microsoft\u2019s C\/C++ Compiler. Retrieved from https:\/\/www.paulkocher.com\/doc\/MicrosoftCompilerSpectreMitigation.html."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_2_1_31_1","volume-title":"2015 IEEE Symposium on Security and Privacy (SP\u201915)","author":"Liu Fangfei","unstructured":"Fangfei Liu , Yuval Yarom , Qian Ge , Gernot Heiser , and Ruby B. Lee . 2015. Last-level cache side-channel attacks are practical . In 2015 IEEE Symposium on Security and Privacy (SP\u201915) . IEEE, 605--622. Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser, and Ruby B. Lee. 2015. Last-level cache side-channel attacks are practical. In 2015 IEEE Symposium on Security and Privacy (SP\u201915). IEEE, 605--622."},{"key":"e_1_2_1_32_1","volume-title":"P\u0103s\u0103reanu","author":"Nilizadeh Shirin","year":"2019","unstructured":"Shirin Nilizadeh , Yannic Noller , and Corina S . P\u0103s\u0103reanu . 2019 . DifFuzz: Differential fuzzing for side-channel analysis. In Proceedings of the 41st International Conference on Software Engineering (ICSE\u201919). IEEE Press , 176--187. Shirin Nilizadeh, Yannic Noller, and Corina S. P\u0103s\u0103reanu. 2019. DifFuzz: Differential fuzzing for side-channel analysis. In Proceedings of the 41st International Conference on Software Engineering (ICSE\u201919). IEEE Press, 176--187."},{"key":"e_1_2_1_34_1","volume-title":"USENIX Security Symposium (USENIX Security\u201920)","author":"Oleksenko Oleksii","year":"2020","unstructured":"Oleksii Oleksenko , Bohdan Trach , Mark Silberstein , and Christof Fetzer . 2020 . SpecFuzz: Bringing spectre-type vulnerabilities to the surface . In USENIX Security Symposium (USENIX Security\u201920) . Oleksii Oleksenko, Bohdan Trach, Mark Silberstein, and Christof Fetzer. 2020. SpecFuzz: Bringing spectre-type vulnerabilities to the surface. In USENIX Security Symposium (USENIX Security\u201920)."},{"key":"e_1_2_1_35_1","volume-title":"Topics in Cryptology (CT-RSA\u201906)","author":"Osvik Dag Arne","unstructured":"Dag Arne Osvik , Adi Shamir , and Eran Tromer . 2006. Cache attacks and countermeasures: The case of AES . In Topics in Cryptology (CT-RSA\u201906) , David Pointcheval (Ed.). Springer , Berlin , 1--20. Dag Arne Osvik, Adi Shamir, and Eran Tromer. 2006. Cache attacks and countermeasures: The case of AES. In Topics in Cryptology (CT-RSA\u201906), David Pointcheval (Ed.). Springer, Berlin, 1--20."},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of BSDCan","author":"Percival Colin","year":"2005","unstructured":"Colin Percival . 2005 . Cache missing for fun and profit . In Proceedings of BSDCan 2005. Colin Percival. 2005. Cache missing for fun and profit. In Proceedings of BSDCan 2005."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00068"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-007-9032-3"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 52nd Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO\u201919)","author":"Saileshwar Gururaj","unstructured":"Gururaj Saileshwar and Moinuddin K. Qureshi . 2019. CleanupSpec: An \u201cundo\u201d approach to safe speculation . In Proceedings of the 52nd Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO\u201919) . 73--86. Gururaj Saileshwar and Moinuddin K. Qureshi. 2019. CleanupSpec: An \u201cundo\u201d approach to safe speculation. In Proceedings of the 52nd Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO\u201919). 73--86."},{"key":"e_1_2_1_40_1","volume-title":"oo7: Low-overhead defense against spectre attacks via program analysis","author":"Wang Guanhua","year":"2020","unstructured":"Guanhua Wang , Sudipta Chattopadhyay , Ivan Gotovchits , Tulika Mitra , and Abhik Roychoudhury . 2020. oo7: Low-overhead defense against spectre attacks via program analysis . IEEE Transactions on Software Engineering ( 2020 ). Guanhua Wang, Sudipta Chattopadhyay, Ivan Gotovchits, Tulika Mitra, and Abhik Roychoudhury. 2020. oo7: Low-overhead defense against spectre attacks via program analysis. IEEE Transactions on Software Engineering (2020)."},{"key":"e_1_2_1_41_1","volume-title":"28th USENIX Security Symposium (USENIX Security\u201919)","author":"Wang Shuai","year":"2019","unstructured":"Shuai Wang , Yuyan Bao , Xiao Liu , Pei Wang , Danfeng Zhang , and Dinghao Wu . 2019 . Identifying cache-based side channels through secret-augmented abstract interpretation . In 28th USENIX Security Symposium (USENIX Security\u201919) . 657--674. Shuai Wang, Yuyan Bao, Xiao Liu, Pei Wang, Danfeng Zhang, and Dinghao Wu. 2019. Identifying cache-based side channels through secret-augmented abstract interpretation. In 28th USENIX Security Symposium (USENIX Security\u201919). 657--674."},{"key":"e_1_2_1_42_1","volume-title":"28th USENIX Security Symposium (USENIX Security\u201919)","author":"Werner Mario","year":"2019","unstructured":"Mario Werner , Thomas Unterluggauer , Lukas Giner , Michael Schwarz , Daniel Gruss , and Stefan Mangard . 2019 . Scattercache: Thwarting cache attacks via cache set randomization . In 28th USENIX Security Symposium (USENIX Security\u201919) . 675--692. Mario Werner, Thomas Unterluggauer, Lukas Giner, Michael Schwarz, Daniel Gruss, and Stefan Mangard. 2019. Scattercache: Thwarting cache attacks via cache set randomization. In 28th USENIX Security Symposium (USENIX Security\u201919). 675--692."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314647"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00042"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385897","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385897","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:32:50Z","timestamp":1750199570000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385897"}},"subtitle":["Detecting Information Leakage through Speculative Cache Attacks via Symbolic Execution"],"short-title":[],"issued":{"date-parts":[[2020,6]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,7,31]]}},"alternative-id":["10.1145\/3385897"],"URL":"https:\/\/doi.org\/10.1145\/3385897","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,6]]},"assertion":[{"value":"2019-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-06-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}