{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T16:30:11Z","timestamp":1773246611755,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":60,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,6,17]],"date-time":"2023-06-17T00:00:00Z","timestamp":1686960000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["CNS-2046359"],"award-info":[{"award-number":["CNS-2046359"]}]},{"name":"NSF","award":["CCF-2217099"],"award-info":[{"award-number":["CCF-2217099"]}]},{"name":"AFOSR","award":["FA9550-20-1-0402"],"award-info":[{"award-number":["FA9550-20-1-0402"]}]},{"name":"AFOSR","award":["FA9550-22-1-0511"],"award-info":[{"award-number":["FA9550-22-1-0511"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,6,17]]},"DOI":"10.1145\/3579371.3589094","type":"proceedings-article","created":{"date-parts":[[2023,6,16]],"date-time":"2023-06-16T20:25:28Z","timestamp":1686947128000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Pensieve: Microarchitectural Modeling for Security Evaluation"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8695-5139","authenticated-orcid":false,"given":"Yuheng","family":"Yang","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8468-8409","authenticated-orcid":false,"given":"Thomas","family":"Bourgeat","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3921-9440","authenticated-orcid":false,"given":"Stella","family":"Lau","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6206-9674","authenticated-orcid":false,"given":"Mengjia","family":"Yan","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,6,17]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3466752.3480074"},{"key":"e_1_3_2_1_2_1","volume-title":"Artefact Evaluation for GhostMinion. https:\/\/github.com\/SamAinsworth\/reproduce-ghostminion-paper. Accessed","author":"Ainsworth Sam","year":"2022","unstructured":"Sam Ainsworth . 2022. Artefact Evaluation for GhostMinion. https:\/\/github.com\/SamAinsworth\/reproduce-ghostminion-paper. Accessed 26 October 2022 . Sam Ainsworth. 2022. Artefact Evaluation for GhostMinion. https:\/\/github.com\/SamAinsworth\/reproduce-ghostminion-paper. Accessed 26 October 2022."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA45697.2020.00022"},{"key":"e_1_3_2_1_4_1","volume-title":"Verifying Hardware Security Modules with Information-Preserving Refinement. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Athalye Anish","year":"2022","unstructured":"Anish Athalye , M. Frans Kaashoek , and Nickolai Zeldovich . 2022 . Verifying Hardware Security Modules with Information-Preserving Refinement. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22) . USENIX Association. Anish Athalye, M. Frans Kaashoek, and Nickolai Zeldovich. 2022. Verifying Hardware Security Modules with Information-Preserving Refinement. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2019.00020"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446708"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363194"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024716.2024718"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676711"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.275352"},{"key":"e_1_3_2_1_12_1","unstructured":"Cadence Design Systems Inc. 2022. Jasper RTL Apps. http:\/\/www.jasper-da.com\/products\/jaspergold-apps. Accessed 26 October 2022.  Cadence Design Systems Inc. 2022. Jasper RTL Apps. http:\/\/www.jasper-da.com\/products\/jaspergold-apps. Accessed 26 October 2022."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00027"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2021.3122830"},{"key":"e_1_3_2_1_16_1","volume-title":"Model Checking","author":"Clarke Edmund","unstructured":"Edmund Clarke , Orna Grumberg , Daniel Kroening , Doron Peled , and Helmut Veith . 2018. Model Checking , second edition. MIT Press . Edmund Clarke, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. 2018. Model Checking, second edition. MIT Press."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97298"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_20_1","volume-title":"Computer Aided Verification","author":"Dill David L.","unstructured":"David L. Dill . 1996. The Murphi verification system . In Computer Aided Verification . Springer Berlin Heidelberg . David L. Dill. 1996. The Murphi verification system. In Computer Aided Verification. Springer Berlin Heidelberg."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18072.2020.9218572"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2019.8715004"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2022.3152666"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3411504.3421216"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA52012.2021.00073"},{"key":"e_1_3_2_1_26_1","volume-title":"Translation Leak-aside Buffer: Defeating Cache Side-channel Protections with TLB Attacks. In 27th USENIX Security Symposium (USENIX Security 18)","author":"Gras Ben","year":"2018","unstructured":"Ben Gras , Kaveh Razavi , Herbert Bos , and Cristiano Giuffrida . 2018 . Translation Leak-aside Buffer: Defeating Cache Side-channel Protections with TLB Attacks. In 27th USENIX Security Symposium (USENIX Security 18) . USENIX Association. Ben Gras, Kaveh Razavi, Herbert Bos, and Cristiano Giuffrida. 2018. Translation Leak-aside Buffer: Defeating Cache Side-channel Protections with TLB Attacks. In 27th USENIX Security Symposium (USENIX Security 18). USENIX Association."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417246"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00036"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00011"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3466752.3480087"},{"key":"e_1_3_2_1_31_1","volume-title":"McMillan","author":"Jhala Ranjit","year":"2001","unstructured":"Ranjit Jhala and Kenneth L . McMillan . 2001 . Microarchitecture Verification by Compositional Model Checking. In Proceedings of the 13th International Conference on Computer Aided Verification. Springer-Verlag . Ranjit Jhala and Kenneth L. McMillan. 2001. Microarchitecture Verification by Compositional Model Checking. In Proceedings of the 13th International Conference on Computer Aided Verification. Springer-Verlag."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3316781.3317903"},{"key":"e_1_3_2_1_33_1","volume-title":"Speculative buffer overflows: Attacks and defenses. arXiv preprint arXiv:1807.03757","author":"Kiriansky Vladimir","year":"2018","unstructured":"Vladimir Kiriansky and Carl Waldspurger . 2018. Speculative buffer overflows: Attacks and defenses. arXiv preprint arXiv:1807.03757 ( 2018 ). Vladimir Kiriansky and Carl Waldspurger. 2018. Speculative buffer overflows: Attacks and defenses. arXiv preprint arXiv:1807.03757 (2018)."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_3_2_1_35_1","volume-title":"12th USENIX Workshop on Offensive Technologies (WOOT 18)","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 Buffer . In 12th USENIX Workshop on Offensive Technologies (WOOT 18) . USENIX Association. Esmaeil Mohammadian Koruyeh, Khaled N. Khasawneh, Chengyu Song, and Nael Abu-Ghazaleh. 2018. Spectre Returns! Speculation Attacks using the Return Stack Buffer. In 12th USENIX Workshop on Offensive Technologies (WOOT 18). USENIX Association."},{"key":"e_1_3_2_1_36_1","volume-title":"Specifying systems: the TLA+ language and tools for hardware and software engineers","author":"Lamport Leslie","unstructured":"Leslie Lamport . 2002. Specifying systems: the TLA+ language and tools for hardware and software engineers . Addison-Wesley Longman Publishing Co., Inc. Leslie Lamport. 2002. Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley Longman Publishing Co., Inc."},{"key":"e_1_3_2_1_37_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) . USENIX Association. 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). USENIX Association."},{"key":"e_1_3_2_1_38_1","volume-title":"DOLMA: Securing Speculation with the Principle of Transient Non-Observability. In 30th USENIX Security Symposium (USENIX Security 21)","author":"Loughlin Kevin","year":"2021","unstructured":"Kevin Loughlin , Ian Neal , Jiacheng Ma , Elisa Tsai , Ofir Weisse , Satish Narayanasamy , and Baris Kasikci . 2021 . DOLMA: Securing Speculation with the Principle of Transient Non-Observability. In 30th USENIX Security Symposium (USENIX Security 21) . USENIX Association. Kevin Loughlin, Ian Neal, Jiacheng Ma, Elisa Tsai, Ofir Weisse, Satish Narayanasamy, and Baris Kasikci. 2021. DOLMA: Securing Speculation with the Principle of Transient Non-Observability. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243761"},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of the International Symposium on Shared Memory Multiprocessing.","author":"McMillan KL","year":"1992","unstructured":"KL McMillan and J Schwalbe . 1992 . Formal verification of the Gigamax Cache Consistency Protocol . In Proceedings of the International Symposium on Shared Memory Multiprocessing. KL McMillan and J Schwalbe. 1992. Formal verification of the Gigamax Cache Consistency Protocol. In Proceedings of the International Symposium on Shared Memory Multiprocessing."},{"key":"e_1_3_2_1_41_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. 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."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3470496.3527412"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.3233\/sat190101"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507729"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358314"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3310273.3321558"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3307650.3322216"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29959-0_14"},{"key":"e_1_3_2_1_50_1","volume-title":"https:\/\/github.com\/shioyadan\/Konata. Accessed","author":"Shioya Ryota","year":"2022","unstructured":"Ryota Shioya . 2022. Konata. https:\/\/github.com\/shioyadan\/Konata. Accessed 26 October 2022 . Ryota Shioya. 2022. Konata. https:\/\/github.com\/shioyadan\/Konata. Accessed 26 October 2022."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00081"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2953709"},{"key":"e_1_3_2_1_54_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. 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."},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358306"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314647"},{"key":"e_1_3_2_1_57_1","volume-title":"SPEECHMINER: A Framework for Investigating and Measuring Speculative Execution Vulnerabilities. In Network and Distributed System Security Symposium.","author":"Xiao Yuan","year":"2020","unstructured":"Yuan Xiao , Yinqian Zhang , and Radu Teodorescu . 2020 . SPEECHMINER: A Framework for Investigating and Measuring Speculative Execution Vulnerabilities. In Network and Distributed System Security Symposium. Yuan Xiao, Yinqian Zhang, and Radu Teodorescu. 2020. SPEECHMINER: A Framework for Investigating and Measuring Speculative Execution Vulnerabilities. In Network and Distributed System Security Symposium."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00042"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA45697.2020.00064"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358274"}],"event":{"name":"ISCA '23: 50th Annual International Symposium on Computer Architecture","location":"Orlando FL USA","acronym":"ISCA '23","sponsor":["SIGARCH ACM Special Interest Group on Computer Architecture","IEEE"]},"container-title":["Proceedings of the 50th Annual International Symposium on Computer Architecture"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3579371.3589094","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3579371.3589094","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3579371.3589094","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:39Z","timestamp":1750178799000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3579371.3589094"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,17]]},"references-count":60,"alternative-id":["10.1145\/3579371.3589094","10.1145\/3579371"],"URL":"https:\/\/doi.org\/10.1145\/3579371.3589094","relation":{},"subject":[],"published":{"date-parts":[[2023,6,17]]},"assertion":[{"value":"2023-06-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}