{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T01:16:04Z","timestamp":1777338964350,"version":"3.51.4"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++.  \nUnfortunately, memory-unsafe C code remains unsafe when compiled to Wasm\u2014and attackers can exploit  \nbuffer overflows and use-after-frees in Wasm almost as easily as they can on native platforms. Memory-  \nSafe WebAssembly (MSWasm) proposes to extend Wasm with language-level memory-safety abstractions to  \nprecisely address this problem. In this paper, we build on the original MSWasm position paper to realize this vision. We give a precise and formal semantics of MSWasm, and prove that well-typed MSWasm programs are, by construction, robustly memory safe. To this end, we develop a novel, language-independent memory-safety property based on colored memory locations and pointers. This property also lets us reason about the security guarantees of a formal C-to-MSWasm compiler\u2014and prove that it always produces memory-safe programs (and preserves the semantics of safe programs). We use these formal results to then guide several implementations: Two compilers of MSWasm to native code, and a C-to-MSWasm compiler (that extends Clang). Our MSWasm compilers support different enforcement mechanisms, allowing developers to make security-performance trade-offs according to their needs. Our evaluation shows that on the PolyBenchC suite, the overhead of enforcing memory safety in software ranges from 22% (enforcing spatial safety alone) to 198% (enforcing full memory safety), and 51.7% when using hardware memory capabilities for spatial safety and pointer integrity.<\/jats:p>\n          <jats:p>More importantly, MSWasm\u2019s design makes it easy to swap between enforcement mechanisms; as fast (especially hardware-based) enforcement techniques become available, MSWasm will be able to take advantage of these advances almost for free.<\/jats:p>","DOI":"10.1145\/3571208","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"425-454","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0305-5424","authenticated-orcid":false,"given":"Alexandra E.","family":"Michael","sequence":"first","affiliation":[{"name":"University of California at San Diego, USA \/ University of Washington, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0861-1418","authenticated-orcid":false,"given":"Anitha","family":"Gollamudi","sequence":"additional","affiliation":[{"name":"University of Massachusetts Lowell, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5596-6828","authenticated-orcid":false,"given":"Jay","family":"Bosamiya","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1784-4512","authenticated-orcid":false,"given":"Evan","family":"Johnson","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA \/ Arm, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5517-0045","authenticated-orcid":false,"given":"Aidan","family":"Denlinger","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4358-2963","authenticated-orcid":false,"given":"Craig","family":"Disselkoen","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0596-877X","authenticated-orcid":false,"given":"Conrad","family":"Watt","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9113-1684","authenticated-orcid":false,"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3411-9678","authenticated-orcid":false,"given":"Marco","family":"Patrignani","sequence":"additional","affiliation":[{"name":"University of Trento, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4795-0236","authenticated-orcid":false,"given":"Marco","family":"Vassena","sequence":"additional","affiliation":[{"name":"Utrecht University, Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7041-7464","authenticated-orcid":false,"given":"Deian","family":"Stefan","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In 2019 IEEE 32th Computer Security Foundations Symposium (CSF","author":"Abate Carmine","year":"2019","unstructured":"Carmine Abate , Roberto Blanco , Deepak Garg , C\u0103t\u0103lin Hri\u0163cu , Marco Patrignani , and J\u00e9r\u00e9my Thibault . 2019 . Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In 2019 IEEE 32th Computer Security Foundations Symposium (CSF 2019). Carmine Abate, Roberto Blanco, Deepak Garg, C\u0103t\u0103lin Hri\u0163cu, Marco Patrignani, and J\u00e9r\u00e9my Thibault. 2019. Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In 2019 IEEE 32th Computer Security Foundations Symposium (CSF 2019)."},{"key":"e_1_2_1_2_1","volume-title":"USENIX Security Symposium. 10","author":"Akritidis Periklis","year":"2009","unstructured":"Periklis Akritidis , Manuel Costa , Miguel Castro , and Steven Hand . 2009 . Baggy Bounds Checking: An Efficient and Backwards-Compatible Defense against Out-of-Bounds Errors . In USENIX Security Symposium. 10 . Periklis Akritidis, Manuel Costa, Miguel Castro, and Steven Hand. 2009. Baggy Bounds Checking: An Efficient and Backwards-Compatible Defense against Out-of-Bounds Errors. In USENIX Security Symposium. 10."},{"key":"e_1_2_1_3_1","unstructured":"Arm. 2019. Armv8.5-A Memory Tagging Extension. White Paper. \t\t\t\t  Arm. 2019. Armv8.5-A Memory Tagging Extension. White Paper."},{"key":"e_1_2_1_4_1","unstructured":"2022. Arm Morello Program. https:\/\/www.arm.com\/architecture\/cpu\/morello \t\t\t\t  2022. Arm Morello Program. https:\/\/www.arm.com\/architecture\/cpu\/morello"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178446"},{"key":"e_1_2_1_6_1","volume-title":"Pierce","author":"de Amorim Arthur Azevedo","year":"2018","unstructured":"Arthur Azevedo de Amorim , C\u0103t\u0103lin Hri\u0163cu , and Benjamin C . Pierce . 2018 . The Meaning of Memory Safety. In Principles of Security and Trust, Lujo Bauer and Ralf K\u00fcsters (Eds.). Springer International Publishing , Cham. 79\u2013105. isbn:978-3-319-89722-6 Arthur Azevedo de Amorim, C\u0103t\u0103lin Hri\u0163cu, and Benjamin C. Pierce. 2018. The Meaning of Memory Safety. In Principles of Security and Trust, Lujo Bauer and Ralf K\u00fcsters (Eds.). Springer International Publishing, Cham. 79\u2013105. isbn:978-3-319-89722-6"},{"key":"e_1_2_1_7_1","volume-title":"USENIX Security Symposium.","author":"Bosamiya Jay","year":"2022","unstructured":"Jay Bosamiya , Wen Shih Lim , and Bryan Parno . 2022 . Provably-Safe Multilingual Software Sandboxing using WebAssembly . In USENIX Security Symposium. Jay Bosamiya, Wen Shih Lim, and Bryan Parno. 2022. Provably-Safe Multilingual Software Sandboxing using WebAssembly. In USENIX Security Symposium."},{"key":"e_1_2_1_8_1","unstructured":"CTSRD-CHERI. 2022. The CHERI LLVM Compiler Infrastructure. https:\/\/github.com\/CTSRD-CHERI\/llvm-project \t\t\t\t  CTSRD-CHERI. 2022. The CHERI LLVM Compiler Infrastructure. https:\/\/github.com\/CTSRD-CHERI\/llvm-project"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.55"},{"key":"e_1_2_1_10_1","volume-title":"Oscar: A Practical page-permissions-based scheme for thwarting dangling pointers. In USENIX Security.","author":"Dang Thurston HY","year":"2017","unstructured":"Thurston HY Dang , Petros Maniatis , and David Wagner . 2017 . Oscar: A Practical page-permissions-based scheme for thwarting dangling pointers. In USENIX Security. Thurston HY Dang, Petros Maniatis, and David Wagner. 2017. Oscar: A Practical page-permissions-based scheme for thwarting dangling pointers. In USENIX Security."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems. ACM","author":"Devietti Joe","year":"2008","unstructured":"Joe Devietti , Colin Blundell , Milo M. K. Martin , and Steve Zdancewic . 2008 . Hardbound: Architectural Support for Spatial Safety of the C Programming Language . In Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems. ACM , New York, NY, USA. Joe Devietti, Colin Blundell, Milo M. K. Martin, and Steve Zdancewic. 2008. Hardbound: Architectural Support for Spatial Safety of the C Programming Language. In Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems. ACM, New York, NY, USA."},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 8th International Workshop on Hardware and Architectural Support for Security and Privacy. ACM.","author":"Disselkoen Craig","year":"2019","unstructured":"Craig Disselkoen , John Renner , Conrad Watt , Tal Garfinkel , Amit Levy , and Deian Stefan . 2019 . Position Paper: Progressive Memory Safety for WebAssembly . In Proceedings of the 8th International Workshop on Hardware and Architectural Support for Security and Privacy. ACM. Craig Disselkoen, John Renner, Conrad Watt, Tal Garfinkel, Amit Levy, and Deian Stefan. 2019. Position Paper: Progressive Memory Safety for WebAssembly. In Proceedings of the 8th International Workshop on Hardware and Architectural Support for Security and Privacy. ACM."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00098"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 21st International Middleware Conference (Middleware \u201920)","author":"Gadepalli Phani Kishore","year":"2020","unstructured":"Phani Kishore Gadepalli , Sean McBride , Gregor Peach , Ludmila Cherkasova , and Gabriel Parmer . 2020 . Sledge: A Serverless-First, Light-Weight Wasm Runtime for the Edge . In Proceedings of the 21st International Middleware Conference (Middleware \u201920) . ACM. Phani Kishore Gadepalli, Sean McBride, Gregor Peach, Ludmila Cherkasova, and Gabriel Parmer. 2020. Sledge: A Serverless-First, Light-Weight Wasm Runtime for the Edge. In Proceedings of the 21st International Middleware Conference (Middleware \u201920). ACM."},{"key":"e_1_2_1_15_1","unstructured":"Richard Grisenthwaite. 2019. Supporting the UK in becoming a leading global player in cybersecurity. https:\/\/community.arm.com\/blog\/company\/b\/blog\/posts\/supporting-the-uk-in-becoming-a-leading-global-player-in-cybersecurity \t\t\t\t  Richard Grisenthwaite. 2019. Supporting the UK in becoming a leading global player in cybersecurity. https:\/\/community.arm.com\/blog\/company\/b\/blog\/posts\/supporting-the-uk-in-becoming-a-leading-global-player-in-cybersecurity"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062363"},{"key":"e_1_2_1_18_1","volume-title":"Conference on Computer and Communications Security. ACM.","author":"Haller Istvan","year":"2016","unstructured":"Istvan Haller , Yuseok Jeon , Hui Peng , Mathias Payer , Cristiano Giuffrida , Herbert Bos , and Erik Van Der Kouwe . 2016 . TypeSan: Practical type confusion detection . In Conference on Computer and Communications Security. ACM. Istvan Haller, Yuseok Jeon, Hui Peng, Mathias Payer, Cristiano Giuffrida, Herbert Bos, and Erik Van Der Kouwe. 2016. TypeSan: Practical type confusion detection. In Conference on Computer and Communications Security. ACM."},{"key":"e_1_2_1_19_1","unstructured":"Michael Hicks. 2014. What is memory safety? http:\/\/www.pl-enthusiast.net\/2014\/07\/21\/memory-safety\/ \t\t\t\t  Michael Hicks. 2014. What is memory safety? http:\/\/www.pl-enthusiast.net\/2014\/07\/21\/memory-safety\/"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Aaron Hilbig Daniel Lehmann and Michael Pradel. 2021. An Empirical Study of Real-World WebAssembly Binaries: Security Languages Use Cases. ACM. \t\t\t\t  Aaron Hilbig Daniel Lehmann and Michael Pradel. 2021. An Empirical Study of Real-World WebAssembly Binaries: Security Languages Use Cases. ACM.","DOI":"10.1145\/3442381.3450138"},{"key":"e_1_2_1_21_1","volume-title":"Native Code. In 2019 USENIX Annual Technical Conference (USENIX ATC 19)","author":"Jangda Abhinav","year":"2019","unstructured":"Abhinav Jangda , Bobby Powers , Emery D. Berger , and Arjun Guha . 2019 . Not So Fast: Analyzing the Performance of WebAssembly vs . Native Code. In 2019 USENIX Annual Technical Conference (USENIX ATC 19) . USENIX Association. Abhinav Jangda, Bobby Powers, Emery D. Berger, and Arjun Guha. 2019. Not So Fast: Analyzing the Performance of WebAssembly vs. Native Code. In 2019 USENIX Annual Technical Conference (USENIX ATC 19). USENIX Association."},{"key":"e_1_2_1_22_1","volume-title":"Cyclone: A Safe Dialect of C. In 2002 USENIX Annual Technical Conference (USENIX ATC 02)","author":"Jim Trevor","year":"2002","unstructured":"Trevor Jim , Greg Morrisett , Dan Grossman , Michael Hicks , James Cheney , and Yanling Wang . 2002 . Cyclone: A Safe Dialect of C. In 2002 USENIX Annual Technical Conference (USENIX ATC 02) . USENIX Association. Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A Safe Dialect of C. In 2002 USENIX Annual Technical Conference (USENIX ATC 02). USENIX Association."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the Thirteenth EuroSys Conference. ACM.","author":"Kroes Taddeus","unstructured":"Taddeus Kroes , Koen Koning , Erik van der Kouwe, Herbert Bos, and Cristiano Giuffrida. 2018. Delta Pointers: Buffer Overflow Checks without the Checks . In Proceedings of the Thirteenth EuroSys Conference. ACM. Taddeus Kroes, Koen Koning, Erik van der Kouwe, Herbert Bos, and Cristiano Giuffrida. 2018. Delta Pointers: Buffer Overflow Checks without the Checks. In Proceedings of the Thirteenth EuroSys Conference. ACM."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516713"},{"key":"e_1_2_1_25_1","volume-title":"Preventing Use-after-free with Dangling Pointers Nullification","author":"Lee Byoungyoung","year":"2015","unstructured":"Byoungyoung Lee , Chengyu Song , Yeongjin Jang , Tielei Wang , Taesoo Kim , Long Lu , and Wenke Lee . 2015. Preventing Use-after-free with Dangling Pointers Nullification .. In NDSS. The Internet Society . http:\/\/dblp.uni-trier.de\/db\/conf\/ndss\/ndss 2015 .html##LeeSJWKLL15 Byoungyoung Lee, Chengyu Song, Yeongjin Jang, Tielei Wang, Taesoo Kim, Long Lu, and Wenke Lee. 2015. Preventing Use-after-free with Dangling Pointers Nullification.. In NDSS. The Internet Society. http:\/\/dblp.uni-trier.de\/db\/conf\/ndss\/ndss2015.html##LeeSJWKLL15"},{"key":"e_1_2_1_26_1","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Lehmann Daniel","year":"2020","unstructured":"Daniel Lehmann , Johannes Kinder , and Michael Pradel . 2020 . Everything Old is New Again: Binary Security of WebAssembly . In 29th USENIX Security Symposium (USENIX Security 20) . USENIX Association. Daniel Lehmann, Johannes Kinder, and Michael Pradel. 2020. Everything Old is New Again: Binary Security of WebAssembly. In 29th USENIX Security Symposium (USENIX Security 20). USENIX Association."},{"key":"e_1_2_1_27_1","volume-title":"Cryptographic Capability Computing. In IEEE\/ACM International Symposium on Microarchitecture. ACM.","author":"LeMay Michael","year":"2021","unstructured":"Michael LeMay , Joydeep Rakshit , Sergej Deutsch , David M Durham , Santosh Ghosh , Anant Nori , Jayesh Gaur , Andrew Weiler , Salmin Sultana , and Karanvir Grewal . 2021 . Cryptographic Capability Computing. In IEEE\/ACM International Symposium on Microarchitecture. ACM. Michael LeMay, Joydeep Rakshit, Sergej Deutsch, David M Durham, Santosh Ghosh, Anant Nori, Jayesh Gaur, Andrew Weiler, Salmin Sultana, and Karanvir Grewal. 2021. Cryptographic Capability Computing. In IEEE\/ACM International Symposium on Microarchitecture. ACM."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_1_29_1","volume-title":"28th USENIX Security Symposium (USENIX Security 19)","author":"Liljestrand Hans","unstructured":"Hans Liljestrand , Thomas Nyman , Kui Wang , Carlos Chinea Perez , Jan-Erik Ekberg , and N. Asokan . 2019. PAC it up: Towards Pointer Integrity using ARM Pointer Authentication . In 28th USENIX Security Symposium (USENIX Security 19) . USENIX Association. Hans Liljestrand, Thomas Nyman, Kui Wang, Carlos Chinea Perez, Jan-Erik Ekberg, and N. Asokan. 2019. PAC it up: Towards Pointer Integrity using ARM Pointer Authentication. In 28th USENIX Security Symposium (USENIX Security 19). USENIX Association."},{"key":"e_1_2_1_30_1","volume-title":"Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing. Principles of Secure Compilation (PriSC).","author":"McMullen Tyler","year":"2020","unstructured":"Tyler McMullen . 2020 . Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing. Principles of Secure Compilation (PriSC). Tyler McMullen. 2020. Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing. Principles of Secure Compilation (PriSC)."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2980983.2908081","article-title":"Into the Depths of C","volume":"51","author":"Memarian Kayvan","year":"2016","unstructured":"Kayvan Memarian , Justus Matthiesen , James Lingard , Kyndylan Nienhuis , David Chisnall , Robert N. M. Watson , and Peter Sewell . 2016 . Into the Depths of C : Elaborating the de Facto Standards. SIGPLAN Not. , 51 , 6 (2016), June , 1 \u2013 15 . Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson, and Peter Sewell. 2016. Into the Depths of C: Elaborating the de Facto Standards. SIGPLAN Not., 51, 6 (2016), June, 1\u201315.","journal-title":"Elaborating the de Facto Standards. SIGPLAN Not."},{"key":"e_1_2_1_34_1","unstructured":"MSWasm. [n.d.]. Memory-Safe WebAssembly. https:\/\/mswasm.programming.systems \t\t\t\t  MSWasm. [n.d.]. Memory-Safe WebAssembly. https:\/\/mswasm.programming.systems"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3554344"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1543135.1542504"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1837855.1806657"},{"key":"e_1_2_1_38_1","volume-title":"Retrofitting Fine Grain Isolation in the Firefox Renderer. In 29th USENIX Security Symposium (USENIX Security 20)","author":"Narayan Shravan","year":"2020","unstructured":"Shravan Narayan , Craig Disselkoen , Tal Garfinkel , Nathan Froyd , Eric Rahm , Sorin Lerner , Hovav Shacham , and Deian Stefan . 2020 . Retrofitting Fine Grain Isolation in the Firefox Renderer. In 29th USENIX Security Symposium (USENIX Security 20) . USENIX Association. Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, and Deian Stefan. 2020. Retrofitting Fine Grain Isolation in the Firefox Renderer. In 29th USENIX Security Symposium (USENIX Security 20). USENIX Association."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065887.1065892"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3224423"},{"key":"e_1_2_1_41_1","volume-title":"Smashing the stack for fun and profit. Phrack magazine, 7, 49","author":"One Aleph","year":"1996","unstructured":"Aleph One . 1996. Smashing the stack for fun and profit. Phrack magazine, 7, 49 ( 1996 ), 14\u201316. Aleph One. 1996. Smashing the stack for fun and profit. Phrack magazine, 7, 49 (1996), 14\u201316."},{"key":"e_1_2_1_42_1","unstructured":"Oracle. 2021. GraalVM. https:\/\/www.graalvm.org\/ \t\t\t\t  Oracle. 2021. GraalVM. https:\/\/www.graalvm.org\/"},{"key":"e_1_2_1_43_1","unstructured":"Oracle. 2021. Truffle Language Implementation Framework. https:\/\/www.graalvm.org\/22.0\/graalvm-as-a-platform\/language-implementation-framework\/ \t\t\t\t  Oracle. 2021. Truffle Language Implementation Framework. https:\/\/www.graalvm.org\/22.0\/graalvm-as-a-platform\/language-implementation-framework\/"},{"key":"e_1_2_1_44_1","volume-title":"Project Snowflake: Non-blocking safe manual memory management in .NET. Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/project-snowflake-non-blocking-safe-manual-memory-management-net\/","author":"Parkinson Matthew","year":"2017","unstructured":"Matthew Parkinson , Kapil Vaswani , Dimitrios Vytiniotis , Manuel Costa , Pantazis Deligiannis , Aaron Blankstein , Dylan McDermott , and Jonathan Balkind . 2017 . Project Snowflake: Non-blocking safe manual memory management in .NET. Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/project-snowflake-non-blocking-safe-manual-memory-management-net\/ Matthew Parkinson, Kapil Vaswani, Dimitrios Vytiniotis, Manuel Costa, Pantazis Deligiannis, Aaron Blankstein, Dylan McDermott, and Jonathan Balkind. 2017. Project Snowflake: Non-blocking safe manual memory management in .NET. Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/project-snowflake-non-blocking-safe-manual-memory-management-net\/"},{"key":"e_1_2_1_45_1","volume-title":"Concurrent Checking of Pointer and Array Accesses in C Programs. Softw. Pract. Exper., 27, 1","author":"Patil Harish","year":"1997","unstructured":"Harish Patil and Charles Fischer . 1997. Low-Cost , Concurrent Checking of Pointer and Array Accesses in C Programs. Softw. Pract. Exper., 27, 1 ( 1997 ), jan, 87\u2013110. issn:0038-0644 Harish Patil and Charles Fischer. 1997. Low-Cost, Concurrent Checking of Pointer and Array Accesses in C Programs. Softw. Pract. Exper., 27, 1 (1997), jan, 87\u2013110. issn:0038-0644"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.3012647"},{"key":"e_1_2_1_47_1","unstructured":"Louis-Noel Pouchet. 2011. PolyBench-C: the Polyhedral Benchmark suite. https:\/\/web.cs.ucla.edu\/ pouchet\/software\/polybench\/ \t\t\t\t  Louis-Noel Pouchet. 2011. PolyBench-C: the Polyhedral Benchmark suite. https:\/\/web.cs.ucla.edu\/ pouchet\/software\/polybench\/"},{"key":"e_1_2_1_48_1","unstructured":"Aleksandar Prokopec. 2019. Announcing GraalWasm \u2013 a WebAssembly engine in GraalVM. https:\/\/medium.com\/graalvm\/announcing-graalwasm-a-webassembly-engine-in-graalvm-25cd0400a7f2 \t\t\t\t  Aleksandar Prokopec. 2019. Announcing GraalWasm \u2013 a WebAssembly engine in GraalVM. https:\/\/medium.com\/graalvm\/announcing-graalwasm-a-webassembly-engine-in-graalvm-25cd0400a7f2"},{"key":"e_1_2_1_49_1","volume-title":"Principles of Security and Trust","author":"Ruef Andrew","unstructured":"Andrew Ruef , Leonidas Lampropoulos , Ian Sweet , David Tarditi , and Michael Hicks . 2019. Achieving Safety Incrementally with Checked C . In Principles of Security and Trust . Springer . Andrew Ruef, Leonidas Lampropoulos, Ian Sweet, David Tarditi, and Michael Hicks. 2019. Achieving Safety Incrementally with Checked C. In Principles of Security and Trust. Springer."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/353323.353382"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.13"},{"key":"e_1_2_1_52_1","volume-title":"Principles and Implementation Techniques of Software-Based Fault Isolation. 1","author":"Tan Gang","unstructured":"Gang Tan . 2017. Principles and Implementation Techniques of Software-Based Fault Isolation. 1 , Now Publishers Inc .. Gang Tan. 2017. Principles and Implementation Techniques of Software-Based Fault Isolation. 1, Now Publishers Inc.."},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the Fourteenth ACM Symposium on Operating Systems Principles (SOSP \u201993)","author":"Wahbe Robert","unstructured":"Robert Wahbe , Steven Lucco , Thomas E. Anderson , and Susan L. Graham . 1993. Efficient Software-based Fault Isolation . In Proceedings of the Fourteenth ACM Symposium on Operating Systems Principles (SOSP \u201993) . ACM. Robert Wahbe, Steven Lucco, Thomas E. Anderson, and Susan L. Graham. 1993. Efficient Software-based Fault Isolation. In Proceedings of the Fourteenth ACM Symposium on Operating Systems Principles (SOSP \u201993). ACM."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"e_1_2_1_55_1","unstructured":"WebAssembly. [n.d.]. WebAssembly System Interface. https:\/\/github.com\/WebAssembly\/wasi \t\t\t\t  WebAssembly. [n.d.]. WebAssembly System Interface. https:\/\/github.com\/WebAssembly\/wasi"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358288"},{"key":"e_1_2_1_57_1","volume-title":"Proceedings of the 12th ACM SIGSOFT Twelfth International Symposium on Foundations of Software Engineering. ACM.","author":"Xu Wei","unstructured":"Wei Xu , Daniel C. DuVarney , and R. Sekar . 2004. An Efficient and Backwards-Compatible Transformation to Ensure Memory Safety of C Programs . In Proceedings of the 12th ACM SIGSOFT Twelfth International Symposium on Foundations of Software Engineering. ACM. Wei Xu, Daniel C. DuVarney, and R. Sekar. 2004. An Efficient and Backwards-Compatible Transformation to Ensure Memory Safety of C Programs. In Proceedings of the 12th ACM SIGSOFT Twelfth International Symposium on Foundations of Software Engineering. ACM."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571208","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571208","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571208"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":57,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571208"],"URL":"https:\/\/doi.org\/10.1145\/3571208","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}