{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:57:26Z","timestamp":1771703846657,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":69,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,3,30]],"date-time":"2025-03-30T00:00:00Z","timestamp":1743292800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Natural Sciences and Engineering Research Council of Canada NSERC","award":["C150-2017-0016"],"award-info":[{"award-number":["C150-2017-0016"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,3,30]]},"DOI":"10.1145\/3676641.3711998","type":"proceedings-article","created":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T16:47:32Z","timestamp":1743094052000},"page":"1365-1381","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["<i>Velosiraptor<\/i>\n            : Code Synthesis for Memory Translation"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3263-7236","authenticated-orcid":false,"given":"Reto","family":"Achermann","sequence":"first","affiliation":[{"name":"University of British Columbia, Vancouver, BC, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-6673-4945","authenticated-orcid":false,"given":"Em","family":"Chu","sequence":"additional","affiliation":[{"name":"JuliaHub, Boston, MA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-0559-4820","authenticated-orcid":false,"given":"Ryan","family":"Mehri","sequence":"additional","affiliation":[{"name":"Replit, San Francisco, CA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-6594-0359","authenticated-orcid":false,"given":"Ilias","family":"Karimalis","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, BC, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2165-4658","authenticated-orcid":false,"given":"Margo","family":"Seltzer","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, BC, Canada"}]}],"member":"320","published-online":{"date-parts":[[2025,3,30]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477113.3487270"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458336.3465273"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.244.4"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_1"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3593856.3595895"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3079856.3080209"},{"key":"e_1_3_2_1_7_1","unstructured":"Arm Ltd. 2016. Introduction to PAC. Online. https: \/\/developer.arm.com\/documentation\/109576\/0100\/Pointer-Authentication-Code\/Introduction-to-PAC."},{"key":"e_1_3_2_1_8_1","unstructured":"Arm Ltd. 2019. Armv8.5-A - Memory Tagging Extension. White Paper."},{"key":"e_1_3_2_1_9_1","unstructured":"Arm Ltd. 2023. LISA+ Language for Fast Models Reference Manual. https:\/\/developer.arm.com\/documentation\/101092\/0100 Version 1.0.."},{"key":"e_1_3_2_1_10_1","volume-title":"Fast Models: SoC Verification Without Hardware. Online. https:\/\/www.arm.com\/products\/development-tools\/simulation\/fast-models.","author":"Ltd Arm","year":"2024","unstructured":"Arm Ltd. 2024. Fast Models: SoC Verification Without Hardware. Online. https:\/\/www.arm.com\/products\/development-tools\/simulation\/fast-models."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660350"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2016.23009"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945462"},{"key":"e_1_3_2_1_14_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2021. The SMT-LIB Standard. https:\/\/smt-lib.org\/papers\/smt-lib-reference-v2.6-r2021-05-12.pdf Version 2.6."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508148.2485943"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629579"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3593856.3595899"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/RSP.2014.6966689"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1346281.1346284"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the 27th USENIX Conference on Security Symposium","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 Proceedings of the 27th USENIX Conference on Security Symposium (Baltimore, MD, USA) (SEC'18). USENIX Association, USA, 65--82."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.26"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294295"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640398"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694386"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.micpro.2021.104377"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3625275.3625400"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3593856.3595903"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582016.3582021"},{"key":"e_1_3_2_1_30_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 Ker- nels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). USENIX Association, Savannah, GA, 653--669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/ presentation\/gu"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451146"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563943"},{"key":"e_1_3_2_1_33_1","volume-title":"26th USENIX Security Symposium (USENIX Security 17)","author":"Hua Zhichao","year":"2017","unstructured":"Zhichao Hua, Jinyu Gu, Yubin Xia, Haibo Chen, Binyu Zang, and Haibing Guan. 2017. vTZ: Virtualizing ARM TrustZone. In 26th USENIX Security Symposium (USENIX Security 17). USENIX Associa- tion, Vancouver, BC, 541--556. https:\/\/www.usenix.org\/conference\/ usenixsecurity17\/technical-sessions\/presentation\/hua"},{"key":"e_1_3_2_1_34_1","volume-title":"Proceedings of the 2016 USENIX Conference on Usenix Annual Technical Conference (Denver, CO, USA) (USENIX ATC '16). USENIX Association","author":"Huang Jian","year":"2016","unstructured":"Jian Huang, Moinuddin K. Qureshi, and Karsten Schwan. 2016. An Evolutionary Study of Linux Memory Management for Fun and Profit. In Proceedings of the 2016 USENIX Conference on Usenix Annual Technical Conference (Denver, CO, USA) (USENIX ATC '16). USENIX Association, Berkeley, CA, USA, 465--478. http:\/\/dl.acm.org\/citation.cfm?id=3026959.3027002"},{"key":"e_1_3_2_1_35_1","unstructured":"Integrated Device Technology Inc. 1995. IDT79R4600 TM and IDT79R4700 TM RISC Processor Hardware User's Manual (revision 2.0 ed.). https:\/\/docslib.org\/doc\/718203\/idt79r4600-and-idt79r4700-risc-processor-hardware-users-manual"},{"key":"e_1_3_2_1_36_1","unstructured":"Intel Corp. 2013. Intel Xeon Phi Coprocessor Developer's Quick Start Guide. https:\/\/www.intel.com\/content\/dam\/develop\/external\/us\/en\/documents\/intel-xeon-phi-coprocessor-quick-start-developers-guide.pdf Version 1.8."},{"key":"e_1_3_2_1_37_1","volume-title":"Intel 64 and IA-32 Architectures Software Developer's Manual. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/intel-sdm.html","author":"Intel Corp. 2023.","year":"2023","unstructured":"Intel Corp. 2023. Intel 64 and IA-32 Architectures Software Developer's Manual. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/intel-sdm.html December 2023."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179285"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","volume":"3","author":"Landgraf Joshua","year":"2023","unstructured":"Joshua Landgraf, Matthew Giordano, Esther Yoon, and Christopher J. Rossbach. 2023. Reconfigurable Virtual Memory for FPGA-Driven I\/O. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3 (Vancouver, BC, Canada) (ASPLOS 2023). Association for Computing Machinery, New York, NY, USA, 556--571. https:\/\/doi.org\/10.1145\/ 3582016.3582048"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695952"},{"key":"e_1_3_2_1_42_1","first-page":"3953","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). USENIX Association, 3953-3970. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/li-shih-wei"},{"key":"e_1_3_2_1_43_1","volume-title":"Design and Verification of the Arm Confidential Compute Architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Li Xupeng","year":"2022","unstructured":"Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, and Gareth Stockwell. 2022. Design and Verification of the Arm Confidential Compute Architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, Carlsbad, CA, 465--484. https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/li"},{"key":"e_1_3_2_1_44_1","unstructured":"Berenice Mann. 2018. New Secure world architecture in Armv8.4. Online. https:\/\/community.arm.com\/arm-community-blogs\/b\/architectures-and-processors-blog\/posts\/architecting-more- secure-world-with-isolation-and-virtualization."},{"key":"e_1_3_2_1_45_1","volume-title":"Thunderclap: Exploring Vulnerabilities in Operating Sys- tem IOMMU Protection via DMA from Untrustworthy Peripherals. In NDSS.","author":"Markettos A Theodore","year":"2019","unstructured":"A Theodore Markettos, Colin Rothwell, Brett F Gutstein, Allison Pearce, Peter G Neumann, Simon W Moore, and Robert NM Watson. 2019. Thunderclap: Exploring Vulnerabilities in Operating Sys- tem IOMMU Protection via DMA from Untrustworthy Peripherals. In NDSS."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872379"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2022.24026"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/LADC.2016.31"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1186\/s13173-017-0066-7"},{"key":"e_1_3_2_1_50_1","unstructured":"National Vulnerability Database. 2014. CVE-2014-9888. Online.https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2014-9888."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"crossref","unstructured":"National Vulnerability Database. 2017. CVE-2017-16994. Online. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2017-16994.","DOI":"10.5465\/AMBPP.2017.16994abstract"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00041"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/36206.36181"},{"key":"e_1_3_2_1_55_1","unstructured":"Alastair Reid. 2016. ARM's Architecture Specification Language. Online. https:\/\/alastairreid.github.io\/specification_languages\/."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/3077629.3077658"},{"key":"e_1_3_2_1_57_1","unstructured":"Alastair Reid. 2020. Using ASLi with Arm's v8.6-A ISA specification. Online. https:\/\/alastairreid.github.io\/using-asli\/."},{"key":"e_1_3_2_1_58_1","unstructured":"Timothy Roscoe and Barrelfish Projec. [n. d.]. Mackerel User Guide - Barrelfish Technical Note 2."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629583"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.5555\/2685048.2685101"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294294"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2017.23455"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2016.23218"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.9"},{"key":"e_1_3_2_1_65_1","unstructured":"The kernel development community. 2024. Paravirt_ops. The Linux Kernel Organization. https:\/\/www.kernel.org\/doc\/html\/latest\/virt\/paravirt_ops.html"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3623759.3624545"},{"key":"e_1_3_2_1_67_1","volume-title":"Proceedings of the 2015 USENIX Conference on Usenix Annual Technical Conference (Santa Clara, CA) (USENIX ATC '15). USENIX Association, USA, 347--360","author":"Wang Xiaoguang","year":"2015","unstructured":"Xiaoguang Wang, Yue Chen, Zhi Wang, Yong Qi, and Yajin Zhou. 2015. SecPod: a framework for virtualization-based security systems. In Proceedings of the 2015 USENIX Conference on Usenix Annual Technical Conference (Santa Clara, CA) (USENIX ATC '15). USENIX Association, USA, 347--360."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095810.1095814"}],"event":{"name":"ASPLOS '25: 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Rotterdam Netherlands","acronym":"ASPLOS '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGOPS ACM Special Interest Group on Operating Systems","SIGARCH ACM Special Interest Group on Computer Architecture"]},"container-title":["Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676641.3711998","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3676641.3711998","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T11:07:17Z","timestamp":1755774437000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676641.3711998"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,30]]},"references-count":69,"alternative-id":["10.1145\/3676641.3711998","10.1145\/3676641"],"URL":"https:\/\/doi.org\/10.1145\/3676641.3711998","relation":{},"subject":[],"published":{"date-parts":[[2025,3,30]]},"assertion":[{"value":"2025-03-30","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}