research-article

Open access

MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code

Authors:

Alexandra E. Michael,

Anitha Gollamudi,

Aidan Denlinger,

Craig Disselkoen,

Marco Patrignani,

Deian StefanAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL

Article No.: 15, Pages 425 - 454

https://doi.org/10.1145/3571208

Published: 11 January 2023 Publication History

Abstract

Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm—and attackers can exploit buffer overflows and use-after-frees in Wasm almost as easily as they can on native platforms. Memory- Safe WebAssembly (MSWasm) proposes to extend Wasm with language-level memory-safety abstractions to precisely 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—and 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.

More importantly, MSWasm’s 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.

References

[1]

Carmine Abate, Roberto Blanco, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, and Jérémy Thibault. 2019. Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In 2019 IEEE 32th Computer Security Foundations Symposium (CSF 2019).

[2]

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.

[3]

Arm. 2019. Armv8.5-A Memory Tagging Extension. White Paper.

[4]

2022. Arm Morello Program. https://www.arm.com/architecture/cpu/morello

[5]

Todd M. Austin, Scott E. Breach, and Gurindar S. Sohi. 1994. Efficient Detection of All Pointer and Array Access Errors. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation (PLDI ’94). Association for Computing Machinery, New York, NY, USA. 290–301. isbn:089791662X https://doi.org/10.1145/178243.178446

Digital Library

[6]

Arthur Azevedo de Amorim, Cătălin Hriţcu, and Benjamin C. Pierce. 2018. The Meaning of Memory Safety. In Principles of Security and Trust, Lujo Bauer and Ralf Küsters (Eds.). Springer International Publishing, Cham. 79–105. isbn:978-3-319-89722-6

[7]

Jay Bosamiya, Wen Shih Lim, and Bryan Parno. 2022. Provably-Safe Multilingual Software Sandboxing using WebAssembly. In USENIX Security Symposium.

[8]

CTSRD-CHERI. 2022. The CHERI LLVM Compiler Infrastructure. https://github.com/CTSRD-CHERI/llvm-project

[9]

A. A. d. Amorim, M. Dénès, N. Giannarakis, C. Hritcu, B. C. Pierce, A. Spector-Zabusky, and A. Tolmach. 2015. Micro-Policies: Formally Verified, Tag-Based Security Monitors. In 2015 IEEE Symposium on Security and Privacy. 813–830. https://doi.org/10.1109/SP.2015.55

Digital Library

[10]

Thurston HY Dang, Petros Maniatis, and David Wagner. 2017. Oscar: A Practical page-permissions-based scheme for thwarting dangling pointers. In USENIX Security.

[11]

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.

Digital Library

[12]

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.

Digital Library

[13]

Nathaniel Wesley Filardo, Brett F Gutstein, Jonathan Woodruff, Sam Ainsworth, Lucian Paul-Trifu, Brooks Davis, Hongyan Xia, Edward Tomasz Napierala, Alexander Richardson, and John Baldwin. 2020. Cornucopia: Temporal safety for CHERI heaps. In 2020 IEEE Symposium on Security and Privacy (SP). 608–625.

[14]

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 ’20). ACM.

Digital Library

[15]

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

[16]

Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017. Bringing the Web up to Speed with WebAssembly. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). Association for Computing Machinery, New York, NY, USA. 185–200. isbn:9781450349888 https://doi.org/10.1145/3062341.3062363

Digital Library

[17]

Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017. Bringing the Web up to Speed with WebAssembly. SIGPLAN Not., 52, 6 (2017), June, 185–200. issn:0362-1340 https://doi.org/10.1145/3140587.3062363

Digital Library

[18]

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.

Digital Library

[19]

Michael Hicks. 2014. What is memory safety? http://www.pl-enthusiast.net/2014/07/21/memory-safety/

[20]

Aaron Hilbig, Daniel Lehmann, and Michael Pradel. 2021. An Empirical Study of Real-World WebAssembly Binaries: Security, Languages, Use Cases. ACM.

[21]

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.

[22]

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.

[23]

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.

[24]

Albert Kwon, Udit Dhawan, Jonathan M. Smith, Thomas F. Knight, and Andre DeHon. 2013. Low-Fat Pointers: Compact Encoding and Efficient Gate-Level Implementation of Fat Pointers for Spatial Safety and Capability-Based Security. In Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security. ACM.

Digital Library

[25]

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

[26]

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.

[27]

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.

[28]

Xavier Leroy. 2009. A Formally Verified Compiler Back-end. Journal of Automated Reasoning, 43, 4 (2009), 363–446. http://dx.doi.org/10.1007/s10817-009-9155-4

Digital Library

[29]

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.

[30]

Tyler McMullen. 2020. Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing. Principles of Secure Compilation (PriSC).

[31]

Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. 2019. Exploring C Semantics and Pointer Provenance. Proc. ACM Program. Lang., 3, POPL (2019), Article 67, Jan., 32 pages. https://doi.org/10.1145/3290380

Digital Library

[32]

Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. 2019. Exploring C Semantics and Pointer Provenance. Proc. ACM Program. Lang., 3, POPL (2019), Article 67, jan, 32 pages. https://doi.org/10.1145/3290380

Digital Library

[33]

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–15.

Digital Library

[34]

MSWasm. [n.d.]. Memory-Safe WebAssembly. https://mswasm.programming.systems

[35]

MSWasm. 2023. Reproduction Package for “MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code”. https://doi.org/10.1145/3554344

Digital Library

[36]

Santosh Nagarakatte, Jianzhou Zhao, Milo M.K. Martin, and Steve Zdancewic. 2009. SoftBound: Highly Compatible and Complete Spatial Memory Safety for C. SIGPLAN Not., 44, 6 (2009), June, 245–258. issn:0362-1340 https://doi.org/10.1145/1543135.1542504

Digital Library

[37]

Santosh Nagarakatte, Jianzhou Zhao, Milo M.K. Martin, and Steve Zdancewic. 2010. CETS: Compiler Enforced Temporal Safety for C. SIGPLAN Not., 45, 8 (2010), June, 31–40. issn:0362-1340 https://doi.org/10.1145/1837855.1806657

Digital Library

[38]

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.

[39]

George C. Necula, Jeremy Condit, Matthew Harren, Scott McPeak, and Westley Weimer. 2005. CCured: Type-safe Retrofitting of Legacy Software. ACM Trans. Program. Lang. Syst., 27, 3 (2005), May, 477–526. issn:0164-0925 https://doi.org/10.1145/1065887.1065892

Digital Library

[40]

Oleksii Oleksenko, Dmitrii Kuvaiskii, Pramod Bhatotia, Pascal Felber, and Christof Fetzer. 2018. Intel MPX Explained: A Cross-Layer Analysis of the Intel MPX System Stack. Proc. ACM Meas. Anal. Comput. Syst., 2, 2 (2018), Article 28, jun, 30 pages. https://doi.org/10.1145/3224423

Digital Library

[41]

Aleph One. 1996. Smashing the stack for fun and profit. Phrack magazine, 7, 49 (1996), 14–16.

[42]

Oracle. 2021. GraalVM. https://www.graalvm.org/

[43]

Oracle. 2021. Truffle Language Implementation Framework. https://www.graalvm.org/22.0/graalvm-as-a-platform/language-implementation-framework/

[44]

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/

[45]

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–110. issn:0038-0644

[46]

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), 3492–3505. https://doi.org/10.1109/TCAD.2020.3012647

[47]

Louis-Noel Pouchet. 2011. PolyBench-C: the Polyhedral Benchmark suite. https://web.cs.ucla.edu/ pouchet/software/polybench/

[48]

Aleksandar Prokopec. 2019. Announcing GraalWasm – a WebAssembly engine in GraalVM. https://medium.com/graalvm/announcing-graalwasm-a-webassembly-engine-in-graalvm-25cd0400a7f2

[49]

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.

[50]

Fred B. Schneider. 2000. Enforceable Security Policies. ACM Trans. Inf. Syst. Secur., 3, 1 (2000), feb, 30–50. issn:1094-9224 https://doi.org/10.1145/353323.353382

Digital Library

[51]

Laszlo Szekeres, Mathias Payer, Tao Wei, and Dawn Song. 2013. SoK: Eternal War in Memory. In Proceedings of the 2013 IEEE Symposium on Security and Privacy (SP ’13). IEEE Computer Society.

Digital Library

[52]

Gang Tan. 2017. Principles and Implementation Techniques of Software-Based Fault Isolation. 1, Now Publishers Inc.

[53]

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 ’93). ACM.

Digital Library

[54]

Robert N.M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan Anderson, David Chisnall, Nirav Dave, Brooks Davis, Khilan Gudka, Ben Laurie, Steven J. Murdoch, Robert Norton, Michael Roe, Stacey Son, and Munraj Vadera. 2015. CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization. In 2015 IEEE Symposium on Security and Privacy. 20–37. https://doi.org/10.1109/SP.2015.9

Digital Library

[55]

WebAssembly. [n.d.]. WebAssembly System Interface. https://github.com/WebAssembly/wasi

[56]

Hongyan Xia, Jonathan Woodruff, Sam Ainsworth, Nathaniel W. Filardo, Michael Roe, Alexander Richardson, Peter Rugg, Peter G. Neumann, Simon W. Moore, Robert N. M. Watson, and Timothy M. Jones. 2019. CHERIvoke: Characterising Pointer Revocation Using CHERI Capabilities for Temporal Memory Safety. In Proceedings of the 52nd Annual IEEE/ACM International Symposium on Microarchitecture (MICRO ’52). Association for Computing Machinery, New York, NY, USA. 545–557. isbn:9781450369381 https://doi.org/10.1145/3352460.3358288

Digital Library

[57]

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.

Cited By

Legoupil MRousseau JGeorges APichon-Pharabod JBirkedal L(2024)Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssemblyProceedings of the ACM on Programming Languages10.1145/36897228:OOPSLA2(304-332)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689722
Fitzgibbons MParaskevopoulou ZMushtak NThalakottur MSulaiman Manzur JAhmed A(2024)RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssemblyProceedings of the ACM on Programming Languages10.1145/36564448:PLDI(1656-1679)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656444
Cao SHe NShe XZhang YZhang MWang HChristakis MPradel M(2024)WASMaker: Differential Testing of WebAssembly Runtimes via Semantic-Aware Binary GenerationProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3680358(1262-1273)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3680358
Show More Cited By

Index Terms

MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
1. Security and privacy
  1. Formal methods and theory of security
    1. Formal security models

Recommendations

Safer unsafe code for .NET

The .NET intermediate language (MSIL) allows expressing both statically verifiable memory and type safe code (typically called managed), as well as unsafe code using direct pointer manipulations. Unsafe code can be expressed in C# by marking regions of ...
Safer unsafe code for .NET
OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications

The .NET intermediate language (MSIL) allows expressing both statically verifiable memory and type safe code (typically called managed), as well as unsafe code using direct pointer manipulations. Unsafe code can be expressed in C# by marking regions of ...
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly

Safe, shared-memory interoperability between languages with different type systems and memory-safety guarantees is an intricate problem as crossing language boundaries may result in memory-safety violations. In this paper, we present RichWasm, a novel ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue POPL

January 2023

2196 pages

EISSN:2475-1421

DOI:10.1145/3554308

Editor:

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2023

Published in PACMPL Volume 7, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation
German Federal Ministry of Education and Research
Intel Corporation
Google
National Science Foundation Computing Innovation Fellowship, 2021
Harvard University Center for Research on Computation and Society
Semiconductor Research Corporation
Italian Ministry of Education Rita Levi Montalcini Grant

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
1,614
Total Downloads

Downloads (Last 12 months)1,033
Downloads (Last 6 weeks)116

Reflects downloads up to 24 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Legoupil MRousseau JGeorges APichon-Pharabod JBirkedal L(2024)Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssemblyProceedings of the ACM on Programming Languages10.1145/36897228:OOPSLA2(304-332)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689722
Fitzgibbons MParaskevopoulou ZMushtak NThalakottur MSulaiman Manzur JAhmed A(2024)RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssemblyProceedings of the ACM on Programming Languages10.1145/36564448:PLDI(1656-1679)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656444
Cao SHe NShe XZhang YZhang MWang HChristakis MPradel M(2024)WASMaker: Differential Testing of WebAssembly Runtimes via Semantic-Aware Binary GenerationProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3680358(1262-1273)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3680358
Scherer MBlaabjerg JSjösten ASolitro MMaffei M(2024)Wappler: Sound Reachability Analysis for WebAssembly2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00025(249-264)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00025
Titzer B(2024)Whose Baseline Compiler is it Anyway?2024 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)10.1109/CGO57630.2024.10444855(207-220)Online publication date: 2-Mar-2024
https://doi.org/10.1109/CGO57630.2024.10444855
Rao XGeorges ALegoupil MWatt CPichon-Pharabod JGardner PBirkedal L(2023)Iris-Wasm: Robust and Modular Verification of WebAssembly ProgramsProceedings of the ACM on Programming Languages10.1145/35912657:PLDI(1096-1120)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591265
Anderson SNaaktgeboren ATolmach A(2023)Flexible Runtime Security Enforcement with Tagged CRuntime Verification10.1007/978-3-031-44267-4_12(231-250)Online publication date: 3-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-44267-4_12

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents