{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T15:30:18Z","timestamp":1773588618365,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":58,"publisher":"ACM","funder":[{"name":"NSF (National Science Foundation)","award":["CCF 2422052"],"award-info":[{"award-number":["CCF 2422052"]}]},{"name":"NSF (National Science Foundation)","award":["CCF 2422053"],"award-info":[{"award-number":["CCF 2422053"]}]},{"name":"NSF (National Science Foundation)","award":["CNS 2046359"],"award-info":[{"award-number":["CNS 2046359"]}]},{"name":"JUMP 2.0, a Semiconductor Research Corporation (SRC) program","award":["ACE Center"],"award-info":[{"award-number":["ACE Center"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,3,22]]},"DOI":"10.1145\/3779212.3790144","type":"proceedings-article","created":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T13:55:26Z","timestamp":1773150926000},"page":"442-458","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Compass: Navigating the Design Space of Taint Schemes for RTL Security Verification"],"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, Massachusett, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2475-3675","authenticated-orcid":false,"given":"Qinhan","family":"Tan","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, New Jersey, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8468-8409","authenticated-orcid":false,"given":"Thomas","family":"Bourgeat","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne, Lausanne, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0837-5443","authenticated-orcid":false,"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, New Jersey, 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, Massachusett, USA"}]}],"member":"320","published-online":{"date-parts":[[2026,3,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2017.7927266"},{"key":"e_1_3_2_1_2_1","unstructured":"Krste Asanovi? Rimas Avizienis Jonathan Bachrach Scott Beamer David Biancolin Christopher Celio Henry Cook Daniel Dabbelt John Hauser Adam Izraelevitz Sagar Karandikar Ben Keller Donggyu Kim John Koenig Yunsup Lee Eric Love Martin Maas Albert Magyar Howard Mao Miquel Moreto Albert Ou David A. Patterson Brian Richards Colin Schmidt Stephen Twigg Huy Vo and Andrew Waterman. 2016. The Rocket Chip Generator. Technical Report UCB\/EECS-2016-17. EECS Department University of California Berkeley. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2016\/EECS-2016-17.html"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228584"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00046"},{"key":"e_1_3_2_1_5_1","volume-title":"Secure information flow by self-composition. Mathematical Structures in Computer Science","author":"Barthe Gilles","year":"2011","unstructured":"Gilles Barthe, Pedro R D'argenio, and Tamara Rezk. 2011. Secure information flow by self-composition. Mathematical Structures in Computer Science (2011)."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3061639.3062203"},{"key":"e_1_3_2_1_7_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 Proceedings of the 6th International Conference on Computer Aided Verification. Springer-Verlag."},{"key":"e_1_3_2_1_8_1","first-page":"06","volume":"2","unstructured":"Cadence. [Accessed 23-06-2024]. Jasper Security Path Verification App. https:\/\/www.cadence.com\/en_US\/home\/tools\/system-design-and-verification\/formal-and-static-verification\/jasper-gold-verification-platform\/security-path-verification-app.html.","journal-title":"Accessed"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3643772"},{"key":"e_1_3_2_1_10_1","first-page":"09","volume":"1","author":"Celio Christopher","unstructured":"Christopher Celio and Et al. 2024. riscv-sodor Github Repository. https:\/\/github.com\/ucb-bar\/riscv-sodor. [Accessed 17-09-2024].","journal-title":"Accessed"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_3_2_1_12_1","volume-title":"Journal of Computer Security","author":"Clarkson Michael R","year":"2010","unstructured":"Michael R Clarkson and Fred B Schneider. 2010. Hyperproperties. Journal of Computer Security (2010)."},{"key":"e_1_3_2_1_13_1","volume-title":"ProSpeCT: Provably Secure Speculation for the Constant-Time Policy. In 32nd USENIX Security Symposium.","author":"Daniel Lesly-Ann","year":"2023","unstructured":"Lesly-Ann Daniel, Marton Bognar, Job Noorman, S\u00e9bastien Bardin, Tamara Rezk, and Frank Piessens. 2023. ProSpeCT: Provably Secure Speculation for the Constant-Time Policy. In 32nd USENIX Security Symposium."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3474376.3487286"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3669940.3707263"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18072.2020.9218572"},{"key":"e_1_3_2_1_17_1","volume-title":"An exhaustive approach to detecting transient execution side channels in RTL designs of processors","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. (2022)."},{"key":"e_1_3_2_1_18_1","first-page":"12","volume":"1","author":"Gonzalez Abraham","unstructured":"Abraham Gonzalez and Et al. 2025. Chipyard Github Repository on tag 1.11.0. https:\/\/github.com\/ucb-bar\/chipyard\/releases\/tag\/1.11.0. [Accessed 16-12-2025].","journal-title":"Accessed"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00036"},{"key":"e_1_3_2_1_20_1","volume-title":"2024 57th Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO).","author":"Hsiao Yao","year":"2024","unstructured":"Yao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P Mulligan, Gustavo Petri, Christopher W Fletcher, and Caroline Trippel. 2024. RTL2M\u03bcPATH: Multi-\u03bcPATH Synthesis with Applications to Hardware Security Verification. In 2024 57th Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO)."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240839"},{"key":"e_1_3_2_1_22_1","volume-title":"Hardware information flow tracking. ACM Computing Surveys (CSUR)","author":"Hu Wei","year":"2021","unstructured":"Wei Hu, Armaiti Ardeshiricham, and Ryan Kastner. 2021. Hardware information flow tracking. ACM Computing Surveys (CSUR) (2021)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2966986.2967046"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2011.2120970"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2012.2189105"},{"key":"e_1_3_2_1_26_1","unstructured":"Intel. 2018. Intel Side Channel Vulnerability L1TF. https:\/\/www.intel.com\/content\/www\/us\/en\/architecture-and-technology\/l1tf.html. [Accessed 23-06-2024]."},{"key":"e_1_3_2_1_27_1","unstructured":"Intel. 2023. Indirect Branch Predictor Barrier. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/software-security-guidance\/technical-documentation\/indirect-branch-predictor-barrier.html. [Accessed 14-11-2024]."},{"key":"e_1_3_2_1_28_1","unstructured":"RISC-V International. 2025. Benchmarks for RISCV Processor. https:\/\/github.com\/riscv-software-src\/riscv-tests\/tree\/master\/benchmarks. [Accessed 16-08-2025]."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2017.8203780"},{"key":"e_1_3_2_1_30_1","volume-title":"Secure-by-Construction Design Methodology for CPUs: Implementing Secure Speculation on the RTL. In 2023 IEEE\/ACM International Conference on Computer Aided Design (ICCAD). IEEE.","author":"Jauch Tobias","year":"2023","unstructured":"Tobias Jauch, Alex Wezel, Mohammad R Fadiheh, Philipp Schmitz, Sayak Ray, Jason M Fung, Christopher W Fletcher, Dominik Stoffel, and Wolfgang Kunz. 2023. Secure-by-Construction Design Methodology for CPUs: Implementing Secure Speculation on the RTL. In 2023 IEEE\/ACM International Conference on Computer Aided Design (ICCAD). IEEE."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","unstructured":"Shuvendu Lahiri and Randal Bryant. 2003. Deductive Verification of Advanced Out-of-Order Microprocessors. In Computer Aided Verification. https:\/\/doi.org\/10.1007\/978-3-540-45069-6_33","DOI":"10.1007\/978-3-540-45069-6_33"},{"key":"e_1_3_2_1_33_1","volume-title":"Indirector:High-Precision Branch Target Injection Attacks Exploiting the Indirect Branch Predictor. In 33rd USENIX Security Symposium.","author":"Li Luyi","year":"2024","unstructured":"Luyi Li, Hosein Yavarzadeh, and Dean Tullsen. 2024. Indirector:High-Precision Branch Target Injection Attacks Exploiting the Indirect Branch Predictor. In 33rd USENIX Security Symposium."},{"key":"e_1_3_2_1_34_1","volume-title":"27th USENIX Security Symposium. USENIX Association.","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 Association."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-98668-0_13"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_1_37_1","unstructured":"Amruth Pillai. 2025. RSA Algorithm in C. https:\/\/gist.github.com\/AmruthPillai\/42f4fef15bd2591aeddccae03b31ab25. [Accessed 16-08-2025]."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_3"},{"key":"e_1_3_2_1_39_1","volume-title":"CellIFT: Leveraging Cells for Scalable and Precise Dynamic Information Flow Tracking in RTL. In 31st USENIX Security Symposium.","author":"Solt Flavien","year":"2022","unstructured":"Flavien Solt, Ben Gras, and Kaveh Razavi. 2022. CellIFT: Leveraging Cells for Scalable and Precise Dynamic Information Flow Tracking in RTL. In 31st USENIX Security Symposium."},{"key":"e_1_3_2_1_40_1","volume-title":"HybriDIFT: Scalable Memory-Aware Dynamic Information Flow Tracking for Hardware. In IEEE\/ACM International Conference on Computer-Aided Design (ICCAD).","author":"Solt Flavien","year":"2024","unstructured":"Flavien Solt and Kaveh Razavi. 2024. HybriDIFT: Scalable Memory-Aware Dynamic Information Flow Tracking for Hardware. In IEEE\/ACM International Conference on Computer-Aided Design (ICCAD)."},{"key":"e_1_3_2_1_41_1","first-page":"08","volume":"1","author":"Spinal Hardware Description Language HDL.","unstructured":"SpinalHDL. 2025. Spinal Hardware Description Language. https:\/\/spinalhdl.github.io\/SpinalDoc-RTD\/master\/index.html. [Accessed 16-08-2025].","journal-title":"Accessed"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1024393.1024404"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3616643"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3669940.3707243"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1669112.1669174"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508258"},{"key":"e_1_3_2_1_47_1","volume-title":"IODINE: Verifying Constant-Time Execution of Hardware. In 28th USENIX Security Symposium.","author":"v. Gleissenthall Klaus","year":"2019","unstructured":"Klaus v. Gleissenthall, Rami G\u00f6khan Kici, Deian Stefan, and Ranjit Jhala. 2019. IODINE: Verifying Constant-Time Execution of Hardware. In 28th USENIX Security Symposium."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484810"},{"key":"e_1_3_2_1_49_1","first-page":"08","volume":"0","unstructured":"Veripool. [Accessed 08-08-2028]. Verilator, the fastest Verilog\/SystemVerilog simulator. https:\/\/veripool.org\/verilator\/.","journal-title":"Accessed"},{"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","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623192"},{"key":"e_1_3_2_1_52_1","unstructured":"XiangShan. 2025. The Abstract Machine (AM). https:\/\/github.com\/OpenXiangShan\/nexus-am\/tree\/master\/tests\/cputest. [Accessed 16-08-2025]."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_11"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358274"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623074"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694372"},{"key":"e_1_3_2_1_57_1","volume-title":"SonicBOOM: The 3rd Generation Berkeley Out-of-Order Machine. In Fourth Workshop on Computer Architecture Research with RISC-V.","author":"Zhao Jerry","year":"2020","unstructured":"Jerry Zhao, Ben Korpan, Abraham Gonzalez, and Krste Asanovic. 2020. SonicBOOM: The 3rd Generation Berkeley Out-of-Order Machine. In Fourth Workshop on Computer Architecture Research with RISC-V."},{"key":"e_1_3_2_1_58_1","volume-title":"Sound and Efficient Static Analysis for Constant-Time Programming. In 38th European Conference on Object-Oriented Programming (ECOOP","author":"Zhou Quan","year":"2024","unstructured":"Quan Zhou, Sixuan Dang, and Danfeng Zhang. 2024. CtChecker: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming. In 38th European Conference on Object-Oriented Programming (ECOOP 2024)."}],"event":{"name":"ASPLOS '26: 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Pittsburgh PA USA","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","SIGPLAN ACM Special Interest Group on Programming Languages","SIGARCH ACM Special Interest Group on Computer Architecture","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2"],"original-title":[],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T13:57:43Z","timestamp":1773583063000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779212.3790144"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,22]]},"references-count":58,"alternative-id":["10.1145\/3779212.3790144","10.1145\/3779212"],"URL":"https:\/\/doi.org\/10.1145\/3779212.3790144","relation":{},"subject":[],"published":{"date-parts":[[2026,3,22]]},"assertion":[{"value":"2026-03-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}