{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:05:36Z","timestamp":1755907536301,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":79,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,12,2]],"date-time":"2024-12-02T00:00:00Z","timestamp":1733097600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100006374","name":"Intel Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["1837132"],"award-info":[{"award-number":["1837132"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-20-C0156"],"award-info":[{"award-number":["FA8750-20-C0156"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,12,2]]},"DOI":"10.1145\/3658644.3690214","type":"proceedings-article","created":{"date-parts":[[2024,12,9]],"date-time":"2024-12-09T12:19:20Z","timestamp":1733746760000},"page":"2756-2770","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["SemPat: From Hyperproperties to Attack Patterns for Scalable Analysis of Microarchitectural Security"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7704-304X","authenticated-orcid":false,"given":"Adwait","family":"Godbole","sequence":"first","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6954-2292","authenticated-orcid":false,"given":"Yatin A.","family":"Manerkar","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, MI, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6190-8707","authenticated-orcid":false,"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,12,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/fmcad.2013.6679385"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3-030--99524--9_24"},{"key":"e_1_3_2_1_5_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org."},{"key":"e_1_3_2_1_6_1","unstructured":"Clark W. Barrett Roberto Sebastiani Sanjit A. Seshia and Cesare Tinelli. 2009. Satisfiability Modulo Theories. In Handbook of Satisfiability."},{"key":"e_1_3_2_1_7_1","volume-title":"Michael Schwarz, Moritz Lipp, Benjamin von","author":"Canella Claudio","year":"2019","unstructured":"Claudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp, Benjamin von Berg, Philipp Ortner, Frank Piessens, Dmitry Evtyushkin, and Daniel Gruss. 2019. A Systematic Evaluation of Transient Execution Attacks and Defenses. (Aug. 2019), 249--266. https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/canella"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363219"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/sp46214.2022.9833707"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICAPP.2002.1173575"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00027"},{"key":"e_1_3_2_1_13_1","volume-title":"et. al","author":"Wolf Claire","year":"2022","unstructured":"Claire Wolf, et. al. 2022. SymbiYosys. https:\/\/github.com\/YosysHQ\/sby."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_3_2_1_15_1","volume-title":"Hyperproperties. 2008 21st IEEE Computer Security Foundations Symposium","author":"Michael","year":"2008","unstructured":"Michael R. Clarkson and Fred B. Schneider. 2008. Hyperproperties. 2008 21st IEEE Computer Security Foundations Symposium (2008), 51--65."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2021.24286"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563037"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_19_1","volume-title":"BINSEC\/SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis. 2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER)","volume":"1","author":"David Robin","year":"2016","unstructured":"Robin David, S\u00e9bastien Bardin, Thanh Dinh Ta, Laurent Mounier, Josselin Feist, Marie-Laure Potet, and Jean-Yves Marion. 2016. BINSEC\/SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis. 2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER), Vol. 1 (2016), 653--656. https:\/\/api.semanticscholar.org\/CorpusID:7488274"},{"volume-title":"International Conference on Tools and Algorithms for Construction and Analysis of Systems.","author":"Leonardo","key":"e_1_3_2_1_20_1","unstructured":"Leonardo Mendonc ca de Moura and Nikolaj S. Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In International Conference on Tools and Algorithms for Construction and Analysis of Systems."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560555"},{"key":"e_1_3_2_1_22_1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE)","author":"Fadiheh Mohammad Rahmani","year":"2018","unstructured":"Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark W. Barrett, Subhasish Mitra, and Wolfgang Kunz. 2018. Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking. 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE) (2018), 994--999."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354175"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/S13389-016-0141--6"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623112"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640418"},{"key":"e_1_3_2_1_27_1","volume-title":"Seshia","author":"Godbole Adwait","year":"2024","unstructured":"Adwait Godbole, Yatin A. Manerkar, and Sanjit A. Seshia. 2024. SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns. arXiv preprint arXiv: 2406.05403 (2024)."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.34727\/2023\/isbn.978--3--85448-060-0_35"},{"key":"e_1_3_2_1_29_1","volume-title":"Unwinding and Inference Control. 1984 IEEE Symposium on Security and Privacy","author":"Joseph","year":"1984","unstructured":"Joseph A. Goguen and Jos\u00e9 Meseguer. 1984. Unwinding and Inference Control. 1984 IEEE Symposium on Security and Privacy (1984), 75--75."},{"key":"e_1_3_2_1_30_1","volume-title":"ABSynthe: Automatic Blackbox Side-channel Synthesis on Commodity Microarchitectures. In 27th Annual Network and Distributed System Security Symposium, NDSS 2020","author":"Gras Ben","year":"2020","unstructured":"Ben Gras, Cristiano Giuffrida, Michael Kurth, Herbert Bos, and Kaveh Razavi. 2020. ABSynthe: Automatic Blackbox Side-channel Synthesis on Commodity Microarchitectures. In 27th Annual Network and Distributed System Security Symposium, NDSS 2020, San Diego, California, USA, February 23--26, 2020. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss-paper\/absynthe-automatic-blackbox-side-channel-synthesis-on-commodity-microarchitectures\/"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417246"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/sp40000.2020.00011"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00036"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380428"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/seed51797.2021.00023"},{"key":"e_1_3_2_1_36_1","unstructured":"Intel. 2023. Data Operand Independent Timing Instruction Set Architecture (ISA) Guidance. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/software-security-guidance\/best-practices\/data-operand-independent-timing-isa-guidance.html Accessed: 2023--11--23."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-017-0294-5"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_39_1","unstructured":"Paul Kocher. 2018. Spectre Mitigations in Microsoft's C\/C Compiler. https:\/\/www.paulkocher.com\/doc\/MicrosoftCompilerSpectreMitigation.html"},{"key":"e_1_3_2_1_40_1","volume-title":"Spectre Attacks: Exploiting Speculative Execution. 2019 IEEE Symposium on Security and Privacy (SP)","author":"Kocher Paul C.","year":"2019","unstructured":"Paul C. Kocher, Daniel Genkin, Daniel Gruss, Werner Haas, Michael Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2019. Spectre Attacks: Exploiting Speculative Execution. 2019 IEEE Symposium on Security and Privacy (SP) (2019), 1--19."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/mdat.2024.3352537"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1561\/3300000008"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.966493"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/micro.2000.898055"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/360128.360133"},{"key":"e_1_3_2_1_46_1","volume-title":"USENIX Security Symposium.","author":"Lipp Moritz","year":"2018","unstructured":"Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul C. Kocher, Daniel Genkin, Yuval Yarom, and Michael Hamburg. 2018. Meltdown: Reading Kernel Memory from User Space. In USENIX Security Symposium."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/sp.2015.43"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872399"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243761"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--1--4615--3190--6_3"},{"key":"e_1_3_2_1_51_1","volume-title":"Downfall: Exploiting Speculative Data Gathering. In 32nd USENIX Security Symposium (USENIX Security 23)","author":"Moghimi Daniel","year":"2023","unstructured":"Daniel Moghimi. 2023. Downfall: Exploiting Speculative Data Gathering. In 32nd USENIX Security Symposium (USENIX Security 23). USENIX Association, Anaheim, CA, 7179--7193. https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/moghimi"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3470496.3527412"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/L-CA.2005.1"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","unstructured":"Hamed Nemati Pablo Buiras Andreas Lindner Roberto Guanciale and Swen Jacobs. 2020. Validation of Abstract Side-Channel Models for Computer Architectures. (2020) 225--248. https:\/\/doi.org\/10.1007\/978--3-030--53288--8_12","DOI":"10.1007\/978--3-030--53288--8_12"},{"key":"e_1_3_2_1_55_1","volume-title":"DifFuzz: Differential Fuzzing for Side-Channel Analysis. 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE)","author":"Nilizadeh Shirin","year":"2018","unstructured":"Shirin Nilizadeh, Yannic Noller, and Corina S. Pasareanu. 2018. DifFuzz: Differential Fuzzing for Side-Channel Analysis. 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE) (2018), 176--187."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464817"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507729"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179391"},{"key":"e_1_3_2_1_59_1","volume-title":"34th International Conference on Computer Aided Verification (CAV) (Lecture Notes in Computer Science","volume":"551","author":"Polgreen Elizabeth","unstructured":"Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, and Sanjit A. Seshia. 2022. UCLID5: Multi-modal Formal Modeling, Verification, and Synthesis. In 34th International Conference on Computer Aided Verification (CAV) (Lecture Notes in Computer Science, Vol. 13371). Springer, 538--551."},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/sp46214.2022.9833774"},{"key":"e_1_3_2_1_61_1","unstructured":"John Rushby. 1992. Noninterference Transitivity and Channel-Control Security Policies. Technical Report. http:\/\/www.csl.sri.com\/papers\/csl-92--2\/"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/isca52012.2021.00035"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3354252"},{"key":"e_1_3_2_1_64_1","volume-title":"NetSpectre: Read Arbitrary Memory over Network. ArXiv","author":"Schwarz Michael","year":"2019","unstructured":"Michael Schwarz, Martin Schwarzl, Moritz Lipp, and Daniel Gruss. 2019. NetSpectre: Read Arbitrary Memory over Network. ArXiv, Vol. abs\/1807.10535 (2019)."},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2006.39"},{"key":"e_1_3_2_1_66_1","first-page":"170","volume-title":"38th Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO'05)","author":"Sha Tingting","year":"2005","unstructured":"Tingting Sha, Milo M. K. Martin, and Amir Roth. 2005. Scalable store-load forwarding via store queue index prediction. 38th Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO'05) (2005), 12 pp.--170."},{"key":"e_1_3_2_1_67_1","volume-title":"Dynamic Instruction Reuse. Conference Proceedings. The 24th Annual International Symposium on Computer Architecture","author":"Sodani Avinash","year":"1997","unstructured":"Avinash Sodani and Gurindar S. Sohi. 1997. Dynamic Instruction Reuse. Conference Proceedings. The 24th Annual International Symposium on Computer Architecture (1997), 194--205."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2006.26"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2019.2910010"},{"key":"e_1_3_2_1_71_1","volume-title":"TheHuzz: Instruction Fuzzing of Processors Using Golden-Reference Models for Finding Software-Exploitable Vulnerabilities. ArXiv","author":"Tyagi Aakash","year":"2022","unstructured":"Aakash Tyagi, Addison Crump, Ahmad-Reza Sadeghi, Garrett Persyn, Jeyavijayan Rajendran, Patrick Jauernig, and Rahul Kande. 2022. TheHuzz: Instruction Fuzzing of Processors Using Golden-Reference Models for Finding Software-Exploitable Vulnerabilities. ArXiv, Vol. abs\/2201.09941 (2022)."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484810"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1109\/sp.2019.00087"},{"key":"e_1_3_2_1_74_1","volume-title":"Deian Stefan, and Ranjit Jhala.","author":"von Gleissenthall Klaus","year":"2019","unstructured":"Klaus von Gleissenthall, Rami G\u00f6khan Kici, Deian Stefan, and Ranjit Jhala. 2019. IODINE: Verifying Constant-Time Execution of Hardware. ArXiv, Vol. abs\/1910.03111 (2019). https:\/\/api.semanticscholar.org\/CorpusID:197672843"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385897"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623192"},{"key":"e_1_3_2_1_77_1","volume-title":"Osiris: Automated Discovery of Microarchitectural Side Channels. In 30th USENIX Security Symposium (USENIX Security 21)","author":"Weber Daniel","year":"2021","unstructured":"Daniel Weber, Ahmad Ibrahim, Hamed Nemati, Michael Schwarz, and Christian Rossow. 2021. Osiris: Automated Discovery of Microarchitectural Side Channels. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association, 1415--1432. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/weber"},{"key":"e_1_3_2_1_78_1","unstructured":"Clifford Wolf Johann Glaser and Johannes Kepler. 2013. Yosys-A Free Verilog Synthesis Suite."},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.5555\/3539845.3539954"}],"event":{"name":"CCS '24: ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Salt Lake City UT USA","acronym":"CCS '24"},"container-title":["Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3690214","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3658644.3690214","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T06:11:56Z","timestamp":1755843116000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3690214"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,2]]},"references-count":79,"alternative-id":["10.1145\/3658644.3690214","10.1145\/3658644"],"URL":"https:\/\/doi.org\/10.1145\/3658644.3690214","relation":{},"subject":[],"published":{"date-parts":[[2024,12,2]]},"assertion":[{"value":"2024-12-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}