{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T15:11:27Z","timestamp":1778080287788,"version":"3.51.4"},"publisher-location":"Singapore","reference-count":90,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819586165","type":"print"},{"value":"9789819586172","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-8617-2_4","type":"book-chapter","created":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T14:21:13Z","timestamp":1778077273000},"page":"89-112","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Foundations of\u00a0Hardware-Software Leakage Contracts"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3459-2214","authenticated-orcid":false,"given":"Jan","family":"Reineke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,1]]},"reference":[{"key":"4_CR1","unstructured":"CVA6: A 6-stage RISC-V CPU core capable of booting linux. https:\/\/github.com\/openhwgroup\/cva6"},{"key":"4_CR2","unstructured":"DarkRISCV processor. https:\/\/github.com\/darklife\/darkriscv"},{"key":"4_CR3","unstructured":"Ibex: An embedded 32 bit RISC-V CPU core. https:\/\/github.com\/lowRISC\/ibex"},{"key":"4_CR4","unstructured":"RISC-V Sodor processor. https:\/\/github.com\/ucb-bar\/riscv-sodor"},{"key":"4_CR5","unstructured":"RISC-V ISA manual, Zkt extension (2024). https:\/\/riscv-software-src.github.io\/riscv-unified-db\/manual\/html\/isa\/isa_20240411\/exts\/Zkt.html. Accessed 1 Jan 2026"},{"key":"4_CR6","unstructured":"RISC-V ISA manual, Zkvt extension (2024). https:\/\/riscv-software-src.github.io\/riscv-unified-db\/manual\/html\/isa\/isa_20240411\/exts\/Zvkt.html. Accessed 1 Jan 2026"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Acii\u00e7mez, O.: Yet another microarchitectural attack: exploiting I-cache. In: Proceedings of the 2007 ACM Workshop on Computer Security Architecture. CSAW, ACM (2007)","DOI":"10.1145\/1314466.1314469"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Acii\u00e7mez, O., Ko\u00e7, \u00c7.K.: Trace-driven cache attacks on AES. In: International Conference on Information and Communications Security (2006)","DOI":"10.1007\/11935308_9"},{"key":"4_CR9","unstructured":"Advanced Micro Devices, Inc.: AMD64 Architecture Programmer\u2019s Manual (2025). https:\/\/www.amd.com\/en\/support\/tech-docs\/amd64-architecture-programmers-manual"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Aldaya, A.C., Brumley, B.B., ul\u00a0Hassan, S., Garc\u00eda, C.P., Tuveri, N.: Port contention for fun and profit. In: Proceedings of the 40th IEEE Symposium on Security and Privacy. S&P, IEEE (2019)","DOI":"10.1109\/SP.2019.00066"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"AlFardan, N.J., Paterson, K.G.: Lucky thirteen: breaking the TLS and DTLS record protocols. In: 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, 19\u201322 May 2013, pp. 526\u2013540. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/SP.2013.42","DOI":"10.1109\/SP.2013.42"},{"key":"4_CR12","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Dupressoir, F., Emmi, M.: Verifying constant-time implementations. In: Proceedings of the 25th USENIX Security Symposium. USENIX Security, USENIX Association (2016)"},{"key":"4_CR13","unstructured":"Arm: How is instruction timing affected by the FEAT_DIT architectural feature? (2020). https:\/\/developer.arm.com\/documentation\/ka005181\/latest. Accessed 1 Jan 2026"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Armstrong, A., et al.: ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS. Proc. ACM Program. Lang. 3(POPL), 71:1\u201371:31 (2019). https:\/\/doi.org\/10.1145\/3290384","DOI":"10.1145\/3290384"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Arranz-Olmos, S., Barthe, G., Blatter, L., Gr\u00e9goire, B., Laporte, V.: Preservation of speculative constant-time by compilation. Proc. ACM Program. Lang. 9(POPL), 1293\u20131325 (2025). https:\/\/doi.org\/10.1145\/3704880","DOI":"10.1145\/3704880"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Arranz-Olmos, S., et al.: Let\u2019s DOIT: using Intel\u2019s extended HW\/SW contract for secure compilation of crypto code. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2025(3), 644\u2013667 (2025). https:\/\/doi.org\/10.46586\/tches.v2025.i3.644-667. https:\/\/artifacts.iacr.org\/tches\/2025\/a28","DOI":"10.46586\/tches.v2025.i3.644-667"},{"key":"4_CR17","unstructured":"Asanovi\u0107, K., et al.: The rocket chip generator. Technical Report UCB\/EECS-2016-17, EECS Department, University of California, Berkeley (2016). http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2016\/EECS-2016-17.html"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Barthe, G., et al.: Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371075","DOI":"10.1145\/3371075"},{"issue":"6","key":"4_CR19","doi-asserted-by":"publisher","first-page":"1207","DOI":"10.1017\/S0960129511000193","volume":"21","author":"G Barthe","year":"2011","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6), 1207\u20131252 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gr\u00e9goire, B., Laporte, V.: Secure compilation of side-channel countermeasures: the case of cryptographic \u201cconstant-time\u201d. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, 9\u201312 July 2018, pp. 328\u2013343. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00031","DOI":"10.1109\/CSF.2018.00031"},{"key":"4_CR21","unstructured":"Bernstein, D.J.: Cache-timing attacks on AES (2005). https:\/\/cr.yp.to\/antiforgery\/cachetiming-20050414.pdf"},{"issue":"1","key":"4_CR22","doi-asserted-by":"publisher","first-page":"137","DOI":"10.3233\/JCS-181136","volume":"27","author":"S Blazy","year":"2019","unstructured":"Blazy, S., Pichardie, D., Trieu, A.: Verifying constant-time implementations by abstract interpretation. J. Comput. Secur. 27(1), 137\u2013163 (2019). https:\/\/doi.org\/10.3233\/JCS-181136","journal-title":"J. Comput. Secur."},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Bloem, R., Gigerl, B., Gourjon, M., Hadzic, V., Mangard, S., Primas, R.: Power contracts: provably complete power leakage models for processors. In: Proceedings of the 29th ACM Conference on Computer and Communication Security. CCS, ACM (2022)","DOI":"10.1145\/3548606.3560600"},{"issue":"5","key":"4_CR24","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1016\/j.comnet.2005.01.010","volume":"48","author":"D Brumley","year":"2005","unstructured":"Brumley, D., Boneh, D.: Remote timing attacks are practical. Comput. Netw. 48(5), 701\u2013716 (2005)","journal-title":"Comput. Netw."},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Buiras, P., Nemati, H., Lindner, A., Guanciale, R.: Validation of side-channel models via observation refinement. In: MICRO 2021: 54th Annual IEEE\/ACM International Symposium on Microarchitecture, Virtual Event, Greece, 18\u201322 October 2021, pp. 578\u2013591. ACM (2021). https:\/\/doi.org\/10.1145\/3466752.3480130","DOI":"10.1145\/3466752.3480130"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Canella, C., et al.: Fallout: leaking data on meltdown-resistant CPUs. In: Proceedings of the 26th ACM Conference on Computer and Communication Security. CCS, ACM (2019)","DOI":"10.1145\/3319535.3363219"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Cauligi, S., et al.: Constant-time foundations for the new spectre era. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, 15\u201320 June 2020, pp. 913\u2013926. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385970","DOI":"10.1145\/3385412.3385970"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Cauligi, S., Disselkoen, C., Moghimi, D., Barthe, G., Stefan, D.: SoK: practical foundations for software spectre defenses. In: 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, 22\u201326 May 2022, pp. 666\u2013680. IEEE (2022). https:\/\/doi.org\/10.1109\/SP46214.2022.9833707","DOI":"10.1109\/SP46214.2022.9833707"},{"key":"4_CR29","unstructured":"Celio, C., Patterson, D.A., Asanovi\u0107, K.: The Berkeley out-of-order machine (BOOM): an industry-competitive, synthesizable, parameterized RISC-V processor. Technical Report UCB\/EECS-2015-167, EECS Department, University of California, Berkeley (2015). http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2015\/EECS-2015-167.html"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Daniel, L.A., Bardin, S., Rezk, T.: Binsec\/Rel: efficient relational symbolic execution for constant-time at binary-level. In: Proceedings of the 41st IEEE Symposium on Security and Privacy. S&P, IEEE (2020)","DOI":"10.1109\/SP40000.2020.00074"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Dasgupta, S., Park, D., Kasampalis, T., Adve, V.S., Rosu, G.: A complete formal semantics of x86-64 user-level instruction set architecture. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, 22\u201326 June 2019, pp. 1133\u20131148. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314601","DOI":"10.1145\/3314221.3314601"},{"key":"4_CR32","unstructured":"Degenbaev, U.: Formal specification of the x86 instruction set architecture. Ph.D. thesis, Saarland University (2012). http:\/\/scidok.sulb.uni-saarland.de\/volltexte\/2012\/4707\/"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Dinesh, S., Parthasarathy, M., Fletcher, C.W.: 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 (2024)","DOI":"10.1109\/SP54263.2024.00180"},{"key":"4_CR34","unstructured":"Dinesh, S., Zhu, Y., Fletcher, C.W.: H-Houdini: scalable invariant learning. In: Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. ASPLOS, ACM (2025)"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Djoudi, A., Bardin, S.: BINSEC: binary code analysis with low-level regions. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems \u2013 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, 11\u201318 April 2015. Proceedings. Lecture Notes in Computer Science, vol.\u00a09035, pp. 212\u2013217. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_17","DOI":"10.1007\/978-3-662-46681-0_17"},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"Doychev, G., K\u00f6pf, B., Mauborgne, L., Reineke, J.: CacheAudit: a tool for the static analysis of cache side channels. ACM Trans. Inf. Syst. Secur. 18(1) (2015)","DOI":"10.1145\/2756550"},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"ElAtali, H., G\u00fclmez, M., Nyman, T., Asokan, N.: BLACKOUT: data-oblivious computation with blinded capabilities. In: Huang, C., Chen, J., Shieh, S., Lie, D., Cortier, V. (eds.) Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, CCS 2025, Taipei, Taiwan, 13\u201317 October 2025, pp. 2039\u20132053. ACM (2025). https:\/\/doi.org\/10.1145\/3719027.3765169","DOI":"10.1145\/3719027.3765169"},{"key":"4_CR38","doi-asserted-by":"publisher","unstructured":"Fabian, X., Guarnieri, M., Patrignani, M.: Automatic detection of speculative execution combinations. In: Yin, H., Stavrou, A., Cremers, C., Shi, E. (eds.) Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, 7\u201311 November 2022, pp. 965\u2013978. ACM (2022). https:\/\/doi.org\/10.1145\/3548606.3560555","DOI":"10.1145\/3548606.3560555"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: International Symposium of Formal Methods Europe, pp. 500\u2013517. Springer (2001)","DOI":"10.1007\/3-540-45251-6_29"},{"key":"4_CR40","doi-asserted-by":"publisher","unstructured":"Fuchs, F.A., et al.: Safe speculation for CHERI. In: 42nd IEEE International Conference on Computer Design, ICCD 2024, Milan, Italy, 18\u201320 November 2024, pp. 364\u2013372. IEEE (2024). https:\/\/doi.org\/10.1109\/ICCD63220.2024.00063","DOI":"10.1109\/ICCD63220.2024.00063"},{"key":"4_CR41","doi-asserted-by":"publisher","unstructured":"Garc\u00eda, C.P., Brumley, B.B., Yarom, Y.: Make sure DSA signing exponentiations really are constant-time. In: Weippl, E.R., Katzenbeisser, S., Kruegel, C., Myers, A.C., Halevi, S. (eds.) Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, 24\u201328 October 2016, pp. 1639\u20131650. ACM (2016). https:\/\/doi.org\/10.1145\/2976749.2978420","DOI":"10.1145\/2976749.2978420"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Gerlach, L., Weber, D., Zhang, R., Schwarz, M.: A security RISC: microarchitectural attacks on hardware RISC-V CPUs. In: Proceedings of the 44th IEEE Symposium on Security and Privacy. S&P, IEEE (2023)","DOI":"10.1109\/SP46215.2023.10179399"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"Goel, S., Hunt Jr, W.A., Kaufmann, M.: Engineering a formal, executable x86 ISA simulator for software verification. In: Hinchey, M.G., Bowen, J.P., Olderog, E. (eds.) Provably Correct Systems, pp. 173\u2013209. NASA Monographs in Systems and Software Engineering. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-48628-4_8","DOI":"10.1007\/978-3-319-48628-4_8"},{"key":"4_CR44","doi-asserted-by":"publisher","unstructured":"Goel, S., Hunt Jr, W.A., Kaufmann, M., Ghosh, S.: Simulation and formal verification of x86 machine-code programs that make system calls. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21\u201324 October 2014, pp. 91\u201398. IEEE (2014). https:\/\/doi.org\/10.1109\/FMCAD.2014.6987600","DOI":"10.1109\/FMCAD.2014.6987600"},{"key":"4_CR45","doi-asserted-by":"crossref","unstructured":"Guarnieri, M., K\u00f6pf, B., Morales, J.F., Reineke, J., S\u00e1nchez, A.: Spectector: principled detection of speculative information flows. In: Proceedings of the 41st IEEE Symposium on Security and Privacy. S&P, IEEE (2020)","DOI":"10.1109\/SP40000.2020.00011"},{"key":"4_CR46","doi-asserted-by":"crossref","unstructured":"Guarnieri, M., K\u00f6pf, B., Reineke, J., Vila, P.: Hardware-software contracts for secure speculation. In: Proceedings of the 42nd IEEE Symposium on Security and Privacy. S&P, IEEE (2021)","DOI":"10.1109\/SP40001.2021.00036"},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"Gullasch, D., Bangerter, E., Krenn, S.: Cache games\u2014bringing access-based cache attacks on AES to practice. 2011 IEEE Symposium on Security and Privacy (S&P) (2011)","DOI":"10.1109\/SP.2011.22"},{"key":"4_CR48","doi-asserted-by":"publisher","unstructured":"Hasabnis, N., Sekar, R.: Extracting instruction semantics via symbolic execution of code generators. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, 13\u201318 November 2016, pp. 301\u2013313. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950335","DOI":"10.1145\/2950290.2950335"},{"key":"4_CR49","doi-asserted-by":"publisher","unstructured":"Heule, S., Schkufza, E., Sharma, R., Aiken, A.: Stratified synthesis: automatically learning the x86-64 instruction set. In: Krintz, C., Berger, E.D. (eds.) Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, 13\u201317 June 2016, pp. 237\u2013250. ACM (2016). https:\/\/doi.org\/10.1145\/2908080.2908121","DOI":"10.1145\/2908080.2908121"},{"key":"4_CR50","unstructured":"Hofmann, J., Vannacci, E., Fournet, C., K\u00f6pf, B., Oleksenko, O.: Speculation at fault: modeling and testing microarchitectural leakage of CPU exceptions. In: 32nd USENIX Security Symposium (USENIX Security 2023), pp. 7143\u20137160 (2023)"},{"key":"4_CR51","doi-asserted-by":"crossref","unstructured":"Hsiao, Y., Mulligan, D.P., Nikoleris, N., Petri, G., Trippel, C.: Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations. In: Proceedings of the 54th Annual IEEE\/ACM International Symposium on Microarchitecture. MICRO, ACM (2021)","DOI":"10.1145\/3466752.3480087"},{"key":"4_CR52","unstructured":"Hsiao, Y., et al.: RTL2M$$\\mu $$PATH: multi-$$\\mu $$path synthesis with applications to hardware security verification. In: Proceedings of the 2024 57th IEEE\/ACM International Symposium on Microarchitecture. MICRO, IEEE (2024)"},{"key":"4_CR53","unstructured":"Intel Corporation: Data operand independent timing instruction set architecture (ISA) guidance (2025). https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/software-security-guidance\/best-practices\/data-operand-independent-timing-isa-guidance.html. Accessed 30 Dec 2025"},{"key":"4_CR54","unstructured":"Intel Corporation: Intel\u00ae 64 and IA-32 Architectures Software Developer\u2019s Manual (2025). https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/intel-sdm.html"},{"key":"4_CR55","doi-asserted-by":"crossref","unstructured":"Kocher, P., et al.: Spectre attacks: exploiting speculative execution. In: Proceedings of the 41st IEEE Symposium on Security and Privacy. S&P, IEEE (2019)","DOI":"10.1109\/SP.2019.00002"},{"key":"4_CR56","doi-asserted-by":"publisher","unstructured":"Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Koblitz, N. (ed.) Advances in Cryptology \u2013 CRYPTO 1996, 16th Annual International Cryptology Conference, Santa Barbara, California, USA, 18\u201322 August 1996, Proceedings. Lecture Notes in Computer Science, vol.\u00a01109, pp. 104\u2013113. Springer (1996). https:\/\/doi.org\/10.1007\/3-540-68697-5_9","DOI":"10.1007\/3-540-68697-5_9"},{"key":"4_CR57","unstructured":"Leino, K.R.M.: This is Boogie 2 (2008). https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"issue":"7","key":"4_CR58","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"4_CR59","doi-asserted-by":"crossref","unstructured":"Liu, F., Yarom, Y., Ge, Q., Heiser, G., Lee, R.B.: Last-level cache side-channel attacks are practical. In: Proceedings of the 36th IEEE Symposium on Security and Privacy. S&P, IEEE (2015)","DOI":"10.1109\/SP.2015.43"},{"key":"4_CR60","doi-asserted-by":"crossref","unstructured":"Maisuradze, G., Rossow, C.: Ret2Spec: speculative execution using return stack buffers. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. CCS, ACM (2018)","DOI":"10.1145\/3243734.3243761"},{"key":"4_CR61","doi-asserted-by":"crossref","unstructured":"Mohr, G., Guarnieri, M., Reineke, J.: Synthesizing hardware-software leakage contracts for RISC-V open-source processors. In: Proceedings of the 27th Design, Automation and Test in Europe Conference and Exhibition. DATE (2024)","DOI":"10.23919\/DATE58400.2024.10546681"},{"key":"4_CR62","doi-asserted-by":"publisher","unstructured":"Molnar, D., Piotrowski, M., Schultz, D., Wagner, D.A.: The program counter security model: automatic detection and removal of control-flow side channel attacks. In: Won, D., Kim, S. (eds.) Information Security and Cryptology \u2013 ICISC 2005, 8th International Conference, Seoul, Korea, 1\u20132 December 2005, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a03935, pp. 156\u2013168. Springer (2005). https:\/\/doi.org\/10.1007\/11734727_14","DOI":"10.1007\/11734727_14"},{"key":"4_CR63","doi-asserted-by":"crossref","unstructured":"Nemati, H., Buiras, P., Lindner, A., Guanciale, R., Jacobs, S.: Validation of abstract side-channel models for computer architectures. In: Proceedings of the 32nd International Conference on Computer Aided Verification. CAV, Springer (2020)","DOI":"10.1007\/978-3-030-53288-8_12"},{"key":"4_CR64","doi-asserted-by":"crossref","unstructured":"Oleksenko, O., Fetzer, C., K\u00f6pf, B., Silberstein, M.: Revizor: testing black-box CPUs against speculation contracts. In: Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. ASPLOS, ACM (2022)","DOI":"10.1145\/3503222.3507729"},{"key":"4_CR65","doi-asserted-by":"crossref","unstructured":"Oleksenko, O., Guarnieri, M., K\u00f6pf, B., Silberstein, M.: Hide and seek with spectres: efficient discovery of speculative information leaks with random testing. In: Proceedings of the 44th IEEE Symposium on Security and Privacy. S&P, IEEE (2023)","DOI":"10.1109\/SP46215.2023.10179391"},{"key":"4_CR66","doi-asserted-by":"publisher","unstructured":"Osvik, D.A., Shamir, A., Tromer, E.: Cache attacks and countermeasures: the case of AES. In: Pointcheval, D. (ed.) Topics in Cryptology \u2013 CT-RSA 2006, The Cryptographers\u2019 Track at the RSA Conference 2006, San Jose, CA, USA, 13\u201317 February 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a03860, pp. 1\u201320. Springer (2006). https:\/\/doi.org\/10.1007\/11605805_1","DOI":"10.1007\/11605805_1"},{"key":"4_CR67","doi-asserted-by":"crossref","unstructured":"Patrignani, M., Guarnieri, M.: Exorcising spectres with secure compilers. In: Proceedings of the 28th ACM Conference on Computer and Communications Security. CCS, ACM (2021)","DOI":"10.1145\/3460120.3484534"},{"key":"4_CR68","unstructured":"Percival, C.: Cache missing for fun and profit. In: BSDCan (2005)"},{"key":"4_CR69","doi-asserted-by":"crossref","unstructured":"Purnal, A., Bognar, M., Piessens, F., Verbauwhede, I.: ShowTime: amplifying arbitrary CPU timing side channels. In: Proceedings of the 18th ACM Asia Conference on Computer and Communications Security. ASIA CCS, ACM (2023)","DOI":"10.1145\/3579856.3590332"},{"key":"4_CR70","doi-asserted-by":"publisher","unstructured":"Rakamaric, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification \u2013 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 18\u201322 July 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08559, pp. 106\u2013113. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"4_CR71","doi-asserted-by":"publisher","unstructured":"Reid, A.: Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture. In: Piskac, R., Talupur, M. (eds.) 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, 3\u20136 October 2016, pp. 161\u2013168. IEEE (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886675","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"4_CR72","unstructured":"Reid, A.: ARM Releases: Machine Readable Architecture Specification (2017). https:\/\/alastairreid.github.io\/ARM-v8a-xml-release\/. Accessed 21 Sept 2025"},{"key":"4_CR73","doi-asserted-by":"publisher","unstructured":"Reid, A., et al.: End-to-end verification of processors with ISA-Formal. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification \u2013 28th International Conference, CAV 2016, Toronto, ON, Canada, 17\u201323 July 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol.\u00a09780, pp. 42\u201358. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_3","DOI":"10.1007\/978-3-319-41540-6_3"},{"key":"4_CR74","doi-asserted-by":"publisher","unstructured":"Ristenpart, T., Tromer, E., Shacham, H., Savage, S.: Hey, you, get off of my cloud: exploring information leakage in third-party compute clouds. In: Al-Shaer, E., Jha, S., Keromytis, A.D. (eds.) Proceedings of the 2009 ACM Conference on Computer and Communications Security, CCS 2009, Chicago, Illinois, USA, 9\u201313 November 2009, pp. 199\u2013212. ACM (2009). https:\/\/doi.org\/10.1145\/1653662.1653687","DOI":"10.1145\/1653662.1653687"},{"key":"4_CR75","doi-asserted-by":"publisher","unstructured":"Roessle, I., Verbeek, F., Ravindran, B.: Formally verified big step semantics out of x86-64 binaries. In: Mahboubi, A., Myreen, M.O. (eds.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, 14\u201315 January 2019, pp. 181\u2013195. ACM (2019). https:\/\/doi.org\/10.1145\/3293880.3294102","DOI":"10.1145\/3293880.3294102"},{"key":"4_CR76","doi-asserted-by":"publisher","unstructured":"Sammler, M., et al.: Islaris: verification of machine code against authoritative ISA semantics. In: Jhala, R., Dillig, I. (eds.) PLDI 2022: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, 13\u201317 June 2022, pp. 825\u2013840. ACM (2022). https:\/\/doi.org\/10.1145\/3519939.3523434","DOI":"10.1145\/3519939.3523434"},{"key":"4_CR77","doi-asserted-by":"crossref","unstructured":"van Schaik, S., et al.: RIDL: rogue in-flight data load. In: Proceedings of the 40th IEEE Symposium on Security and Privacy. S&P, IEEE (2019)","DOI":"10.1109\/SP.2019.00087"},{"key":"4_CR78","doi-asserted-by":"crossref","unstructured":"Schwarz, M., et al.: ZombieLoad: cross-privilege-boundary data sampling. In: Proceedings of the 26th ACM Conference on Computer and Communication Security. CCS, ACM (2019)","DOI":"10.1145\/3319535.3354252"},{"key":"4_CR79","unstructured":"Stecklina, J., Prescher, T.: LazyFP: leaking FPU register state using microarchitectural side-channels. CoRR abs\/1806.07480 (2018)"},{"key":"4_CR80","doi-asserted-by":"crossref","unstructured":"Tan, Q., Yang, Y., Bourgeat, T., Malik, S., Yan, M.: RTL verification for secure speculation using contract shadow logic. In: Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. ASPLOS, ACM (2025)","DOI":"10.1145\/3669940.3707243"},{"key":"4_CR81","doi-asserted-by":"crossref","unstructured":"Tsunoo, Y., Saito, T., Suzaki, T., Shigeri, M., Miyauchi, H.: Cryptanalysis of DES implemented on computers with cache. In: Proceedings of the 5th International Workshop on Cryptographic Hardware and Embedded Systems. CHES, Springer (2003)","DOI":"10.1007\/978-3-540-45238-6_6"},{"key":"4_CR82","doi-asserted-by":"publisher","unstructured":"Vassena, M., et al.: Automatically eliminating speculative leaks from cryptographic code with blade. Proc. ACM Program. Lang. 5(POPL), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3434330","DOI":"10.1145\/3434330"},{"key":"4_CR83","doi-asserted-by":"publisher","unstructured":"van\u00a0der Wall, S., Meyer, R.: SNIP: speculative execution and non-interference preservation for compiler transformations. Proc. ACM Program. Lang. 9(POPL), 1506\u20131535 (2025). https:\/\/doi.org\/10.1145\/3704887","DOI":"10.1145\/3704887"},{"key":"4_CR84","doi-asserted-by":"crossref","unstructured":"Wang, Z., Mohr, G., von Gleissenthall, K., Reineke, J., Guarnieri, M.: Specification and verification of side-channel security for open-source processors via leakage contracts. In: Proceedings of the 30th ACM Conference on Computer and Communications Security. CCS, ACM (2023)","DOI":"10.1145\/3576915.3623192"},{"key":"4_CR85","doi-asserted-by":"crossref","unstructured":"Wang, Z., Mohr, G., von Gleissenthall, K., Reineke, J., Guarnieri, M.: Synthesis of sound and precise leakage contracts for open-source RISC-V processors. In: Proceedings of the 32nd ACM Conference on Computer and Communications Security. CCS 2025, ACM (2025)","DOI":"10.1145\/3719027.3765148"},{"key":"4_CR86","doi-asserted-by":"crossref","unstructured":"Waterman, A., Lee, Y., Patterson, D.A., Asanovi\u0107, K.: 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 (2014)","DOI":"10.21236\/ADA605735"},{"key":"4_CR87","unstructured":"Weber, D., Ibrahim, A., Nemati, H., Schwarz, M., Rossow, C.: Osiris: automated discovery of microarchitectural side channels. In: Proceedings of the 30th USENIX Security Symposium. USENIX Security, USENIX Association (2021)"},{"key":"4_CR88","doi-asserted-by":"publisher","unstructured":"Woodruff, J., et al.: The CHERI capability model: revisiting RISC in an age of risk. In: ACM\/IEEE 41st International Symposium on Computer Architecture, ISCA 2014, Minneapolis, MN, USA, 14\u201318 June 2014, pp. 457\u2013468. IEEE Computer Society (2014). https:\/\/doi.org\/10.1109\/ISCA.2014.6853201","DOI":"10.1109\/ISCA.2014.6853201"},{"key":"4_CR89","unstructured":"Yarom, Y., Falkner, K.: Flush+Reload: a high resolution, low noise, L3 cache side-channel attack. In: Proceedings of the 23rd USENIX Security Symposium. USENIX Security, USENIX Association (2014)"},{"key":"4_CR90","doi-asserted-by":"crossref","unstructured":"Yarom, Y., Genkin, D., Heninger, N.: CacheBleed: a timing attack on openssl constant-time RSA. J. Cryptogr. Eng. 7(2) (2017)","DOI":"10.1007\/s13389-017-0152-y"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-8617-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T14:22:04Z","timestamp":1778077324000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-8617-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9789819586165","9789819586172"],"references-count":90,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-8617-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"1 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Summer School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Beijing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tis.ios.ac.cn\/SETSS2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}