{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T02:44:37Z","timestamp":1778121877740,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":57,"publisher":"ACM","funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101020415, 101115046"],"award-info":[{"award-number":["101020415, 101115046"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Ministerio de Ciencia, Innovaci\u00f3n y Universidades","award":["TED2021-132464B-I00, RYC2021-032614-I, PID2022-142290OB-I00, CEX2024-001471-M"],"award-info":[{"award-number":["TED2021-132464B-I00, RYC2021-032614-I, PID2022-142290OB-I00, CEX2024-001471-M"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,19]]},"DOI":"10.1145\/3719027.3765148","type":"proceedings-article","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T23:33:16Z","timestamp":1763854396000},"page":"111-125","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors"],"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, Madrid, Spain and Universidad Polit\u00e9cnica de Madrid, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2425-9354","authenticated-orcid":false,"given":"Gideon","family":"Mohr","sequence":"additional","affiliation":[{"name":"Saarland University, Saarland, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3459-2214","authenticated-orcid":false,"given":"Jan","family":"Reineke","sequence":"additional","affiliation":[{"name":"Saarland University, Saarland, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5767-555X","authenticated-orcid":false,"given":"Marco","family":"Guarnieri","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,11,22]]},"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.]. Google OR-Tools. https:\/\/github.com\/google\/or-tools"},{"key":"e_1_3_2_1_3_1","unstructured":"[n.d.]. Ibex: An embedded 32 bit RISC-V CPU core. https:\/\/github.com\/lowRISC\/ibex"},{"key":"e_1_3_2_1_4_1","unstructured":"[n.d.]. Ibex RISC-V Core -- Mult.\/Divider Block. https:\/\/ibex-core.readthedocs.io\/en\/latest\/03_reference\/instruction_decode_execute.html#mult-div"},{"key":"e_1_3_2_1_5_1","unstructured":"[n.d.]. Icarus Verilog. https:\/\/github.com\/steveicarus\/iverilog"},{"key":"e_1_3_2_1_6_1","unstructured":"[n.d.]. RISC-V Formal Verification Framework. https:\/\/github.com\/SymbioticEDA\/riscv-formal"},{"key":"e_1_3_2_1_7_1","unstructured":"[n.d.]. RISC-V Sodor processor. https:\/\/github.com\/ucb-bar\/riscv-sodor"},{"key":"e_1_3_2_1_8_1","unstructured":"[n.d.]. LeaSyn implementation. https:\/\/github.com\/zilongwang123\/LeaSyn"},{"key":"e_1_3_2_1_9_1","unstructured":"[n.d.]. Yices 2 SMT Solver. https:\/\/yices.csl.sri.com"},{"key":"e_1_3_2_1_10_1","unstructured":"[n.d.]. Yosys Open SYnthesis Suite. https:\/\/github.com\/YosysHQ\/yosys"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1314466.1314469"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00066"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the 25th USENIX Security Symposium (USENIX Security). USENIX Association.","author":"Almeida Jos\u00e9 Bacelar","year":"2016","unstructured":"Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Fran\u00e7ois Dupressoir, and Michael Emmi. 2016. Verifying Constant-Time Implementations. In Proceedings of the 25th USENIX Security Symposium (USENIX Security). USENIX Association."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3658644.3670319"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560600"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363219"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the 31st ACM Conference on Computer and Communication Security (CCS). ACM.","author":"Ceesay-Seitz Katharina","year":"2024","unstructured":"Katharina Ceesay-Seitz, Flavien Solt, and Kaveh Razavi. 2024. \u03bc-CFI: Formal Verification of Microarchitectural Control-flow Integrity. In Proceedings of the 31st ACM Conference on Computer and Communication Security (CCS). ACM."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00074"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the 34th USENIX Security Symposium (USENIX Security). USENIX Association.","author":"de Faveri Tron Alvise","year":"2025","unstructured":"Alvise de Faveri Tron, Raphael Isemann, Hany Ragab, Cristiano Giuffrida, Klaus von Gleissenthall, and Herbert Bos. 2025. Phantom Trails: Practical Pre-Silicon Discovery of Transient Data Leaks. In Proceedings of the 34th USENIX Security Symposium (USENIX Security). USENIX Association."},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the 45th IEEE Symposium on Security and Privacy (S&P). IEEE.","author":"Dinesh Sushant","unstructured":"Sushant Dinesh, Madhusudan Parthasarathy, and Christopher W. Fletcher. 2024. ConjunCT: Learning Inductive Invariants to Prove Unbounded Instruction Safety Against Microarchitectural Timing Attacks. In Proceedings of the 45th IEEE Symposium on Security and Privacy (S&P). IEEE."},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM.","author":"Dinesh Sushant","unstructured":"Sushant Dinesh, Yongye Zhu, and Christopher W. Fletcher. 2025. H-Houdini: Scalable Invariant Learning. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2756550"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560555"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704867"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM.","author":"Fu Bo","year":"2025","unstructured":"Bo Fu, Leo Tenenbaum, David Adler, Assaf Klein, Arpit Gogia, Alaa R. Alameldeen, Marco Guarnieri, Mark Silberstein, Oleksii Oleksenko, and Gururaj Saileshwar. 2025. AMuLeT: Automated Design-Time Testing of Secure Speculation Counter measures. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179399"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA52012.2021.00073"},{"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.1109\/SP40001.2021.00036"},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of the 32nd USENIX Security Symposium (USENIX Security). USENIX Association.","author":"Hofmann Jana","year":"2023","unstructured":"Jana Hofmann, Emanuele Vannacci, C\u00e9dric Fournet, Boris K\u00f6pf, and Oleksii Oleksenko. 2023. Speculation at fault: modeling and testing microarchitectural leakage of CPU exceptions. In Proceedings of the 32nd USENIX Security Symposium (USENIX Security). USENIX Association."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3466752.3480087"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO61859.2024.00045"},{"key":"e_1_3_2_1_34_1","volume-title":"Proceedings of the 29th ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM.","author":"Hur Jaewon","year":"2022","unstructured":"Jaewon Hur, Suhwan Song, Sunwoo Kim, and Byoungyoung Lee. 2022. Spec-Doctor: Differential Fuzz Testing to Find Transient Execution Vulnerabilities. In Proceedings of the 29th ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM."},{"key":"e_1_3_2_1_35_1","volume-title":"Proceedings of the 41st IEEE Symposium on Security and Privacy (S&P). IEEE.","author":"Kocher P.","unstructured":"P. Kocher, J. Horn, A. Fogh, D. Genkin, D. Gruss, W. Haas, M. Hamburg, M. Lipp, S. Mangard, T. Prescher, M. Schwarz, and Y. Yarom. 2019. Spectre Attacks: Exploiting Speculative Execution. In Proceedings of the 41st IEEE Symposium on Security and Privacy (S&P). IEEE."},{"key":"e_1_3_2_1_36_1","volume-title":"Proceedings of the 36th IEEE Symposium on Security and Privacy (S&P). IEEE.","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 Proceedings of the 36th IEEE Symposium on Security and Privacy (S&P). IEEE."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243761"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE58400.2024.10546681"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_12"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507729"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179391"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484534"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579856.3590332"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1653662.1653687"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3354252"},{"key":"e_1_3_2_1_46_1","volume-title":"LazyFP: Leaking FPU Register State using Microarchitectural Side-Channels. CoRR abs\/1806.07480","author":"Stecklina Julian","year":"2018","unstructured":"Julian Stecklina and Thomas Prescher. 2018. LazyFP: Leaking FPU Register State using Microarchitectural Side-Channels. CoRR abs\/1806.07480 (2018)."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3669940.3707243"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45238-6_6"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00087"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623192"},{"key":"e_1_3_2_1_51_1","volume-title":"Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors. CoRR abs\/2509.06509","author":"Wang Zilong","year":"2025","unstructured":"Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, and Marco Guarnieri. 2025. Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors. CoRR abs\/2509.06509 (2025). http:\/\/arxiv.org\/abs\/2509.06509"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"crossref","unstructured":"Andrew Waterman Yunsup Lee David A. Patterson and Krste Asanovi\u0107. 2014. The RISC-V Instruction Set Manual Volume I: User-Level ISA Version 2.0. Technical Report UCB\/EECS-2014--54. EECS Department University of California Berkeley.","DOI":"10.21236\/ADA605735"},{"key":"e_1_3_2_1_53_1","volume-title":"Proceedings of the 30th USENIX Security Symposium (USENIX Security). USENIX Association.","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 Proceedings of the 30th USENIX Security Symposium (USENIX Security). USENIX Association."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3658644.3690319"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP54263.2024.00047"},{"key":"e_1_3_2_1_56_1","volume-title":"Proceedings of the 23rd USENIX Security Symposium (USENIX Security). USENIX Association.","author":"Yarom Yuval","year":"2014","unstructured":"Yuval Yarom and Katrina Falkner. 2014. FlushReload: A High Resolution, Low Noise, L3 Cache Side-channel Attack. In Proceedings of the 23rd USENIX Security Symposium (USENIX Security). USENIX Association."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-017-0152-y"}],"event":{"name":"CCS '25: ACM SIGSAC Conference on Computer and Communications Security","location":"Taipei Taiwan","acronym":"CCS '25","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3719027.3765148","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:18:39Z","timestamp":1766441919000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719027.3765148"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,19]]},"references-count":57,"alternative-id":["10.1145\/3719027.3765148","10.1145\/3719027"],"URL":"https:\/\/doi.org\/10.1145\/3719027.3765148","relation":{},"subject":[],"published":{"date-parts":[[2025,11,19]]},"assertion":[{"value":"2025-11-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}