{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:16:32Z","timestamp":1763968592693,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":113,"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:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Swiss State Secretariat for Education, Research and Innovation","award":["MB22.00057 (ERC-StG PROMISE)"],"award-info":[{"award-number":["MB22.00057 (ERC-StG PROMISE)"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,12,2]]},"DOI":"10.1145\/3658644.3690344","type":"proceedings-article","created":{"date-parts":[[2024,12,9]],"date-time":"2024-12-09T12:19:20Z","timestamp":1733746760000},"page":"213-227","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["\u03bcCFI: Formal Verification of Microarchitectural Control-flow Integrity"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8398-2705","authenticated-orcid":false,"given":"Katharina","family":"Ceesay-Seitz","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0872-5562","authenticated-orcid":false,"given":"Flavien","family":"Solt","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8588-7100","authenticated-orcid":false,"given":"Kaveh","family":"Razavi","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]}],"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\/1609956.1609960"},{"key":"e_1_3_2_1_2_1","volume-title":"USENIX Security","author":"Almeida Jose Bacelar","year":"2016","unstructured":"Jose Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Fran\u00e7ois Dupressoir, and Michael Emmi. [n. d.] Verifying Constant-Time Implementations. In USENIX Security 2016."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-65277-7_6"},{"key":"e_1_3_2_1_4_1","volume-title":"ACM SIGSAC","author":"Andrysco Marc","year":"2018","unstructured":"Marc Andrysco, Andres N\u00f6tzli, Fraser Brown, Ranjit Jhala, and Deian Stefan. [n. d.] Towards verified, constant-time floating point operations. In ACM SIGSAC 2018."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2017.8203772"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2017.7927266"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660283"},{"key":"e_1_3_2_1_8_1","volume-title":"ACM POPL","author":"Barthe Gilles","year":"2019","unstructured":"Gilles Barthe, Sandrine Blazy, Benjamin Gregoire, Remi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. [n. d.] Formal verification of a constanttime preserving C compiler. In ACM POPL 2019."},{"key":"e_1_3_2_1_9_1","volume-title":"ASPLOS","author":"Mohammad","year":"2022","unstructured":"Mohammad Behnia et al. 2021. Speculative interference attacks: breaking invisible speculation schemes. In ASPLOS 2022."},{"volume-title":"ACM PLDI '06","author":"Emery","key":"e_1_3_2_1_10_1","unstructured":"Emery D. Berger and Benjamin G. Zorn. [n. d.] DieHard: Probabilistic memory safety for unsafe languages. In ACM PLDI '06."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-181136"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966913.1966919"},{"key":"e_1_3_2_1_13_1","unstructured":"Pallavi Borkar Chen Chen Mohamadreza Rostami Nikhilesh Singh Rahul Kande Ahmad-Reza Sadeghi Chester Rebeiro and Jeyavijayan Rajendran. WhisperFuzz: White-box fuzzing for detecting and locating timing vulnerabilities in processors. ()."},{"key":"e_1_3_2_1_14_1","volume-title":"USENIX Security","author":"Bosamiya Jay","year":"2022","unstructured":"Jay Bosamiya, Wen Shih Lim, and Bryan Parno. [n. d.] Provably-Safe Multilingual Software Sandboxing Using Webassembly. In USENIX Security 2022."},{"volume-title":"Sat-based model checking without unrolling","author":"Bradley Aaron R.","key":"e_1_3_2_1_15_1","unstructured":"Aaron R. Bradley. 2011. Sat-based model checking without unrolling. In Springer Berlin Heidelberg."},{"key":"e_1_3_2_1_16_1","volume-title":"VLSI","author":"Bruns N.","year":"2022","unstructured":"N. Bruns, V. Herdt, D. Gro\u00dfe, and R. Drechsler. [n. d.] Efficient cross-level processor verification using coverage-guided fuzzing. In VLSI 2022."},{"key":"e_1_3_2_1_17_1","volume-title":"DATE","author":"Bruns N.","year":"2022","unstructured":"N. Bruns, V. Herdt, E. Jentzsch, and R. Drechsler. [n. d.] Cross-level processor verification via endless randomized instruction stream generation with coverage-guided aging. In DATE 2022."},{"key":"e_1_3_2_1_18_1","unstructured":"[n. d.] Cadence jasper formal property verification (fpv) app. Accessed: 2024-07--10. https:\/\/www.cadence.com\/en_US\/home\/tools\/system-design-and-verification\/formal-and-static-verification\/jasper-gold-verification-platform\/formal-property-verification-app.html."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/HOST55118.2023.10133714"},{"key":"e_1_3_2_1_20_1","volume-title":"USENIX Security","author":"Carlini Nicholas","year":"2015","unstructured":"Nicholas Carlini, Antonio Barresi, Mathias Payer, DavidWagner, and Thomas R Gross. [n. d.] Control-Flow Bending: On the Effectiveness of Control-Flow Integrity. In USENIX Security 2015."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385970"},{"volume-title":"Springer","author":"Ceesay-Seitz Katharina","key":"e_1_3_2_1_22_1","unstructured":"Katharina Ceesay-Seitz, Hamza Boukabache, and Daniel Perrin. 2020. A functional verification methodology for highly parametrizable, continuously operating safety-critical fpga designs: applied to the cern radiation monitoring electronics (crome). In Computer Safety, Reliability, and Security. Ant\u00f3nio Casimiro, Frank Ortmeier, Friedemann Bitsch, and Pedro Ferreira, (Eds.) Springer International Publishing, Cham, 67--81. isbn: 978--3-030--54549--9."},{"key":"e_1_3_2_1_23_1","volume-title":"d.] Semiformal reformulation of requirements for formal property verification. In accellera DVCON EUROPE","author":"Ceesay-Seitz Katharina","year":"2019","unstructured":"Katharina Ceesay-Seitz, Hamza Boukabache, and Daniel Perrin. [n. d.] Semiformal reformulation of requirements for formal property verification. In accellera DVCON EUROPE 2019."},{"key":"e_1_3_2_1_24_1","volume-title":"Hamza Boukabache, and Daniel Perrin. [n. d.] Formal property verification of the digital section of an ultra-low current digitizer asic. In accellera DVCON EUROPE","author":"Ceesay-Seitz Katharina","year":"2021","unstructured":"Katharina Ceesay-Seitz, Sarath Kundumattathil Mohanan, Hamza Boukabache, and Daniel Perrin. [n. d.] Formal property verification of the digital section of an ultra-low current digitizer asic. In accellera DVCON EUROPE 2021."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Katharina Ceesay-Seitz Flavien Solt and Kaveh Razavi. 2024. 'CFI: formal verification of microarchitectural control-flow integrity. In Extended version of this paper. https:\/\/comsec.ethz.ch\/wp-content\/files\/mucfi_ccs24.pdf.","DOI":"10.1145\/3658644.3690344"},{"key":"e_1_3_2_1_26_1","unstructured":"C. Chen R. Kande N. Nyugen F. Andersen A. Tyagi A. R. Sadeghi and J. Rajendran. HyPFuzz: Formal-assisted processor fuzzing. ()."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377813.3381347"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--319--10575--8"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891830"},{"key":"e_1_3_2_1_30_1","volume-title":"d.] KCoFI: Complete control-flow integrity for commodity operating system kernels","author":"Criswell John","year":"2014","unstructured":"John Criswell, Nathan Dautenhahn, and Vikram Adve. [n. d.] KCoFI: Complete control-flow integrity for commodity operating system kernels. In IEEE S&P 2014."},{"key":"e_1_3_2_1_31_1","volume-title":"d.] Binsec\/rel: Efficient relational symbolic execution for constant-time at binary-level","author":"Daniel Lesly-Ann","year":"2020","unstructured":"Lesly-Ann Daniel, S\u00e9bastien Bardin, and Tamara Rezk. [n. d.] Binsec\/rel: Efficient relational symbolic execution for constant-time at binary-level. In IEEE S&P 2020."},{"key":"e_1_3_2_1_32_1","volume-title":"ACM ASHES","author":"Deutschbein Calvin","year":"2021","unstructured":"Calvin Deutschbein, Andres Meza, Francesco Restuccia, Ryan Kastner, and Cynthia Sturton. [n. d.] Isadora: Automated information flow property generation for hardware designs. In ACM ASHES 2021."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2024.3374249"},{"key":"e_1_3_2_1_34_1","volume-title":"ACM\/IEEE DAC","author":"Deutschmann Lucas","year":"2022","unstructured":"Lucas Deutschmann, Johannes M\u00fcller, Mohammad R. Fadiheh, Dominik Stoffel, and Wolfgang Kunz. [n. d.] Towards a formally verified hardware root-oftrust for data-oblivious computing. In ACM\/IEEE DAC 2022."},{"key":"e_1_3_2_1_35_1","volume-title":"[n. d.]","author":"Dinesh S.","year":"2024","unstructured":"S. Dinesh, M. Parthasarathy, and C. Fletcher. [n. d.] ConjunCT: Learning inductive invariants to prove unbounded instruction safety against microarchitectural timing attacks. In IEEE S&P 2024."},{"key":"e_1_3_2_1_36_1","volume-title":"FMCAD","author":"Dong Ning","year":"2023","unstructured":"Ning Dong, Roberto Guanciale, Mads Dam, and Andreas L\u00f6\u00f6w. [n. d.] Formal verification of correctness and information flow security for an in-order pipelined processor. In FMCAD 2023."},{"key":"e_1_3_2_1_37_1","volume-title":"USENIX Security","author":"Du Yufei","year":"2022","unstructured":"Yufei Du, Zhuojia Shen, Komail Dharsee, Jie Zhou, Robert J Walls, and John Criswell. [n. d.] Holistic control-flow protection on real-time embedded systems with kage. In USENIX Security 2022."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","unstructured":"Limor Fix. 2008. Fifteen Years of Formal Property Verification in Intel. In 25 Years of Model Checking: History Achievements Perspectives. Orna Grumberg and Helmut Veith (Eds.) Springer Berlin Heidelberg 139--144. https:\/\/doi.org\/10.1007\/978--3--540--69850-0_8.","DOI":"10.1007\/978--3--540--69850-0_8"},{"key":"e_1_3_2_1_39_1","volume-title":"d.] A security RISC: Microarchitectural attacks on hardware RISC-v cpus","author":"Gerlach Lukas","year":"2023","unstructured":"Lukas Gerlach, Daniel Weber, Ruiyi Zhang, and Michael Schwarz. [n. d.] A security RISC: Microarchitectural attacks on hardware RISC-v cpus. In IEEE S&P 2023."},{"key":"e_1_3_2_1_40_1","volume-title":"Deian Stefan, and Ranjit Jhala. [n. d.] IODINE: Verifying Constant-Time Execution of Hardware. In USENIX Security","author":"Gleissenthall Klaus","year":"2019","unstructured":"Klaus v Gleissenthall, Rami G\u00f6khan Kici, Deian Stefan, and Ranjit Jhala. [n. d.] IODINE: Verifying Constant-Time Execution of Hardware. In USENIX Security 2019."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20652-9_11"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2017.23271"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00036"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-09484-2_7"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Karine Heydemann Jean-Fran\u00e7ois Lalande and Pascal Berthome. 2019. Formally verified software countermeasures for control-flow integrity of smart card C code. Computers & Security 85.","DOI":"10.1016\/j.cose.2019.05.004"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3447867"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ATS49688.2020.9301533"},{"key":"e_1_3_2_1_48_1","volume-title":"[n. d.] Difuzzrtl: Differential fuzz testing to find cpu bugs","author":"Hur J.","year":"2021","unstructured":"J. Hur, S. Song, D. Kwon, E. Baek, J. Kim, and B. Lee. [n. d.] Difuzzrtl: Differential fuzz testing to find cpu bugs. In IEEE S&P 2021."},{"key":"e_1_3_2_1_49_1","unstructured":"[n. d.] Ibex CPU. Accessed: 2024-04--16. https:\/\/github.com\/lowRISC\/opentitan."},{"key":"e_1_3_2_1_50_1","unstructured":"[n. d.] Ibex documentation - verification stages. Accessed: 2024-04--16. https:\/\/ibex-core.readthedocs.io\/en\/latest\/03_reference\/verification_stages.html."},{"volume-title":"IEEE standard for SystemVerilog--unified hardware design, specification, and verification language","year":"1800","key":"e_1_3_2_1_51_1","unstructured":"2018. IEEE standard for SystemVerilog--unified hardware design, specification, and verification language. IEEE Std 1800--2017 (Revision of IEEE Std 1800--2012)."},{"key":"e_1_3_2_1_52_1","unstructured":"Intel Corporation. [n. d.] Data Operand Independent Timing ISA Guidance. [Updated 13-February-2023]. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/software-security-guidance\/best-practices\/data-operand-independent-timing-isa-guidance.html."},{"key":"e_1_3_2_1_53_1","volume-title":"Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, and Yasemin Acar. [n. d.] 'They're not that hard to mitigate': What cryptographic library developers think about timing attacks","author":"Jancar Jan","year":"2022","unstructured":"Jan Jancar, Marcel Fourne, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, and Yasemin Acar. [n. d.] 'They're not that hard to mitigate': What cryptographic library developers think about timing attacks. In IEEE S&P 2022."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3466752.3480092"},{"key":"e_1_3_2_1_55_1","volume-title":"USENIX Security","author":"Kande R.","year":"2022","unstructured":"R. Kande, A. Crump, G. Persyn, P. Jauernig, A. R. Sadeghi, A. Tyagi, and J. Rajendran. [n. d.] TheHuzz: Instruction Fuzzing of Processors Using Golden-Reference Models for Finding Software-Exploitable Vulnerabilities. In USENIX Security 2022."},{"key":"e_1_3_2_1_56_1","volume-title":"[n. d.] Spectre attacks: Exploiting speculative execution","author":"Paul Kocher","year":"2019","unstructured":"Paul Kocher et al. [n. d.] Spectre attacks: Exploiting speculative execution. In IEEE S&P 2019."},{"key":"e_1_3_2_1_57_1","unstructured":"[n. d.] Kronos RISC-v (all cascade fixes integrated). Accessed: 2024-07--10. https:\/\/github.com\/cascade-artifacts-designs\/cascade-kronos."},{"key":"e_1_3_2_1_58_1","volume-title":"d.] NetCAT: Practical cache attacks from the network","author":"Kurth Michael","year":"2020","unstructured":"Michael Kurth, Ben Gras, Dennis Andriesse, Cristiano Giuffrida, Herbert Bos, and Kaveh Razavi. [n. d.] NetCAT: Practical cache attacks from the network. In IEEE S&P 2020."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240842"},{"key":"e_1_3_2_1_60_1","volume-title":"USENIX Security","author":"Moritz Lipp","year":"2018","unstructured":"Moritz Lipp et al. [n. d.] Meltdown: Reading kernel memory from user space. In USENIX Security 2018."},{"key":"e_1_3_2_1_61_1","volume-title":"Memory Trace Oblivious Program Execution. In IEEE CSF","author":"Liu Chang","year":"2013","unstructured":"Chang Liu, Michael Hicks, and Elaine Shi. [n. d.] Memory Trace Oblivious Program Execution. In IEEE CSF 2013."},{"volume-title":"Benchmarking tools for verification of constant-time execution. SBSEG. Bento Goncalves","author":"Lopes Arthur Costa","key":"e_1_3_2_1_62_1","unstructured":"Arthur Costa Lopes and Diego F Aranha. 2017. Benchmarking tools for verification of constant-time execution. SBSEG. Bento Goncalves, Brazil: SBC."},{"key":"e_1_3_2_1_63_1","unstructured":"lowRISC contributors. [n. d.] OpenTitan root of trust. Accessed: 2024-07--10. https:\/\/opentitan.org\/."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP51992.2021.00048"},{"key":"e_1_3_2_1_65_1","volume-title":"ACM SIGSAC","author":"Mashtizadeh Ali Jose","year":"2015","unstructured":"Ali Jose Mashtizadeh, Andrea Bittau, Dan Boneh, and David Mazieres. [n. d.] CCFI: Cryptographically enforced control flow integrity. In ACM SIGSAC 2015."},{"key":"e_1_3_2_1_66_1","volume-title":"CAV","author":"McMillan K. L.","year":"2003","unstructured":"K. L. McMillan. [n. d.] Interpolation and sat-based model checking. In CAV 2003."},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10766-018-0611-9"},{"key":"e_1_3_2_1_68_1","volume-title":"USENIX Security","author":"Moghimi Daniel","year":"2023","unstructured":"Daniel Moghimi. [n. d.] Downfall: Exploiting speculative data gathering. In USENIX Security 2023."},{"key":"e_1_3_2_1_69_1","volume-title":"USENIX Security","author":"Molnar David","year":"2005","unstructured":"David Molnar, Matt Piotrowski, David Schultz, and David Wagner. [n. d.] The program counter security model: Automatic detection and removal of control-flow side channel attacks. In USENIX Security 2005."},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3470496.3527412"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2331332"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507729"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18074.2021.9586118"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3613424.3614254"},{"key":"e_1_3_2_1_75_1","unstructured":"[n. d.] PicoRV32 - a size-optimized RISC-v CPU. Accessed: 2024-07--10. https:\/\/github.com\/YosysHQ\/picorv32."},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2012.152"},{"key":"e_1_3_2_1_77_1","volume-title":"d.] Dejitleak: eliminating jit-induced timing side-channel leaks. In (ACM ESEC\/FSE","author":"Qin Qi","year":"2022","unstructured":"Qi Qin, JulianAndres JiYang, Fu Song, Taolue Chen, and Xinyu Xing. [n. d.] Dejitleak: eliminating jit-induced timing side-channel leaks. In (ACM ESEC\/FSE 2022)."},{"key":"e_1_3_2_1_78_1","volume-title":"d.] Crosstalk: Speculative data leaks across cores are real","author":"Ragab Hany","year":"2021","unstructured":"Hany Ragab, Alyssa Milburn, Kaveh Razavi, Herbert Bos, and Cristiano Giuffrida. [n. d.] Crosstalk: Speculative data leaks across cores are real. In IEEE S&P 2021."},{"key":"e_1_3_2_1_79_1","volume-title":"CAV","author":"Alastair","year":"2016","unstructured":"Alastair Reid et al. [n. d.] End-to-end verification of processors with ISAformal. In CAV 2016."},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.46586\/tches.v2022.i4.255--284"},{"key":"e_1_3_2_1_81_1","volume-title":"RISC-v cryptography extension. [Online","author":"RISC-V.","year":"2023","unstructured":"RISC-V. 2024. RISC-v cryptography extension. [Online; accessed 1-December-2023]. https:\/\/github.com\/riscv\/riscv-crypto."},{"volume-title":"RV '2009","author":"Rosu Grigore","key":"e_1_3_2_1_82_1","unstructured":"Grigore Rosu, Wolfram Schulte, and Traian Florin Serbanuta. [n. d.] Runtime verification of C memory safety. In RV '2009. Springer."},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.3390\/app9204229"},{"key":"e_1_3_2_1_84_1","unstructured":"[n. d.] SCARV: processor core implementation. Accessed: 2024-07--10. https:\/\/github.com\/scarv\/scarv-cpu."},{"key":"e_1_3_2_1_85_1","volume-title":"Kiran Kumar","author":"Seligman Erik","year":"2023","unstructured":"Erik Seligman, Tom Schubert, and Achutha M. V. Kiran Kumar. 2023. Formal Verification. An Essential Toolkit for Modern VLSI Design. (2nd ed.). Elsvier Science & Technology.","edition":"2"},{"key":"e_1_3_2_1_86_1","unstructured":"Siemens AG. [n. d.] The 2022 Wilson Research Group Functional Verification Study. Accessed: 2024--4--28. https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2022\/12\/12\/part-8-the-2022-wilson-research-group-functional-verification-study\/."},{"key":"e_1_3_2_1_87_1","volume-title":"USENIX Security","author":"Solt Flavien","year":"2024","unstructured":"Flavien Solt, Katharina Ceesay-Seitz, and Kaveh Razavi. [n. d.] Cascade: CPU Fuzzing via Intricate Program Generation. In USENIX Security 2024."},{"key":"e_1_3_2_1_88_1","volume-title":"USENIX Security","author":"Solt Flavien","year":"2022","unstructured":"Flavien Solt, Ben Gras, and Kaveh Razavi. [n. d.] CellIFT: Leveraging Cells for Scalable and Precise Dynamic Information Flow Tracking in RTL. In USENIX Security 2022."},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO56248.2022.00081"},{"key":"e_1_3_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676536.3676658"},{"key":"e_1_3_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/1037187.1024404"},{"key":"e_1_3_2_1_92_1","volume-title":"USENIX Security","author":"Tice Caroline","year":"2014","unstructured":"Caroline Tice, Tom Roeder, Peter Collingbourne, Stephen Checkoway, Ulfar Erlingsson, Luis Lozano, and Geoff Pike. [n. d.] Enforcing forward-edge control-flow integrity in GCC & LLVM. In USENIX Security 2014."},{"key":"e_1_3_2_1_93_1","volume-title":"ASPLOS","author":"Tiwari Mohit","year":"2019","unstructured":"Mohit Tiwari, Hassan MGWassel, Bita Mazloom, Shashidhar Mysore, Frederic T Chong, and Timothy Sherwood. [n. d.] Complete information flow tracking from the gates up. In ASPLOS 2019."},{"key":"e_1_3_2_1_94_1","volume-title":"USENIX Security","author":"Trippel T.","year":"2022","unstructured":"T. Trippel, K. G. Shin, A. Chernyakhovsky, G. Kelly, D. Rizzo, and M. Hicks. [n. d.] Fuzzing Hardware Like Software. In USENIX Security 2022."},{"key":"e_1_3_2_1_95_1","volume-title":"USENIX Security","author":"Trujillo Dani\u00ebl","year":"2023","unstructured":"Dani\u00ebl Trujillo, Johannes Wikner, and Kaveh Razavi. [n. d.] INCEPTION: Exposing New Attack Surfaces with Training in Transient Execution. In USENIX Security 2023."},{"key":"e_1_3_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484810"},{"key":"e_1_3_2_1_97_1","volume-title":"d.] RIDL: Rogue in-flight data load","author":"Schaik Stephan Van","year":"2019","unstructured":"Stephan Van Schaik, Alyssa Milburn, Sebastian \u00d6sterlund, Pietro Frigo, Giorgi Maisuradze, Kaveh Razavi, Herbert Bos, and Cristiano Giuffrida. [n. d.] RIDL: Rogue in-flight data load. In IEEE S&P 2019."},{"key":"e_1_3_2_1_98_1","volume-title":"d.] Augury: Using data memory-dependent prefetchers to leak data at rest","author":"Sanchez Vicarte Jose Rodrigo","year":"2022","unstructured":"Jose Rodrigo Sanchez Vicarte, Michael Flanders, Riccardo Paccagnella, Grant Garrett-Grossman, Adam Morrison, Christopher W. Fletcher, and David Kohlbrenner. [n. d.] Augury: Using data memory-dependent prefetchers to leak data at rest. In IEEE S&P 2022."},{"key":"e_1_3_2_1_99_1","volume-title":"ACM SIGSAC","author":"Huibo","year":"2019","unstructured":"Huibo Wang et al. [n. d.] Towards memory safe enclave programming with rust-sgx. In ACM SIGSAC 2019."},{"key":"e_1_3_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623192"},{"key":"e_1_3_2_1_101_1","volume-title":"d.] Memory Security in Reconfigurable Computers: Combining Formal Verification with Monitoring","author":"Wiersema Tobias","year":"2014","unstructured":"Tobias Wiersema, Stephanie Drzevitzky, and Marco Platzner. [n. d.] Memory Security in Reconfigurable Computers: Combining Formal Verification with Monitoring. In IEEE FPT 2014."},{"key":"e_1_3_2_1_102_1","volume-title":"Spring: Spectre Returning in the Browser with Speculative Load Queuing and Deep Stacks. In WOOT","author":"Wikner Johannes","year":"2022","unstructured":"Johannes Wikner, Cristiano Giuffrida, Herbert Bos, and Kaveh Razavi. [n. d.] Spring: Spectre Returning in the Browser with Speculative Load Queuing and Deep Stacks. In WOOT 2022."},{"key":"e_1_3_2_1_103_1","volume-title":"USENIX Security","author":"Wikner Johannes","year":"2022","unstructured":"Johannes Wikner and Kaveh Razavi. [n. d.] RETBLEED: Arbitrary Speculative Code Execution with Return Instructions. In USENIX Security 2022."},{"key":"e_1_3_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1145\/3613424.3614275"},{"key":"e_1_3_2_1_105_1","volume-title":"Austrochip","author":"Glaser Johann","year":"2013","unstructured":"CliffordWolf, Johann Glaser, and Johannes Kepler. [n. d.] Yosys-a free Verilog synthesis suite. In Austrochip 2013."},{"key":"e_1_3_2_1_106_1","volume-title":"USENIX Security","author":"Xu Xiaoyang","year":"2019","unstructured":"Xiaoyang Xu, Masoud Ghaffarinia, Wenhao Wang, Kevin W Hamlen, and Zhiqiang Lin. [n. d.] Confirm: Evaluating Compatibility and Relevance of Control-Flow Integrity Protections for Modern Software. In USENIX Security 2019."},{"key":"e_1_3_2_1_107_1","volume-title":"USENIX Security","author":"Yoo Sungbae","year":"2022","unstructured":"Sungbae Yoo, Jinbum Park, Seolheui Kim, Yeji Kim, and Taesoo Kim. [n. d.] In-Kernel Control-Flow Integrity on Commodity OSes using ARM Pointer Authentication. In USENIX Security 2022."},{"key":"e_1_3_2_1_108_1","unstructured":"Yosys Open SYnthesis Suite. [n. d.] RISC-V Formal Verification Framework. Accessed: 2024-07--10. https:\/\/github.com\/YosysHQ\/riscv-formal."},{"key":"e_1_3_2_1_109_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579371.3589100"},{"key":"e_1_3_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046713"},{"key":"e_1_3_2_1_111_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE54114.2022.9774527"},{"key":"e_1_3_2_1_112_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD57027.2022.00067"},{"key":"e_1_3_2_1_113_1","doi-asserted-by":"publisher","unstructured":"Qizhi Zhang Jiaji He Yiqiang Zhao and Xiaolong Guo. 2020. A formal framework for gate-level information leakage using z3. In AsianHOST 1--6. doi: 10.1109\/AsianHOST51057.2020.9358257.","DOI":"10.1109\/AsianHOST51057.2020.9358257"}],"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.3690344","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3658644.3690344","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T06:09:47Z","timestamp":1755842987000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3658644.3690344"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,2]]},"references-count":113,"alternative-id":["10.1145\/3658644.3690344","10.1145\/3658644"],"URL":"https:\/\/doi.org\/10.1145\/3658644.3690344","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"}}]}}