{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:58:54Z","timestamp":1750309134287,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T00:00:00Z","timestamp":1698019200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["2225441"],"award-info":[{"award-number":["2225441"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,23]]},"DOI":"10.1145\/3625275.3625402","type":"proceedings-article","created":{"date-parts":[[2023,10,20]],"date-time":"2023-10-20T13:09:57Z","timestamp":1697807397000},"page":"26-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["The K2 Architecture for Trustworthy Hardware Security Modules"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9355-6857","authenticated-orcid":false,"given":"Anish","family":"Athalye","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7098-586X","authenticated-orcid":false,"given":"Frans","family":"Kaashoek","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0238-2703","authenticated-orcid":false,"given":"Nickolai","family":"Zeldovich","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5692-3347","authenticated-orcid":false,"given":"Joseph","family":"Tassarotti","sequence":"additional","affiliation":[{"name":"New York University, New York, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,23]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2004. CVE-2004-0320. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2004-0320. 2004. CVE-2004-0320. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2004-0320."},{"key":"e_1_3_2_1_2_1","unstructured":"2015. YSA-2015-1. https:\/\/developers.yubico.com\/ykneo-openpgp\/SecurityAdvisory%202015-04-14.html. 2015. YSA-2015-1. https:\/\/developers.yubico.com\/ykneo-openpgp\/SecurityAdvisory%202015-04-14.html."},{"key":"e_1_3_2_1_3_1","unstructured":"2018. CVE-2018-6875. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2018-6875. 2018. CVE-2018-6875. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2018-6875."},{"key":"e_1_3_2_1_4_1","unstructured":"2018. YSA-2018-01. https:\/\/www.yubico.com\/support\/security-advisories\/ysa-2018-01\/. 2018. YSA-2018-01. https:\/\/www.yubico.com\/support\/security-advisories\/ysa-2018-01\/."},{"key":"e_1_3_2_1_5_1","unstructured":"2019. CVE-2019-18671. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2019-18671. 2019. CVE-2019-18671. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2019-18671."},{"key":"e_1_3_2_1_6_1","unstructured":"2019. CVE-2019-18672. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2019-18672. 2019. CVE-2019-18672. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2019-18672."},{"key":"e_1_3_2_1_7_1","unstructured":"2020. YSA-2020-04. https:\/\/www.yubico.com\/support\/security-advisories\/ysa-2020-04\/. 2020. YSA-2020-04. https:\/\/www.yubico.com\/support\/security-advisories\/ysa-2020-04\/."},{"key":"e_1_3_2_1_8_1","unstructured":"2021. CVE-2021-31616. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2021-31616. 2021. CVE-2021-31616. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2021-31616."},{"key":"e_1_3_2_1_9_1","unstructured":"2021. WhatsApp Security Whitepaper: Security of End-to-End Encrypted Backups. https:\/\/www.whatsapp.com\/security\/WhatsApp_Security_Encrypted_Backups_Whitepaper.pdf. 2021. WhatsApp Security Whitepaper: Security of End-to-End Encrypted Backups. https:\/\/www.whatsapp.com\/security\/WhatsApp_Security_Encrypted_Backups_Whitepaper.pdf."},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the 26th ACM Conference on Computer and Communications Security (CCS)","author":"Aas Josh","year":"2019","unstructured":"Josh Aas , Richard Barnes , Benton Case , Zakir Durumeric , Peter Eckersley , Alan Flores-L\u00f3pez , J. Alex Halderman , Jacob Hoffman-Andrews , James Kasten , Eric Rescorla , Seth Schoen , and Brad Warren . 2019 . Let's Encrypt: An Automated Certificate Authority to Encrypt the Entire Web . In Proceedings of the 26th ACM Conference on Computer and Communications Security (CCS) . London, United Kingdom, 2473--2487. Josh Aas, Richard Barnes, Benton Case, Zakir Durumeric, Peter Eckersley, Alan Flores-L\u00f3pez, J. Alex Halderman, Jacob Hoffman-Andrews, James Kasten, Eric Rescorla, Seth Schoen, and Brad Warren. 2019. Let's Encrypt: An Automated Certificate Authority to Encrypt the Entire Web. In Proceedings of the 26th ACM Conference on Computer and Communications Security (CCS). London, United Kingdom, 2473--2487."},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the 2002 IACR Workshop on Cryptographic Hardware and Embedded Systems (CHES)","author":"Agrawal Dakshi","year":"2002","unstructured":"Dakshi Agrawal , Bruce Archambeault , Josyula R. Rao , and Pankaj Rohatgi . 2002 . The EM Side-Channel(s) . In Proceedings of the 2002 IACR Workshop on Cryptographic Hardware and Embedded Systems (CHES) . Redwood City, CA. Dakshi Agrawal, Bruce Archambeault, Josyula R. Rao, and Pankaj Rohatgi. 2002. The EM Side-Channel(s). In Proceedings of the 2002 IACR Workshop on Cryptographic Hardware and Embedded Systems (CHES). Redwood City, CA."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_5"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the 23rd International Conference on Fast Software Encryption (FSE)","author":"Almeida Jos\u00e9 Bacelar","year":"2016","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , and Fran\u00e7ois Dupressoir . 2016 . Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC . In Proceedings of the 23rd International Conference on Fast Software Encryption (FSE) . Bochum, Germany, 163--184. Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and Fran\u00e7ois Dupressoir. 2016. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. In Proceedings of the 23rd International Conference on Fast Software Encryption (FSE). Bochum, Germany, 163--184."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/3241094.3241100"},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP). Huntsville","author":"Athalye Anish","year":"2019","unstructured":"Anish Athalye , Adam Belay , M. Frans Kaashoek , Robert Morris , and Nickolai Zeldovich . 2019 . Notary: A Device for Secure Transaction Approval . In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP). Huntsville , Ontario, Canada, 97--113. Anish Athalye, Adam Belay, M. Frans Kaashoek, Robert Morris, and Nickolai Zeldovich. 2019. Notary: A Device for Secure Transaction Approval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP). Huntsville, Ontario, Canada, 97--113."},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Athalye Anish","year":"2022","unstructured":"Anish Athalye , M. Frans Kaashoek , and Nickolai Zeldovich . 2022 . Verifying Hardware Security Modules with Information-Preserving Refinement . In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI) . Carlsbad, CA, 503--519. Anish Athalye, M. Frans Kaashoek, and Nickolai Zeldovich. 2022. Verifying Hardware Security Modules with Information-Preserving Refinement. In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI). Carlsbad, CA, 503--519."},{"key":"e_1_3_2_1_17_1","unstructured":"Jean-Baptiste B\u00e9drune and Gabriel Campana. 2019. Everybody be Cool This is a Robbery! https:\/\/donjon.ledger.com\/BlackHat2019-presentation\/. Jean-Baptiste B\u00e9drune and Gabriel Campana. 2019. Everybody be Cool This is a Robbery! https:\/\/donjon.ledger.com\/BlackHat2019-presentation\/."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243131"},{"key":"e_1_3_2_1_19_1","volume-title":"Proceedings of the 26th USENIX Security Symposium","author":"Bond Barry","year":"2017","unstructured":"Barry Bond , Chris Hawblitzel , Manos Kapritsos , K. Rustan M. Leino , Jacob R. Lorch , Bryan Parno , Ashay Rane , Srinath Setty , and Laure Thompson . 2017 . Vale: Verifying High-Performance Cryptographic Assembly Code . In Proceedings of the 26th USENIX Security Symposium . Vancouver, Canada, 917--934. Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In Proceedings of the 26th USENIX Security Symposium. Vancouver, Canada, 917--934."},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the 42th IEEE\/ACM International Symposium on Microarchitecture","author":"Buiras Pablo","year":"2021","unstructured":"Pablo Buiras , Hamed Nemati , Andreas Lindner , and Roberto Guanciale . 2021 . Validation of Side-Channel Models via Observation Refinement . In Proceedings of the 42th IEEE\/ACM International Symposium on Microarchitecture . Athens, Greece, 578--591. Pablo Buiras, Hamed Nemati, Andreas Lindner, and Roberto Guanciale. 2021. Validation of Side-Channel Models via Observation Refinement. In Proceedings of the 42th IEEE\/ACM International Symposium on Microarchitecture. Athens, Greece, 578--591."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Sunjay Cauligi Gary Soeller Brian Johannesmeyer Fraser Brown Riad S. Wahby John Renner Benjamin Gr\u00e9goire Gilles Barthe Ranjit Jhala and Deian Stefan. 2019. FaCT: A DSL for Timing-Sensitive Computation. (June 2019) 174--189. Sunjay Cauligi Gary Soeller Brian Johannesmeyer Fraser Brown Riad S. Wahby John Renner Benjamin Gr\u00e9goire Gilles Barthe Ranjit Jhala and Deian Stefan. 2019. FaCT: A DSL for Timing-Sensitive Computation. (June 2019) 174--189.","DOI":"10.1145\/3314221.3314605"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_3_2_1_24_1","unstructured":"Filippo Cremonese. 2020. Security Analysis of the Solo Firmware. https:\/\/blog.doyensec.com\/2020\/02\/19\/solokeys-audit.html. Filippo Cremonese. 2020. Security Analysis of the Solo Firmware. https:\/\/blog.doyensec.com\/2020\/02\/19\/solokeys-audit.html."},{"key":"e_1_3_2_1_25_1","volume-title":"Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Virtual conference.","author":"Erbsen Andres","year":"2021","unstructured":"Andres Erbsen , Samuel Gruetter , Joonwon Choi , Clark Wood , and Adam Chlipala . 2021 . Integration Verification across Software and Hardware for a Simple Embedded System . In Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Virtual conference. Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, and Adam Chlipala. 2021. Integration Verification across Software and Hardware for a Simple Embedded System. In Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Virtual conference."},{"key":"e_1_3_2_1_26_1","volume-title":"Without Compromises. In Proceedings of the 40th IEEE Symposium on Security and Privacy","author":"Erbsen Andres","year":"2019","unstructured":"Andres Erbsen , Jade Philipoom , Jason Gross , Robert Sloan , and Adam Chlipala . 2019 . Simple High-Level Code For Cryptographic Arithmetic - With Proofs , Without Compromises. In Proceedings of the 40th IEEE Symposium on Security and Privacy . San Francisco, CA, 73--90. Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple High-Level Code For Cryptographic Arithmetic - With Proofs, Without Compromises. In Proceedings of the 40th IEEE Symposium on Security and Privacy. San Francisco, CA, 73--90."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the 42nd IEEE Symposium on Security and Privacy. Virtual conference","author":"Guarnieri Marco","year":"2021","unstructured":"Marco Guarnieri , Boris K\u00f6pf , Jan Reineke , and Pepe Vila . 2021 . Hardware-Software Contracts for Secure Speculation . In Proceedings of the 42nd IEEE Symposium on Security and Privacy. Virtual conference , 1868--1883. Marco Guarnieri, Boris K\u00f6pf, Jan Reineke, and Pepe Vila. 2021. Hardware-Software Contracts for Secure Speculation. In Proceedings of the 42nd IEEE Symposium on Security and Privacy. Virtual conference, 1868--1883."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3421473.3421475"},{"key":"e_1_3_2_1_30_1","unstructured":"Mason Hemmel Jason Meltzer Thomas Pornin Keegan Ryan Javed Samuel David Wong Rob Wood and Greg Worona. 2018. Android Cloud Backup\/Restore. https:\/\/research.nccgroup.com\/wp-content\/uploads\/2020\/07\/Final_Public_Report_NCC_Group_Google_EncryptedBackup_2018-10-10_v1.0.pdf. Mason Hemmel Jason Meltzer Thomas Pornin Keegan Ryan Javed Samuel David Wong Rob Wood and Greg Worona. 2018. Android Cloud Backup\/Restore. https:\/\/research.nccgroup.com\/wp-content\/uploads\/2020\/07\/Final_Public_Report_NCC_Group_Google_EncryptedBackup_2018-10-10_v1.0.pdf."},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of the 12th Smart Card Research and Advanced Application Conference (CARDIS)","author":"Hutter Michael","year":"2013","unstructured":"Michael Hutter and J\u00f6rn-Marc Schmidt . 2013 . The Temperature Side Channel and Heating Fault Attacks . In Proceedings of the 12th Smart Card Research and Advanced Application Conference (CARDIS) . Berlin, Germany, 219--235. Michael Hutter and J\u00f6rn-Marc Schmidt. 2013. The Temperature Side Channel and Heating Fault Attacks. In Proceedings of the 12th Smart Card Research and Advanced Application Conference (CARDIS). Berlin, Germany, 219--235."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","first-page":"281","DOI":"10.46586\/tches.v2020.i4.281-308","article-title":"Minerva: The curse of ECDSA nonces (Systematic analysis of lattice attacks on noisy leakage of bit-length of ECDSA nonces)","volume":"2020","author":"Jancar Jan","year":"2020","unstructured":"Jan Jancar , Vladimir Sedlacek , Petr Svenda , and Marek Sys . 2020 . Minerva: The curse of ECDSA nonces (Systematic analysis of lattice attacks on noisy leakage of bit-length of ECDSA nonces) . IACR Transactions on Cryptographic Hardware and Embedded Systems 2020 , 4 (2020), 281 -- 308 . Jan Jancar, Vladimir Sedlacek, Petr Svenda, and Marek Sys. 2020. Minerva: The curse of ECDSA nonces (Systematic analysis of lattice attacks on noisy leakage of bit-length of ECDSA nonces). IACR Transactions on Cryptographic Hardware and Embedded Systems 2020, 4 (2020), 281--308.","journal-title":"IACR Transactions on Cryptographic Hardware and Embedded Systems"},{"key":"e_1_3_2_1_33_1","unstructured":"Ivan Krsti\u0107. 2016. Behind the Scenes with iOS Security. https:\/\/www.blackhat.com\/docs\/us-16\/materials\/us-16-Krstic.pdf. Ivan Krsti\u0107. 2016. Behind the Scenes with iOS Security. https:\/\/www.blackhat.com\/docs\/us-16\/materials\/us-16-Krstic.pdf."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314622"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44499-8_6"},{"key":"e_1_3_2_1_36_1","volume-title":"Proceedings of the 29th USENIX Security Symposium. Virtual conference","author":"Moghimi Daniel","year":"2020","unstructured":"Daniel Moghimi , Berk Sunar , Thomas Eisenbarth , and Nadia Heninger . 2020 . TPM-FAIL: TPM meets Timing and Lattice Attacks . In Proceedings of the 29th USENIX Security Symposium. Virtual conference , 2057--2073. Daniel Moghimi, Berk Sunar, Thomas Eisenbarth, and Nadia Heninger. 2020. TPM-FAIL: TPM meets Timing and Lattice Attacks. In Proceedings of the 29th USENIX Security Symposium. Virtual conference, 2057--2073."},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the 5th Workshop on Computer Architecture Research with RISC-V (CARRV). Virtual conference.","author":"Moroze Noah","year":"2021","unstructured":"Noah Moroze , Anish Athalye , M. Frans Kaashoek , and Nickolai Zeldovich . 2021 . rtlv: push-button verification of software on hardware . In Proceedings of the 5th Workshop on Computer Architecture Research with RISC-V (CARRV). Virtual conference. Noah Moroze, Anish Athalye, M. Frans Kaashoek, and Nickolai Zeldovich. 2021. rtlv: push-button verification of software on hardware. In Proceedings of the 5th Workshop on Computer Architecture Research with RISC-V (CARRV). Virtual conference."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3470496.3527412"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_40_1","unstructured":"OASIS PKCS 11 Technical Committee. 2020. PKCS #11 Cryptographic Token Interface Current Mechanisms Specification Version 3.0. https:\/\/docs.oasis-open.org\/pkcs11\/pkcs11-curr\/v3.0\/os\/pkcs11-curr-v3.0-os.html. OASIS PKCS 11 Technical Committee. 2020. PKCS #11 Cryptographic Token Interface Current Mechanisms Specification Version 3.0. https:\/\/docs.oasis-open.org\/pkcs11\/pkcs11-curr\/v3.0\/os\/pkcs11-curr-v3.0-os.html."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507729"},{"key":"e_1_3_2_1_42_1","volume-title":"Proceedings of the 44th IEEE Symposium on Security and Privacy","author":"Oleksenko Oleksii","year":"2023","unstructured":"Oleksii Oleksenko , Marco Guarnieri , Boris Kopf , and Mark Silberstein . 2023 . 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 . San Francisco, CA, 1737--1752. Oleksii Oleksenko, Marco Guarnieri, Boris Kopf, and Mark Silberstein. 2023. 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. San Francisco, CA, 1737--1752."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_3_2_1_44_1","volume-title":"Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson Helgi","year":"2018","unstructured":"Helgi Sigurbjarnarson , Luke Nelson , Bruno Castro-Karney , James Bornholt , Emina Torlak , and Xi Wang . 2018 . Nickel: A Framework for Design and Verification of Information Flow Control Systems . In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI) . Carlsbad, CA, 287--306. Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. 2018. Nickel: A Framework for Design and Verification of Information Flow Control Systems. In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI). Carlsbad, CA, 287--306."},{"key":"e_1_3_2_1_45_1","volume-title":"Proceedings of the 25th International Symposium on Formal Methods (FM)","author":"Sison Robert","year":"2023","unstructured":"Robert Sison , Scott Buckley , Toby Murray , Gerwin Klein , and Gernot Heiser . 2023 . Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems . In Proceedings of the 25th International Symposium on Formal Methods (FM) . L\u00fcbeck, Germany, 103--121. Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein, and Gernot Heiser. 2023. Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems. In Proceedings of the 25th International Symposium on Formal Methods (FM). L\u00fcbeck, Germany, 103--121."},{"key":"e_1_3_2_1_46_1","unstructured":"Sampath Srinivas Dirk Balfanz Eric Tiffany and Alexei Czeskis. 2016. Universal 2nd Factor (U2F) Overview. https:\/\/fidoalliance.org\/specs\/fido-u2f-v1.1-id-20160915\/fido-u2f-overview-v1.1-id-20160915.pdf. Sampath Srinivas Dirk Balfanz Eric Tiffany and Alexei Czeskis. 2016. Universal 2nd Factor (U2F) Overview. https:\/\/fidoalliance.org\/specs\/fido-u2f-v1.1-id-20160915\/fido-u2f-overview-v1.1-id-20160915.pdf."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_1_48_1","unstructured":"Florian Uekermann. 2016. Buggy OTP slot range check. https:\/\/github.com\/Nitrokey\/nitrokey-pro-firmware\/issues\/4. Florian Uekermann. 2016. Buggy OTP slot range check. https:\/\/github.com\/Nitrokey\/nitrokey-pro-firmware\/issues\/4."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"crossref","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. https:\/\/arxiv.org\/abs\/2305.06979. 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. https:\/\/arxiv.org\/abs\/2305.06979.","DOI":"10.1145\/3576915.3623192"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"event":{"name":"KISV '23: 1st Workshop on Kernel Isolation, Safety and Verification","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"],"location":"Koblenz Germany","acronym":"KISV '23"},"container-title":["Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3625275.3625402","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:04Z","timestamp":1750287004000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3625275.3625402"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,23]]},"references-count":50,"alternative-id":["10.1145\/3625275.3625402","10.1145\/3625275"],"URL":"https:\/\/doi.org\/10.1145\/3625275.3625402","relation":{},"subject":[],"published":{"date-parts":[[2023,10,23]]},"assertion":[{"value":"2023-10-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}