{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,2]],"date-time":"2025-10-02T00:47:45Z","timestamp":1759366065681,"version":"build-2065373602"},"publisher-location":"New York, NY, USA","reference-count":65,"publisher":"ACM","funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["2327336","2155235","2120642","2120696","2154964","2048262","2303639"],"award-info":[{"award-number":["2327336","2155235","2120642","2120696","2154964","2048262","2303639"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3731569.3764856","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:43:24Z","timestamp":1759322604000},"page":"786-801","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["TickTock: Verified Isolation in a Production Embedded OS"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-7723-5032","authenticated-orcid":false,"given":"Vivien","family":"Rindisbacher","sequence":"first","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1784-4512","authenticated-orcid":false,"given":"Evan","family":"Johnson","sequence":"additional","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6838-3714","authenticated-orcid":false,"given":"Nico","family":"Lehmann","sequence":"additional","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0569-3806","authenticated-orcid":false,"given":"Tyler","family":"Potyondy","sequence":"additional","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7720-6267","authenticated-orcid":false,"given":"Pat","family":"Pannuto","sequence":"additional","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6617-8029","authenticated-orcid":false,"given":"Stefan","family":"Savage","sequence":"additional","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7041-7464","authenticated-orcid":false,"given":"Deian","family":"Stefan","sequence":"additional","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1802-9421","authenticated-orcid":false,"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,10,12]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"International Conference on Verified Software: Theories, Tools, and Experiments. Springer.","author":"Alkassar Eyad","year":"2010","unstructured":"Eyad Alkassar, Mark A Hillebrand, Wolfgang Paul, and Elena Petrova. 2010. Automated verification of a small hypervisor. In International Conference on Verified Software: Theories, Tools, and Experiments. Springer."},{"key":"e_1_3_2_1_2_1","volume-title":"Proc. 2nd Workshop on Mixed Criticality Systems (WMC), RTSS.","author":"Armbrust Eric","year":"2014","unstructured":"Eric Armbrust, Jiguo Song, Gedare Bloom, and Gabriel Parmer. 2014. On spatial isolation for mixed criticality, embedded systems. In Proc. 2nd Workshop on Mixed Criticality Systems (WMC), RTSS."},{"key":"e_1_3_2_1_3_1","volume-title":"Summers","author":"Astrauskas Vytautas","year":"2022","unstructured":"Vytautas Astrauskas, Aurel B\u00edl\u00fd, Jon\u00e1\u0161 Fiala, Zachary Grannan, Christoph Matheja, Peter M\u00fcller, Federico Poli, and Alexander J. Summers. 2022. The Prusti Project: Formal Verification for Rust. In NASA Formal Methods. Springer."},{"key":"e_1_3_2_1_4_1","volume-title":"Proceedings of the 15th European Workshop on Systems Security (EuroSec '22)","author":"Ayers Hudson","year":"2022","unstructured":"Hudson Ayers, Prabal Dutta, Philip Levis, Amit Levy, Pat Pannuto, Johnathan Van Why, and Jean-Luc Watson. 2022. Tiered trust for useful embedded systems security. In Proceedings of the 15th European Workshop on Systems Security (EuroSec '22). ACM."},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the 15th European Workshop on Systems Security.","author":"Ayers Hudson","year":"2022","unstructured":"Hudson Ayers, Prabal Dutta, Philip Levis, Amit Levy, Pat Pannuto, Johnathan Van Why, and Jean-Luc Watson. 2022. Tiered trust for useful embedded systems security. In Proceedings of the 15th European Workshop on Systems Security."},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the 23rd ACM SIGPLAN\/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems.","author":"Ayers Hudson","year":"2022","unstructured":"Hudson Ayers, Evan Laufer, Paul Mure, Jaehyeon Park, Eduardo Rodelo, Thea Rossman, Andrey Pronin, Philip Levis, and Johnathan Van Why. 2022. Tighten Rust's belt: shrinking embedded Rust binaries. In Proceedings of the 23rd ACM SIGPLAN\/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems."},{"key":"e_1_3_2_1_7_1","volume-title":"The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64, 8","author":"Baudin Patrick","year":"2021","unstructured":"Patrick Baudin, Fran\u00e7ois Bobot, David B\u00fchler, Lo\u00efc Correnson, Florent Kirchner, Nikolai Kosmatov, Andr\u00e9 Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles, and Nicky Williams. 2021. The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64, 8 (2021)."},{"key":"e_1_3_2_1_8_1","volume-title":"Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Castran. 2010. Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions (1st ed.).","edition":"1"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 26th USENIX Conference on Security Symposium (SEC'17)","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 Conference on Security Symposium (SEC'17). USENIX."},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the 19th Workshop on Hot Topics in Operating Systems (HOTOS '23)","author":"Brun Matthias","year":"2023","unstructured":"Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger, and Andrea Lattuada. 2023. Beyond isolation: OS verification as a foundation for correct applications. In Proceedings of the 19th Workshop on Hot Topics in Operating Systems (HOTOS '23). ACM."},{"key":"e_1_3_2_1_11_1","unstructured":"Brad Campbell. 2020. riscv: pmp: disallow access above app brk. https:\/\/github.com\/tock\/tock\/pull\/2173 GitHub pull request."},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (KISV '23)","author":"Chen Xiangdong","year":"2023","unstructured":"Xiangdong Chen, Zhaofeng Li, Lukas Mesicek, Vikram Narayanan, and Anton Burtsev. 2023. Atmosphere: Towards Practical Verified Kernels in Rust. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (KISV '23). ACM."},{"key":"e_1_3_2_1_13_1","volume-title":"27th USENIX Security Symposium (USENIX Security 18)","author":"Clements Abraham A","year":"2018","unstructured":"Abraham A Clements, Naif Saleh Almakhdhub, Saurabh Bagchi, and Mathias Payer. 2018. ACES: Automatic compartments for embedded systems. In 27th USENIX Security Symposium (USENIX Security 18)."},{"key":"e_1_3_2_1_14_1","volume-title":"2017 IEEE Symposium on Security and Privacy (SP). IEEE.","author":"Clements Abraham A","year":"2017","unstructured":"Abraham A Clements, Naif Saleh Almakhdhub, Khaled S Saab, Prashast Srivastava, Jinkyu Koo, Saurabh Bagchi, and Mathias Payer. 2017. Protecting bare-metal embedded systems with privilege overlays. In 2017 IEEE Symposium on Security and Privacy (SP). IEEE."},{"key":"e_1_3_2_1_15_1","volume-title":"2009 31st International Conference on Software Engineering - Companion Volume.","author":"Dahlweid Markus","year":"2009","unstructured":"Markus Dahlweid, Michal Moskal, Thomas Santen, Stephan Tobies, and Wolfram Schulte. 2009. VCC: Contract-based modular verification of concurrent C. In 2009 31st International Conference on Software Engineering - Companion Volume."},{"key":"e_1_3_2_1_16_1","volume-title":"2021 8th International Conference on Future Internet of Things and Cloud (FiCloud).","author":"Dejon Nicolas","year":"2021","unstructured":"Nicolas Dejon, Chrystel Gaber, and Gilles Grimaud. 2021. Nested compartmentalisation for constrained devices. In 2021 8th International Conference on Future Internet of Things and Cloud (FiCloud)."},{"key":"e_1_3_2_1_17_1","volume-title":"1979 International Workshop on Managing Requirements Knowledge (MARK). IEEE.","author":"Feiertag Richard J","year":"1979","unstructured":"Richard J Feiertag and Peter G Neumann. 1979. The foundations of a provably secure operating system (PSOS). In 1979 International Workshop on Managing Requirements Knowledge (MARK). IEEE."},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the 26th Symposium on Operating Systems Principles (SOSP '17)","author":"Ferraiuolo Andrew","year":"2017","unstructured":"Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. 2017. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the 26th Symposium on Operating Systems Principles (SOSP '17). ACM."},{"key":"e_1_3_2_1_19_1","unstructured":"Alistair Francis. 2022. arch\/rv32i: pmp\/ePMP: Fixup PMP comparision. https:\/\/github.com\/tock\/tock\/pull\/2947 GitHub pull request."},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the Second Asia-Pacific Workshop on Systems.","author":"Gu Liang","year":"2011","unstructured":"Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, and David Costanzo. 2011. CertiKOS: A certified kernel for secure cloud computing. In Proceedings of the Second Asia-Pacific Workshop on Systems."},{"key":"e_1_3_2_1_21_1","volume-title":"Building certified concurrent OS kernels. Commun. ACM 62, 10","author":"Gu Ronghui","year":"2019","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, J\u00e9r\u00e9mie Koenig, Xiongnan Wu, Vilhelm Sj\u00f6berg, and David Costanzo. 2019. Building certified concurrent OS kernels. Commun. ACM 62, 10 (2019)."},{"key":"e_1_3_2_1_22_1","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)."},{"key":"e_1_3_2_1_23_1","article-title":"Provably secure memory isolation for Linux on ARM","volume":"24","author":"Guanciale Roberto","year":"2016","unstructured":"Roberto Guanciale, Hamed Nemati, Mads Dam, and Christoph Baumann. 2016. Provably secure memory isolation for Linux on ARM. Journal of Computer Security 24, 6 (2016).","journal-title":"Journal of Computer Security"},{"key":"e_1_3_2_1_24_1","volume-title":"Proceedings of the 1st Workshop on Isolation and Integration in Embedded Systems.","author":"Heiser Gernot","year":"2008","unstructured":"Gernot Heiser. 2008. The role of virtualization in embedded systems. In Proceedings of the 1st Workshop on Isolation and Integration in Embedded Systems."},{"key":"e_1_3_2_1_25_1","unstructured":"Tony Hoare. 1980. Turing Award Lecture."},{"key":"e_1_3_2_1_26_1","unstructured":"Evan Johnson. 2024. Defensive programming in MPU driver API. https:\/\/github.com\/tock\/tock\/issues\/4104 GitHub issue."},{"key":"e_1_3_2_1_27_1","volume-title":"IEEE Symposium on Security and Privacy (S&P). IEEE.","author":"Johnson Evan","year":"2023","unstructured":"Evan Johnson, Evan Laufer, Zijie Zhao, Dan Gohman, Shravan Narayan, Stefan Savage, Deian Stefan, and Fraser Brown. 2023. WaVe: a verifiably secure WebAssembly sandboxing runtime. In IEEE Symposium on Security and Privacy (S&P). IEEE."},{"key":"e_1_3_2_1_28_1","volume-title":"2023 IEEE Symposium on Security and Privacy (SP).","author":"Khan Arslan","year":"2023","unstructured":"Arslan Khan, Dongyan Xu, and Dave Jing Tian. 2023. EC: Embedded Systems Compartmentalization via Intra-Kernel Isolation. In 2023 IEEE Symposium on Security and Privacy (SP)."},{"key":"e_1_3_2_1_29_1","volume-title":"Network and Distributed System Security Symposium.","author":"Kim Chung Hwan","year":"2018","unstructured":"Chung Hwan Kim, Taegyu Kim, Hongjun Choi, Zhongshu Gu, Byoungyoung Lee, X. Zhang, and Dongyan Xu. 2018. Securing Real-Time Microcontroller Systems through Customized Memory View Switching. In Network and Distributed System Security Symposium."},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the ACM SIGOPS 22nd Symposium on Operating systems principles.","author":"Klein Gerwin","year":"2009","unstructured":"Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. 2009. seL4: Formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating systems principles."},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of the Ninth European Conference on Computer Systems (EuroSys '14)","author":"Koeberl Patrick","year":"2014","unstructured":"Patrick Koeberl, Steffen Schulz, Ahmad-Reza Sadeghi, and Vijay Varadharajan. 2014. TrustLite: a security architecture for tiny embedded devices. In Proceedings of the Ninth European Conference on Computer Systems (EuroSys '14). ACM."},{"key":"e_1_3_2_1_32_1","volume-title":"The Real Time Kernel","author":"Labrosse Jean","unstructured":"Jean Labrosse. 2002. MicroC\/OS-II: The Real Time Kernel. CRC Press."},{"key":"e_1_3_2_1_33_1","volume-title":"Proc. ACM Program. Lang. 7, OOPSLA","author":"Lattuada Andrea","year":"2023","unstructured":"Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types. Proc. ACM Program. Lang. 7, OOPSLA (2023)."},{"key":"e_1_3_2_1_34_1","volume-title":"18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"LeBlanc Hayley","year":"2024","unstructured":"Hayley LeBlanc, Nathan Taylor, James Bornholt, and Vijay Chidambaram. 2024. SquirrelFS: using the Rust compiler to check file-system crash consistency. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX."},{"key":"e_1_3_2_1_35_1","volume-title":"Proc. ACM Program. Lang. 7, PLDI, Article 169 (June","author":"Lehmann Nico","year":"2023","unstructured":"Nico Lehmann, Adam T. Geller, Niki Vazou, and Ranjit Jhala. 2023. Flux: Liquid Types for Rust. Proc. ACM Program. Lang. 7, PLDI, Article 169 (June 2023)."},{"key":"e_1_3_2_1_36_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR).","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)."},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the 26th Symposium on Operating Systems Principles.","author":"Levy Amit","year":"2017","unstructured":"Amit Levy, Bradford Campbell, Branden Ghena, Daniel B Giffin, Pat Pannuto, Prabal Dutta, and Philip Levis. 2017. Multiprogramming a 64kb computer safely and efficiently. In Proceedings of the 26th Symposium on Operating Systems Principles."},{"key":"e_1_3_2_1_38_1","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Li Shih-Wei","year":"2021","unstructured":"Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021. Formally verified memory protection for a commodity multiprocessor hypervisor. In 30th USENIX Security Symposium (USENIX Security 21)."},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the eighteenth international conference on Architectural support for programming languages and operating systems.","author":"Mai Haohui","year":"2013","unstructured":"Haohui Mai, Edgar Pek, Hui Xue, Samuel Talmadge King, and Parthasarathy Madhusudan. 2013. Verifying security invariants in ExpressOS. In Proceedings of the eighteenth international conference on Architectural support for programming languages and operating systems."},{"key":"e_1_3_2_1_40_1","volume-title":"Ruimin Sun, Engin Kirda, and Long Lu.","author":"Mera Alejandro","year":"2022","unstructured":"Alejandro Mera, Yi Hui Chen, Ruimin Sun, Engin Kirda, and Long Lu. 2022. D-box: DMA-enabled compartmentalization for embedded applications. arXiv preprint arXiv:2201.05199 (2022)."},{"key":"e_1_3_2_1_41_1","volume-title":"Automated Deduction-CADE 28: 28th International Conference on Automated Deduction, Virtual Event, 2021, Proceedings 28","author":"de Moura Leonardo","year":"2021","unstructured":"Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 theorem prover and programming language. In Automated Deduction-CADE 28: 28th International Conference on Automated Deduction, Virtual Event, 2021, Proceedings 28."},{"key":"e_1_3_2_1_42_1","volume-title":"Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP '19)","author":"Nelson Luke","year":"2019","unstructured":"Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. 2019. Scaling symbolic evaluation for automated verification of systems code with Serval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP '19). ACM."},{"key":"e_1_3_2_1_43_1","volume-title":"Proceedings of the 26th Symposium on Operating Systems Principles.","author":"Nelson Luke","year":"2017","unstructured":"Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. 2017. Hyperkernel: Push-button verification of an OS kernel. In Proceedings of the 26th Symposium on Operating Systems Principles."},{"key":"e_1_3_2_1_44_1","volume-title":"41st International Conference on Current Trends in Theory and Practice of Computer Science. Springer.","author":"Nemati Hamed","year":"2015","unstructured":"Hamed Nemati, Roberto Guanciale, and Mads Dam. 2015. Trustworthy virtualization of the ARMv7 memory subsystem. In 41st International Conference on Current Trends in Theory and Practice of Computer Science. Springer."},{"key":"e_1_3_2_1_45_1","volume-title":"Paulson","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic."},{"key":"e_1_3_2_1_46_1","article-title":"eWASM: Practical software fault isolation for reliable embedded devices","volume":"39","author":"Peach Gregor","year":"2020","unstructured":"Gregor Peach, Runyu Pan, Zhuoyi Wu, Gabriel Parmer, Christopher Haster, and Ludmila Cherkasova. 2020. eWASM: Practical software fault isolation for reliable embedded devices. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39, 11 (2020).","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"e_1_3_2_1_47_1","volume-title":"Trustworthy specifications of ARM v8-A and v8-M system level architecture. In 2016 Formal Methods in Computer-Aided Design (FMCAD)","author":"Reid Alastair","unstructured":"Alastair Reid. 2016. Trustworthy specifications of ARM v8-A and v8-M system level architecture. In 2016 Formal Methods in Computer-Aided Design (FMCAD). IEEE."},{"key":"e_1_3_2_1_48_1","unstructured":"Vivien Rindisbacher. 2024. Thread mode not set to privileged execution in certain ISRs. https:\/\/github.com\/tock\/tock\/issues\/4246 GitHub issue."},{"key":"e_1_3_2_1_49_1","unstructured":"Vivien Rindisbacher. 2025. App crashing allows potential sharing of kernel memory. https:\/\/github.com\/tock\/tock\/issues\/4371 GitHub issue."},{"key":"e_1_3_2_1_50_1","unstructured":"Vivien Rindisbacher. 2025. Cortex-M MPU: allo-cate_app_memory_region allows access to kernel grant memory. https:\/\/github.com\/tock\/tock\/issues\/4366 GitHub issue."},{"key":"e_1_3_2_1_51_1","unstructured":"Vivien Rindisbacher. 2025. Register clobbering in Generic ISR causes exception exit to return to process rather than Kernel. https:\/\/github.com\/tock\/tock\/issues\/4245 GitHub issue."},{"key":"e_1_3_2_1_52_1","unstructured":"Vivien Rindisbacher. 2025. Underflow in update_app_memory_regions. Private communication with Tock developers."},{"key":"e_1_3_2_1_53_1","unstructured":"Leon Schuermann. 2024. Call for Tock 2.2 Release Testing. https:\/\/github.com\/tock\/tock\/issues\/4272#issuecomment-2552364086 GitHub issue."},{"key":"e_1_3_2_1_54_1","volume-title":"Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification.","author":"Schuermann Leon","year":"2023","unstructured":"Leon Schuermann, Arun Thomas, and Amit Levy. 2023. Encapsulated Functions: Fortifying Rust's FFI in Embedded Systems. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification."},{"key":"e_1_3_2_1_55_1","volume-title":"Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation.","author":"Leck Sewell Thomas Arthur","year":"2013","unstructured":"Thomas Arthur Leck Sewell, Magnus O Myreen, and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation."},{"key":"e_1_3_2_1_56_1","volume-title":"International Conference on Security and Privacy in Communication Systems. Springer.","author":"Strackx Raoul","year":"2010","unstructured":"Raoul Strackx, Frank Piessens, and Bart Preneel. 2010. Efficient isolation of trusted subsystems in embedded systems. In International Conference on Security and Privacy in Communication Systems. Springer."},{"key":"e_1_3_2_1_57_1","volume-title":"Strom and Shaula Yemini","author":"Robert","year":"1986","unstructured":"Robert E. Strom and Shaula Yemini. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering SE-12, 1 (1986)."},{"key":"e_1_3_2_1_58_1","volume-title":"Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles.","author":"Tao Runzhou","year":"2021","unstructured":"Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, and Ronghui Gu. 2021. Formal verification of a multiprocessor hypervisor on arm relaxed memory hardware. In Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles."},{"key":"e_1_3_2_1_59_1","volume-title":"25th USENIX Security Symposium (USENIX Security 16)","author":"Vasudevan Amit","year":"2016","unstructured":"Amit Vasudevan, Sagar Chaki, Petros Maniatis, Limin Jia, and Anupam Datta. 2016. \u00fcberSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor. In 25th USENIX Security Symposium (USENIX Security 16)."},{"key":"e_1_3_2_1_60_1","unstructured":"Christof Windeck. 2024. Microsoft security controller Pluton is also coming to Intel Core. https:\/\/www.heise.de\/en\/news\/Microsoft-security-controller-Pluton-is-also-coming-to-Intel-Core-9833954.html."},{"key":"e_1_3_2_1_61_1","volume-title":"International Conference on Computer Aided Verification. Springer.","author":"Xu Fengwei","year":"2016","unstructured":"Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li. 2016. A practical verification framework for preemptive OS kernels. In International Conference on Computer Aided Verification. Springer."},{"key":"e_1_3_2_1_62_1","unstructured":"Ido Yariv. 2018. Potential Sharing of Kernel Memory. https:\/\/github.com\/tock\/tock\/issues\/1141 GitHub issue."},{"key":"e_1_3_2_1_63_1","volume-title":"Proceedings of the Ninth ACM International Conference on Embedded Software (EMSOFT '11)","author":"Zhao Lu","year":"2011","unstructured":"Lu Zhao, Guodong Li, Bjorn De Sutter, and John Regehr. 2011. ARMor: fully verified software fault isolation. In Proceedings of the Ninth ACM International Conference on Embedded Software (EMSOFT '11). ACM."},{"key":"e_1_3_2_1_64_1","volume-title":"Proceedings of the Seventeenth European Conference on Computer Systems.","author":"Zhou Xia","year":"2022","unstructured":"Xia Zhou, Jiaqi Li, Wenlong Zhang, Yajin Zhou, Wenbo Shen, and Kui Ren. 2022. OPEC: operation-based security isolation for bare-metal embedded systems. In Proceedings of the Seventeenth European Conference on Computer Systems."},{"key":"e_1_3_2_1_65_1","volume-title":"VeriSMo: A Verified Security Module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"Zhou Ziqiao","year":"2024","unstructured":"Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, and Weidong Cui. 2024. VeriSMo: A Verified Security Module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX."}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","location":"Lotte Hotel World Seoul Republic of Korea","acronym":"SOSP '25","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles"],"original-title":[],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:52:23Z","timestamp":1759323143000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3731569.3764856"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,12]]},"references-count":65,"alternative-id":["10.1145\/3731569.3764856","10.1145\/3731569"],"URL":"https:\/\/doi.org\/10.1145\/3731569.3764856","relation":{},"subject":[],"published":{"date-parts":[[2025,10,12]]},"assertion":[{"value":"2025-10-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}