{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:40:34Z","timestamp":1773193234330,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,11,15]],"date-time":"2023-11-15T00:00:00Z","timestamp":1700006400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Spanish Ministry of Science and Innovation","award":["TED2021-132464B-I00 PRODIGY, RYC2021-032614-I, PID2022-142290OB-I00 ESPADA"],"award-info":[{"award-number":["TED2021-132464B-I00 PRODIGY, RYC2021-032614-I, PID2022-142290OB-I00 ESPADA"]}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101020415"],"award-info":[{"award-number":["101020415"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,11,15]]},"DOI":"10.1145\/3576915.3623192","type":"proceedings-article","created":{"date-parts":[[2023,11,21]],"date-time":"2023-11-21T12:35:13Z","timestamp":1700570113000},"page":"2128-2142","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-0863-5487","authenticated-orcid":false,"given":"Zilong","family":"Wang","sequence":"first","affiliation":[{"name":"IMDEA Software Institute & Universidad Polit\u00e9cnica de Madrid, Madrid, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2425-9354","authenticated-orcid":false,"given":"Gideon","family":"Mohr","sequence":"additional","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0826-4425","authenticated-orcid":false,"given":"Klaus","family":"von Gleissenthall","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Amsterdam, Amsterdam, Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3459-2214","authenticated-orcid":false,"given":"Jan","family":"Reineke","sequence":"additional","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5767-555X","authenticated-orcid":false,"given":"Marco","family":"Guarnieri","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}]}],"member":"320","published-online":{"date-parts":[[2023,11,21]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n. d.]. DarkRISCV processor. https:\/\/github.com\/darklife\/darkriscv"},{"key":"e_1_3_2_1_2_1","unstructured":"[n. d.]. Ibex: An embedded 32 bit RISC-V CPU core. https:\/\/github.com\/lowRISC\/ ibex"},{"key":"e_1_3_2_1_3_1","unstructured":"[n. d.]. Ibex RISC-V Core ? Multiplier\/Divider Block. https:\/\/ibex-core. readthedocs.io\/en\/latest\/03_reference\/instruction_decode_execute.html#mult- div"},{"key":"e_1_3_2_1_4_1","unstructured":"[n. d.]. Icarus Verilog. https:\/\/github.com\/steveicarus\/iverilog"},{"key":"e_1_3_2_1_5_1","unstructured":"[n. d.]. RISC-V Sodor processor. https:\/\/github.com\/ucb-bar\/riscv-sodor"},{"key":"e_1_3_2_1_6_1","unstructured":"[n. d.]. LeaVe implementation and benchmarks. https:\/\/github.com\/ zilongwang123\/LeaVe"},{"key":"e_1_3_2_1_7_1","unstructured":"[n. d.]. Yices 2 SMT Solver. https:\/\/yices.csl.sri.com"},{"key":"e_1_3_2_1_8_1","unstructured":"[n. d.]. Yosys Open SYnthesis Suite. https:\/\/github.com\/YosysHQ\/yosys"},{"key":"e_1_3_2_1_9_1","volume-title":"Francc ois Dupressoir, and Michael Emmi","author":"Almeida Jos\u00e9 Bacelar","year":"2016","unstructured":"Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francc ois Dupressoir, and Michael Emmi. 2016. Verifying Constant-Time Implementations. In USENIX Security."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_1_11_1","unstructured":"Anish Athalye M. Frans Kaashoek and Nickolai Zeldovich. 2022. Verifying Hardware Security Modules with Information-Preserving Refinement. In OSDI."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560600"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Pablo Buiras Hamed Nemati Andreas Lindner and Roberto Guanciale. 2021. Validation of Side-Channel Models via Observation Refinement. In MICRO-54. ACM. https:\/\/doi.org\/10.1145\/3466752.3480130","DOI":"10.1145\/3466752.3480130"},{"key":"e_1_3_2_1_15_1","volume-title":"Foreshadow: Extracting the Keys to the Intel SGX Kingdom with Transient Out-of-Order Execution. In USENIX Security.","author":"Bulck Jo Van","year":"2018","unstructured":"Jo Van Bulck et al. 2018. Foreshadow: Extracting the Keys to the Intel SGX Kingdom with Transient Out-of-Order Execution. In USENIX Security."},{"key":"e_1_3_2_1_16_1","volume-title":"Dill","author":"Burch Jerry R.","year":"1994","unstructured":"Jerry R. Burch and David L. Dill. 1994. Automatic verification of pipelined microprocessor control. In CAV."},{"key":"e_1_3_2_1_17_1","volume-title":"Leila Delshadtehrani, Michael Taylor, Manuel Egele, and Ajay Joshi.","author":"Canakci Sadullah","year":"2022","unstructured":"Sadullah Canakci, Chathura Rajapaksha, Anoop Mysore Nataraja, Leila Delshadtehrani, Michael Taylor, Manuel Egele, and Ajay Joshi. 2022. ProcessorFuzz: Guiding Processor Fuzzing using Control and Status Registers. arXiv preprint arXiv:2209.01789 (2022)."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Sunjay Cauligi Craig Disselkoen Klaus V. Gleissenthall Dean Tullsen Deian Stefan Tamara Rezk and Gilles Barthe. 2020. Constant-Time Foundations for the New Spectre Era. In PLDI. https:\/\/doi.org\/10.1145\/3385412.3385970","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_1_20_1","volume-title":"Wenjie Xiong, Sercan Sari, Y Serhan Gener, Corine Lu, Onur Demir, and Jakub Szefer.","author":"Deng Shuwen","year":"2019","unstructured":"Shuwen Deng, Doug uhan G\u00fcm\u00fccs oug lu, Wenjie Xiong, Sercan Sari, Y Serhan Gener, Corine Lu, Onur Demir, and Jakub Szefer. 2019. SecChisel framework for security verification of secure processor architectures. In HASP@ISCA."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Xaver Fabian Marco Patrignani and Marco Guarnieri. 2022. Automatic Detection of Speculative Execution Combinations. In CCS.","DOI":"10.1145\/3548606.3560555"},{"key":"e_1_3_2_1_22_1","article-title":"An exhaustive approach to detecting transient execution side channels in RTL designs of processors","volume":"72","author":"Fadiheh Mohammad Rahmani","year":"2022","unstructured":"Mohammad Rahmani Fadiheh, Alex Wezel, Johannes M\u00fcller, J\u00f6rg Bormann, Sayak Ray, Jason M Fung, Subhasish Mitra, Dominik Stoffel, and Wolfgang Kunz. 2022. An exhaustive approach to detecting transient execution side channels in RTL designs of processors. IEEE Trans. Comput., Vol. 72, 1 (2022).","journal-title":"IEEE Trans. Comput."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan and K Rustan M Leino. 2001. Houdini an annotation assistant for ESC\/Java. In FME.","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Ben Gras Cristiano Giuffrida Michael Kurth Herbert Bos and Kaveh Razavi. 2020. ABSynthe: Automatic Blackbox Side-channel Synthesis on Commodity Microarchitectures. In NDSS.","DOI":"10.14722\/ndss.2020.23018"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Roberto Guanciale Musard Balliu and Mads Dam. 2020. InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal Analysis. In CCS.","DOI":"10.1145\/3372297.3417246"},{"key":"e_1_3_2_1_26_1","volume-title":"textscSpectector: Principled detection of speculative information flows","author":"Guarnieri Marco","unstructured":"Marco Guarnieri, Boris K\u00f6pf, Jos\u00e9 F. Morales, Jan Reineke, and Andr\u00e9s S\u00e1nchez. 2020. textscSpectector: Principled detection of speculative information flows. In IEEE S&P."},{"key":"e_1_3_2_1_27_1","volume-title":"Hardware-software contracts for secure speculation","author":"Guarnieri Marco","unstructured":"Marco Guarnieri, Boris K\u00f6pf, Jan Reineke, and Pepe Vila. 2021. Hardware-software contracts for secure speculation. In IEEE S&P."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3282444"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Jaewon Hur Suhwan Song Sunwoo Kim and Byoungyoung Lee. 2022. SpecDoctor: Differential Fuzz Testing to Find Transient Execution Vulnerabilities. In CCS.","DOI":"10.1145\/3548606.3560578"},{"key":"e_1_3_2_1_30_1","volume-title":"Microarchitecture verification by compositional model checking","author":"Jhala Ranjit","unstructured":"Ranjit Jhala and Kenneth L McMillan. 2001. Microarchitecture verification by compositional model checking. In CAV. Springer."},{"key":"e_1_3_2_1_31_1","unstructured":"Rahul Kande Addison Crump Garrett Persyn Patrick Jauernig Ahmad-Reza Sadeghi Aakash Tyagi and Jeyavijayan Rajendran. 2022. TheHuzz: Instruction Fuzzing of Processors Using Golden-Reference Models for Finding Software-Exploitable Vulnerabilities. In USENIX Security."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_3_2_1_33_1","unstructured":"Ulrich K\u00fchne Sven Beyer Jorg Bormann and John Barstow. 2010. Automated formal verification of processors based on architectural models. In FMCAD."},{"key":"e_1_3_2_1_34_1","volume-title":"Meltdown: Reading Kernel Memory from User Space. In USENIX Security.","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 USENIX Security."},{"key":"e_1_3_2_1_35_1","volume-title":"Medusa: Microarchitectural Data Leakage via Automated Attack Synthesis Background Superscalar Memory Architecture. In USENIX Security.","author":"Moghimi Daniel","year":"2020","unstructured":"Daniel Moghimi, Moritz Lipp, Berk Sunar, and Michael Schwarz. 2020. Medusa: Microarchitectural Data Leakage via Automated Attack Synthesis Background Superscalar Memory Architecture. In USENIX Security."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"David Molnar Matt Piotrowski David Schultz and David Wagner. 2005. The Program Counter Security Model: Automatic Detection and Removal of Control-Flow Side Channel Attacks. In ICISC. 156--168.","DOI":"10.1007\/11734727_14"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Nicholas Mosier Hanna Lachnitt Hamed Nemati and Caroline Trippel. 2022. Axiomatic hardware-software contracts for security. In ISCA.","DOI":"10.1145\/3470496.3527412"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Hamed Nemati Pablo Buiras Andreas Lindner Roberto Guanciale and Swen Jacobs. 2020. Validation of Abstract Side-Channel Models for Computer Architectures. In CAV.","DOI":"10.1007\/978-3-030-53288-8_12"},{"key":"e_1_3_2_1_39_1","volume-title":"Revizor: Testing Black-Box CPUs against Speculation Contracts. In ASPLOS.","author":"Oleksenko Oleksii","year":"2022","unstructured":"Oleksii Oleksenko, Christof Fetzer, Boris K\u00f6pf, and Mark Silberstein. 2022. Revizor: Testing Black-Box CPUs against Speculation Contracts. In ASPLOS."},{"key":"e_1_3_2_1_40_1","volume-title":"Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing","author":"Oleksenko Oleksii","unstructured":"Oleksii Oleksenko, Marco Guarnieri, Boris K\u00f6pf, and Mark Silberstein. 2023. Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing. In IEEE S&P."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICVD.1999.745161"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Marco Patrignani and Marco Guarnieri. 2021. Exorcising Spectres with Secure Compilers. In CCS.","DOI":"10.1145\/3460120.3484534"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Chathura Rajapaksha Leila Delshadtehrani Manuel Egele and Ajay Joshi. 2023. SIGFuzz: A Framework for Discovering Microarchitectural Timing Side Channels. In DATE. https:\/\/doi.org\/10.23919\/DATE56975.2023.10136966","DOI":"10.23919\/DATE56975.2023.10136966"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Alastair Reid Rick Chen Anastasios Deligiannis David Gilday David Hoyes Will Keen Ashan Pathirane Owen Shepherd Peter Vrabel and Ali Zaidi. 2016. End-to-end verification of processors with ISA-Formal. In CAV.","DOI":"10.1007\/978-3-319-41540-6_3"},{"key":"e_1_3_2_1_45_1","volume-title":"Deian Stefan, and Ranjit Jhala.","author":"v. Gleissenthall Klaus","year":"2021","unstructured":"Klaus v. Gleissenthall, Rami G\u00f6khan Kici, Deian Stefan, and Ranjit Jhala. 2021. Solver-Aided Constant-Time Hardware Verification. In CCS."},{"key":"e_1_3_2_1_46_1","volume-title":"RIDL: Rogue In-flight Data Load. In S&P.","author":"van Schaik Stephan","year":"2019","unstructured":"Stephan van Schaik et al. 2019. RIDL: Rogue In-flight Data Load. In S&P."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"crossref","unstructured":"Marco Vassena et al. 2021. Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade. In POPL.","DOI":"10.1145\/3410264"},{"key":"e_1_3_2_1_48_1","volume-title":"Deian Stefan, and Ranjit Jhala.","author":"von Gleissenthall Klaus","year":"2019","unstructured":"Klaus von Gleissenthall, Rami G\u00f6 khan Kici, Deian Stefan, and Ranjit Jhala. 2019. IODINE: Verifying Constant-Time Execution of Hardware. In USENIX Security."},{"key":"e_1_3_2_1_49_1","volume-title":"Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. CoRR","author":"Wang Zilong","year":"2023","unstructured":"Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, and Marco Guarnieri. 2023. Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. CoRR, Vol. abs\/2305.06979 (2023)."},{"key":"e_1_3_2_1_50_1","volume-title":"Osiris: Automated Discovery of Microarchitectural Side Channels. In USENIX Security.","author":"Daniel Weber","year":"2021","unstructured":"Daniel Weber et al. 2021. Osiris: Automated Discovery of Microarchitectural Side Channels. In USENIX Security."},{"key":"e_1_3_2_1_51_1","unstructured":"Yuval Yarom and Katrina Falkner. 2014. FlushReload: A High Resolution Low Noise L3 Cache Side-channel Attack. In USENIX Security."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD51958.2021.9643584"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694372"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"crossref","unstructured":"Hongce Zhang Weikun Yang Grigory Fedyukovich Aarti Gupta and Sharad Malik. 2020. Synthesizing environment invariants for modular hardware verification. In VMCAI.","DOI":"10.1007\/978-3-030-39322-9_10"}],"event":{"name":"CCS '23: ACM SIGSAC Conference on Computer and Communications Security","location":"Copenhagen Denmark","acronym":"CCS '23","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576915.3623192","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3576915.3623192","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T01:42:34Z","timestamp":1755740554000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576915.3623192"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,15]]},"references-count":54,"alternative-id":["10.1145\/3576915.3623192","10.1145\/3576915"],"URL":"https:\/\/doi.org\/10.1145\/3576915.3623192","relation":{},"subject":[],"published":{"date-parts":[[2023,11,15]]},"assertion":[{"value":"2023-11-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}