{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,25]],"date-time":"2026-09-25T20:57:19Z","timestamp":1790369839058,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":61,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,30]],"date-time":"2020-10-30T00:00:00Z","timestamp":1604016000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Swedish Civil Contingencies Agency","award":["CERCES"],"award-info":[{"award-number":["CERCES"]}]},{"name":"Swedish Research Council","award":["JointForce."],"award-info":[{"award-number":["JointForce."]}]},{"name":"Swedish Foundation for Strategic Research","award":["TrustFull"],"award-info":[{"award-number":["TrustFull"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,30]]},"DOI":"10.1145\/3372297.3417246","type":"proceedings-article","created":{"date-parts":[[2020,11,2]],"date-time":"2020-11-02T13:27:04Z","timestamp":1604323624000},"page":"1853-1869","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":44,"title":["InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis"],"prefix":"10.1145","author":[{"given":"Roberto","family":"Guanciale","sequence":"first","affiliation":[{"name":"KTH Royal Institute of Technology, Strockholm, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Musard","family":"Balliu","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mads","family":"Dam","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Stockholm, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,11,2]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Jones","author":"Aagaard Mark D.","year":"2001"},{"key":"e_1_3_2_2_2_1","volume-title":"International Conference on Information and Communications Security. Springer, 112--121","author":"Onur"},{"key":"e_1_3_2_2_3_1","volume-title":"25th USENIX Security Symposium (USENIX Security 16)","author":"Almeida Jos\u00e9 Bacelar","year":"2016"},{"key":"e_1_3_2_2_4_1","unstructured":"ARM. 2018. SSBS Speculative Store Bypass Safe. https:\/\/developer.arm.com\/docs\/ddi0595\/d\/aarch64-system-registers\/ssbs Accessed: 2020-01--16.  ARM. 2018. SSBS Speculative Store Bypass Safe. https:\/\/developer.arm.com\/docs\/ddi0595\/d\/aarch64-system-registers\/ssbs Accessed: 2020-01--16."},{"key":"e_1_3_2_2_5_1","unstructured":"ARM. 2019. Cache Speculation Side channels v2.4.  ARM. 2019. Cache Speculation Side channels v2.4."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660322"},{"key":"e_1_3_2_2_7_1","unstructured":"Daniel J. Bernstein. 2005. Cache-timing attacks on AES. http:\/\/cr.yp.to\/antiforgery\/cachetiming-20050414.pdf.  Daniel J. Bernstein. 2005. Cache-timing attacks on AES. http:\/\/cr.yp.to\/antiforgery\/cachetiming-20050414.pdf."},{"key":"e_1_3_2_2_8_1","volume-title":"Dill","author":"Burch Jerry R.","year":"1994"},{"key":"e_1_3_2_2_9_1","volume-title":"Michael Schwarz, Moritz Lipp, Benjamin von","author":"Canella Claudio","year":"2019"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363219"},{"key":"e_1_3_2_2_11_1","volume-title":"Deian Stefan, Tamara Rezk, and Gilles Barthe.","author":"Cauligi Sunjay","year":"2019"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00027"},{"key":"e_1_3_2_2_13_1","volume-title":"Sgxpectre attacks: Stealing intel secrets from sgx enclaves via speculative execution. arXiv preprint arXiv:1802.09085","author":"Chen Guoxing","year":"2018"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00047"},{"key":"e_1_3_2_2_15_1","volume-title":"26th USENIX Security Symposium. 51--67","author":"Disselkoen Craig","year":"2017"},{"key":"e_1_3_2_2_16_1","volume-title":"Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems. ACM.","author":"Evtyushkin Dmitry"},{"key":"e_1_3_2_2_17_1","volume-title":"White","author":"Feiste Kurt A.","year":"2000"},{"key":"e_1_3_2_2_18_1","unstructured":"Anders Fogh and Christopher Ertl. 2018. Wrangling with the Ghost An Inside Story of Mitigating Speculative Execution Side Channel Vulnerabilities.  Anders Fogh and Christopher Ertl. 2018. Wrangling with the Ghost An Inside Story of Mitigating Speculative Execution Side Channel Vulnerabilities."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-016-0141-6"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40667-1_14"},{"key":"e_1_3_2_2_21_1","volume-title":"24th USENIX Security Symposium. 897--912","author":"Gruss Daniel","year":"2015"},{"key":"e_1_3_2_2_22_1","volume-title":"InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis. arxiv","author":"Guanciale Roberto","year":"1911"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00011"},{"key":"e_1_3_2_2_24_1","unstructured":"Jann Horn. 2018. speculative execution variant 4: speculative store bypass.  Jann Horn. 2018. speculative execution variant 4: speculative store bypass."},{"key":"e_1_3_2_2_25_1","volume-title":"Project Zero","volume":"39","author":"Jann","year":"2018"},{"key":"e_1_3_2_2_26_1","unstructured":"Intel. 2018a. Speculative Execution Side Channel Mitigations Revision 3.0.  Intel. 2018a. Speculative Execution Side Channel Mitigations Revision 3.0."},{"key":"e_1_3_2_2_27_1","unstructured":"Intel. 2018b. Speculative Execution Side Channel Update.  Intel. 2018b. Speculative Execution Side Channel Update."},{"key":"e_1_3_2_2_28_1","unstructured":"Intel. 2019. Guidelines for Mitigating Timing Side Channels Against Cryptographic Implementations. https:\/\/software.intel.com\/security-software-guidance\/insights\/guidelines-mitigating-timing-side-channels-against-cryptographic-implementations  Intel. 2019. Guidelines for Mitigating Timing Side Channels Against Cryptographic Implementations. https:\/\/software.intel.com\/security-software-guidance\/insights\/guidelines-mitigating-timing-side-channels-against-cryptographic-implementations"},{"key":"e_1_3_2_2_29_1","volume-title":"McMillan","author":"Jhala Ranjit","year":"2001"},{"key":"e_1_3_2_2_30_1","volume-title":"DAWG: A Defense Against Cache Timing Attacks in Speculative Execution Processors. In 2018 51st Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO).","author":"Kiriansky V."},{"key":"e_1_3_2_2_31_1","volume-title":"Speculative buffer overflows: Attacks and defenses. arXiv preprint arXiv:1807.03757","author":"Kiriansky Vladimir","year":"2018"},{"key":"e_1_3_2_2_32_1","volume-title":"Spectre Attacks: Exploiting Speculative Execution. In 2019 IEEE Symposium on Security and Privacy, SP 2019","author":"Kocher Paul","year":"2019"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/646761.706156"},{"key":"e_1_3_2_2_34_1","volume-title":"12th USENIX Workshop on Offensive Technologies (WOOT).","author":"Koruyeh Esmaeil Mohammadian","year":"2018"},{"key":"e_1_3_2_2_35_1","volume-title":"12th USENIX Workshop on Offensive Technologies (WOOT 18)","author":"Koruyeh Esmaeil Mohammadian","year":"2018"},{"key":"e_1_3_2_2_36_1","volume-title":"27th USENIX Security Symposium. 973--990","author":"Lipp Moritz","year":"2018"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.43"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243761"},{"key":"e_1_3_2_2_39_1","unstructured":"P. Manolios and S. K. Srinivasan. 2005. Refinement maps for efficient verification of processor models. In Design Automation and Test in Europe. 1304--1309 Vol. 2.  P. Manolios and S. K. Srinivasan. 2005. Refinement maps for efficient verification of processor models. In Design Automation and Test in Europe. 1304--1309 Vol. 2."},{"key":"e_1_3_2_2_40_1","first-page":"8","article-title":"Hello from the Other Side: SSH over Robust Cache Covert Channels in the Cloud","volume":"17","author":"Maurice Cl\u00e9mentine","year":"2017","journal-title":"NDSS"},{"key":"e_1_3_2_2_41_1","volume-title":"Spectre is here to stay: An analysis of side-channels and speculative execution. arXiv preprint arXiv:1902.05178","author":"Mcilroy Ross","year":"2019"},{"key":"e_1_3_2_2_42_1","unstructured":"Matt Miller. 2018. Mitigating speculative execution side channel hardware vulnerabilities. https:\/\/msrc-blog.microsoft.com\/2018\/03\/15\/mitigating-speculative-execution-side-channel-hardware-vulnerabilities\/  Matt Miller. 2018. Mitigating speculative execution side channel hardware vulnerabilities. https:\/\/msrc-blog.microsoft.com\/2018\/03\/15\/mitigating-speculative-execution-side-channel-hardware-vulnerabilities\/"},{"key":"e_1_3_2_2_43_1","volume-title":"8th International Conference","author":"Molnar David","year":"2005"},{"key":"e_1_3_2_2_44_1","volume-title":"International Workshop on Selected Areas in Cryptography. Springer, 147--162","author":"Neve Michael","year":"2006"},{"key":"e_1_3_2_2_45_1","volume-title":"Cryptographers? track at the RSA conference","author":"Osvik Dag Arne"},{"key":"e_1_3_2_2_46_1","volume-title":"Theoretical use of cache memory as a cryptanalytic side-channel. IACR Cryptology ePrint Archive","author":"Page Dan","year":"2002"},{"key":"e_1_3_2_2_47_1","unstructured":"Andrew Pardoe. 2018. Spectre mitigations in MSVC.  Andrew Pardoe. 2018. Spectre mitigations in MSVC."},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014122630277"},{"key":"e_1_3_2_2_49_1","volume-title":"Julian Stecklina, Thomas Prescher, and Daniel Gruss.","author":"Schwarz Michael","year":"2019"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304060"},{"key":"e_1_3_2_2_51_1","volume-title":"CheckMate: Automated Synthesis of Hardware Exploits and Security Litmus Tests. In 51st Annual IEEE\/ACM International Symposium on Microarchitecture, MICRO 2018","author":"Trippel Caroline","year":"2018"},{"key":"e_1_3_2_2_52_1","unstructured":"Paul Turner. 2018. Retpoline: a software construct for preventing branch-target-injection. https:\/\/support.google.com\/faqs\/answer\/7625886  Paul Turner. 2018. Retpoline: a software construct for preventing branch-target-injection. https:\/\/support.google.com\/faqs\/answer\/7625886"},{"key":"e_1_3_2_2_53_1","volume-title":"RIDL: Rogue In-flight Data Load. In S&P.","author":"van Schaik Stephan","year":"2019"},{"key":"e_1_3_2_2_54_1","volume-title":"Tulika Mitra, and Abhik Roychoudhury.","author":"Wang Guanhua","year":"2019"},{"key":"e_1_3_2_2_55_1","unstructured":"G. Wang S. Chattopadhyay I. Gotovchits T. Mitra and A. Roychoudhury. 2019. oo7: Low-overhead Defense against Spectre attacks via Program Analysis. IEEE Transactions on Software Engineering (2019).  G. Wang S. Chattopadhyay I. Gotovchits T. Mitra and A. Roychoudhury. 2019. oo7: Low-overhead Defense against Spectre attacks via Program Analysis. IEEE Transactions on Software Engineering (2019)."},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358306"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2014.6853201"},{"key":"e_1_3_2_2_58_1","volume-title":"SPEECHMINER: A Framework for Investigating and Measuring Speculative Execution Vulnerabilities. In NDSS.","author":"Xiao Yuan","year":"2020"},{"key":"e_1_3_2_2_59_1","volume-title":"23rd USENIX Security Symposium. 719--732","author":"Yarom Yuval","year":"2014"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-017-0152-y"},{"key":"e_1_3_2_2_61_1","volume-title":"32nd IEEE Computer Security Foundations Symposium, CSF. 272--287","author":"Zagieboylo Drew"}],"event":{"name":"CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security","location":"Virtual Event USA","acronym":"CCS '20","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372297.3417246","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372297.3417246","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:33:25Z","timestamp":1750185205000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372297.3417246"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,30]]},"references-count":61,"alternative-id":["10.1145\/3372297.3417246","10.1145\/3372297"],"URL":"https:\/\/doi.org\/10.1145\/3372297.3417246","relation":{},"subject":[],"published":{"date-parts":[[2020,10,30]]},"assertion":[{"value":"2020-11-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}