{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:15:47Z","timestamp":1784232947871,"version":"3.55.0"},"reference-count":74,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1844964"],"award-info":[{"award-number":["1844964"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Virtual memory management (VMM) code is a critical piece of general-purpose OS kernels, but verification of this functionality is challenging due to the complexity of the hardware interface (the page tables are updated via writes to those memory locations, using addresses which are themselves virtualized). Prior work on verification of VMM code has either only handled a single address space, or trusted significant pieces of assembly code.<\/jats:p>\n                  <jats:p>In this paper, we introduce a modal abstraction to describe the truth of assertions relative to a specific virtual address space: [r]P indicating that P holds in the virtual address space rooted at r. Such modal assertions allow different address spaces to refer to each other, enabling complete verification of instruction sequences manipulating multiple address spaces. Using them effectively requires working with other assertions, such as points-to assertions about memory contents \u2014 which implicitly depend on the address space they are used in. We therefore define virtual points-to assertions to definitionally mimic hardware address translation, relative to a page table root. We demonstrate our approach with challenging fragments of VMM code showing that our approach handles examples beyond what prior work can address, including reasoning about a sequence of instructions as it changes address spaces. Our results are formalized for a RISC-like fragment of x86-64 assembly in Rocq.<\/jats:p>","DOI":"10.1145\/3763134","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"2338-2366","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Modal Abstractions for Virtualizing Memory Addresses"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5796-2150","authenticated-orcid":false,"given":"Ismail","family":"Kuru","sequence":"first","affiliation":[{"name":"Drexel University, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9012-4490","authenticated-orcid":false,"given":"Colin S.","family":"Gordon","sequence":"additional","affiliation":[{"name":"Drexel University, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_5"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_9"},{"key":"e_1_3_1_5_2","volume-title":"AMD64 Architecture Programmer's Manual,","author":"AMD","year":"2023","unstructured":"AMD. 2023. AMD64 Architecture Programmer's Manual,. Volume ,2: System Programming.Revision 3.40."},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.5555\/2670099"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.2307\/2695090"},{"key":"e_1_3_1_9_2","volume-title":"Handbook of Modal Logic.","author":"Areces Carlos","year":"2006","unstructured":"Carlos Areces and Balder ten Cate. 2006. Hybrid Logics. In Handbook of Modal Logic. Elsevier. https:\/\/carlosareces.github.io\/content\/papers\/files\/hml-arecestencate.pdf"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.27"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926401"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01049415"},{"key":"e_1_3_1_14_2","volume-title":"Handbook of Modal Logic.","author":"Blackburn Patrick","year":"2006","unstructured":"Patrick Blackburn and Johan van Benthem. 2006. Modal Logic: A Semantic Perspective. In Handbook of Modal Logic. Elsevier. https:\/\/carlosareces.github.io\/mll8\/downloads\/hb.pdf"},{"key":"e_1_3_1_15_2","volume-title":"USENIX summer","author":"Bonwick Jeff","year":"1994","unstructured":"Jeff Bonwick et al. 1994. The slab allocator: An object-caching kernel memory allocator.. In USENIX summer, 16. Boston, MA, USA."},{"key":"e_1_3_1_16_2","doi-asserted-by":"crossref","unstructured":"James Brotherston and Jules Villard. 2014. Parametric completeness for separation theories. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 453\u2013464.","DOI":"10.1145\/2535838.2535844"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000439"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677003"},{"key":"e_1_3_1_22_2","unstructured":"Christopher Clark Keir Fraser Steven Hand Jacob Gorm Hansen Eric Jul Christian Limpach Ian Pratt and Andrew Warfield. 2005. Live migration of virtual machines. In Proceedings of the 2nd Conference on Symposium on Networked Systems Design & Implementation-Volume 2 273\u2013286."},{"key":"e_1_3_1_23_2","volume-title":"Local Verification of Global Invariants in Concurrent Programs.","author":"Coehn Ernie","year":"2010","unstructured":"Ernie Coehn, Michal Moskal, Wolfram Shulte, and Stephan Tobies. 2010. Local Verification of Global Invariants in Concurrent Programs.Technical Report MSR-TR-2010-9. Microsoft Research."},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35843-2-1"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_23"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_3_1_29_2","doi-asserted-by":"crossref","unstructured":"Hoang-Hai Dang Jaehwang Jung Jaemin Choi Duc-Than Nguyen William Mansky Jeehoon Kang and Derek Dreyer. 2022. Compass: strong and compositional library specifications in relaxed memory separation logic. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 792\u2013808.","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_9"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/356571.356573"},{"key":"e_1_3_1_32_2","first-page":"150","volume-title":"PostProceedings of the 9th Inti. Conference on Types for Proofs and Programs (TYPES 2013)","author":"Despeyroux Jo\u0451lle","year":"2014","unstructured":"Jo\u0451lle Despeyroux and Kaustuv Chaudhuri. 2014. A hybrid linear logic for constrained transition systems. In PostProceedings of the 9th Inti. Conference on Types for Proofs and Programs (TYPES 2013), 26. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 150\u2013168."},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_3_1_35_2","volume-title":"Operating Systems in Depth: Design and Programming.","author":"Doeppner Thomas W.","year":"2010","unstructured":"Thomas W. Doeppner. 2010. Operating Systems in Depth: Design and Programming. Wiley."},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729311"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217953"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01054038"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00215625"},{"key":"e_1_3_1_40_2","doi-asserted-by":"crossref","unstructured":"Colin S Gordon. 2019. Modal assertions for actor correctness. In Proceedings of the 9th ACM SIGPLAN International Workshop on Programming Based on Actors Agents and Decentralized Control. 11\u201320.","DOI":"10.1145\/3358499.3361221"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_1_42_2","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 OSDI. 653\u2013669."},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_1_44_2","unstructured":"Mark Hillebrand. 2005. Address Spaces and Virtual Memory: Specification Implementation and Correctness. Ph. D. Dissertation. PhD thesis Saarland University Computer Science Dept."},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_46_2","doi-asserted-by":"crossref","unstructured":"Aquinas Hobor Robert Dockins and Andrew W Appel. 2010. A theory of indirection via approximation. In Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 171\u2013184.","DOI":"10.1145\/1706299.1706322"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/1272996.1273032"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/1243418.1243424"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_6"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_20"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","unstructured":"Ismail Kuru and Colin S Gordon. 2025. Modal Abstractions for Virtualizing Memory Addresses (Artifact). doi:10.5281\/zenodo.16896150","DOI":"10.5281\/zenodo.16896150"},{"key":"e_1_3_1_55_2","doi-asserted-by":"crossref","unstructured":"Ismail Kuru and Colin S Gordon. 2025. Modal Abstractions for Virtualizing Memory Addresses (Technical Report). Technical Report arXiv:2307.14471. arXiV.","DOI":"10.1145\/3763134"},{"key":"e_1_3_1_56_2","doi-asserted-by":"crossref","unstructured":"Ori Lahav Viktor Vafeiadis Jeehoon Kang Chung-Kil Hur and Derek Dreyer. 2017. Repairing sequential consistency in C\/C++ 11. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. 618\u2013632.","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132786"},{"key":"e_1_3_1_60_2","volume-title":"Solaris internals: Solaris 10 and OpenSolaris kernel architecture","author":"McDougall Richard","year":"2006","unstructured":"Richard McDougall and Jim Mauro. 2006. Solaris internals: Solaris 10 and OpenSolaris kernel architecture. Pearson Education."},{"key":"e_1_3_1_61_2","first-page":"108","volume-title":"Trustworthy Global Computing: Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers 3","year":"2008","unstructured":"Tom Murphy VII, Karl Crary, and Robert Harper. 2008. Type-safe distributed programming with ML5. In Trustworthy Global Computing: Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers 3. Springer, 108\u2013123."},{"key":"e_1_3_1_62_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_1_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111066"},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_15"},{"key":"e_1_3_1_65_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_1_66_2","first-page":"109","volume-title":"Foundations of Computer Science, 1976., 17th Annual Symposium on.","author":"Pratt Vaughan R","year":"1976","unstructured":"Vaughan R Pratt. 1976. Semantical consideration on Floyd-Hoare logic. In Foundations of Computer Science, 1976., 17th Annual Symposium on. IEEE, 109\u2013121."},{"key":"e_1_3_1_67_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_1_69_2","unstructured":"Artem Starostin. 2010. Formal verification of demand paging. Ph. D. Dissertation. PhD thesis Saarland University Computer Science Dept."},{"key":"e_1_3_1_70_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_32"},{"key":"e_1_3_1_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09539-7"},{"key":"e_1_3_1_72_2","unstructured":"Michael von Tessin. 2013. The clustered multikernel: An approach to formal verification of multiprocessor operating-system kernels. Ph. D. Dissertation. PhD thesis School of Computer Science and Engineering UNSW Sydney Australia . Sydney Australia"},{"key":"e_1_3_1_73_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689755"},{"key":"e_1_3_1_74_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_32"},{"key":"e_1_3_1_75_2","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763134","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763134","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:12:29Z","timestamp":1784196749000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763134"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":74,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763134"],"URL":"https:\/\/doi.org\/10.1145\/3763134","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}