Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

AEGIS: Towards Formalized and Practical Memory-Safe Execution of C programs via MSWASM

Shahram Esmaeilsabzali, Arayi Khalatyan, Zhijun Mo, Sruthi Venkatanarayanan, Shengjie Xu

TL;DR

This work addresses memory safety in C by leveraging Memory-Safe WebAssembly (MSWASM) as a safe intermediate representation. It delivers a formal Coq/Iris model of MSWASM with inter-module interaction and proves local handle isolation, then couples this with Aegis, a pipeline that translates MSWASM to spatially safe Checked C code to protect C programs, including legacy libraries. The key contributions are a mechanized MSWASM formalization, a proof of translation to Checked C ensuring spatial safety, and a practical toolchain that achieves substantial runtime efficiency while preserving binary compatibility. The approach enables safe interoperability among multi-party components and offers a concrete path to deploy memory-safety guarantees in real-world C systems with modest performance overhead and limited memory impact.

Abstract

Programs written in unsafe languages such as C are prone to memory safety errors, which can lead to program compromises and serious real-world security consequences. Recently, Memory-Safe WebAssembly (MSWASM) is introduced as a general-purpose intermediate bytecode with built-in memory safety semantics. Programs written in C can be compiled into MSWASM to get complete memory safety protection. In this paper, we present our extensions on MSWASM, which improve its semantics and practicality. First, we formalize MSWASM semantics in Coq/Iris, extending it with inter-module interaction, showing that MSWASM provides fine-grained isolation guarantees analogous to WASM's coarse-grained isolation via linear memory. Second, we present Aegis, a system to adopt the memory safety of MSWASM for C programs in an interoperable way. Aegis pipeline generates Checked C source code from MSWASM modules to enforce spatial memory safety. Checked C is a recent binary-compatible extension of C which can provide guaranteed spatial safety. Our design allows Aegis to protect C programs that depend on legacy C libraries with no extra dependency and with low overhead. Aegis pipeline incurs 67% runtime overhead and near-zero memory overhead on PolyBenchC programs compared to native.

AEGIS: Towards Formalized and Practical Memory-Safe Execution of C programs via MSWASM

TL;DR

This work addresses memory safety in C by leveraging Memory-Safe WebAssembly (MSWASM) as a safe intermediate representation. It delivers a formal Coq/Iris model of MSWASM with inter-module interaction and proves local handle isolation, then couples this with Aegis, a pipeline that translates MSWASM to spatially safe Checked C code to protect C programs, including legacy libraries. The key contributions are a mechanized MSWASM formalization, a proof of translation to Checked C ensuring spatial safety, and a practical toolchain that achieves substantial runtime efficiency while preserving binary compatibility. The approach enables safe interoperability among multi-party components and offers a concrete path to deploy memory-safety guarantees in real-world C systems with modest performance overhead and limited memory impact.

Abstract

Programs written in unsafe languages such as C are prone to memory safety errors, which can lead to program compromises and serious real-world security consequences. Recently, Memory-Safe WebAssembly (MSWASM) is introduced as a general-purpose intermediate bytecode with built-in memory safety semantics. Programs written in C can be compiled into MSWASM to get complete memory safety protection. In this paper, we present our extensions on MSWASM, which improve its semantics and practicality. First, we formalize MSWASM semantics in Coq/Iris, extending it with inter-module interaction, showing that MSWASM provides fine-grained isolation guarantees analogous to WASM's coarse-grained isolation via linear memory. Second, we present Aegis, a system to adopt the memory safety of MSWASM for C programs in an interoperable way. Aegis pipeline generates Checked C source code from MSWASM modules to enforce spatial memory safety. Checked C is a recent binary-compatible extension of C which can provide guaranteed spatial safety. Our design allows Aegis to protect C programs that depend on legacy C libraries with no extra dependency and with low overhead. Aegis pipeline incurs 67% runtime overhead and near-zero memory overhead on PolyBenchC programs compared to native.

Paper Structure

This paper contains 26 sections, 4 theorems, 6 figures.

Table of Contents

  1. Introduction
  2. Formalism.
  3. Aegis Pipeline.
  4. Background
  5. WASM and MSWASM
  6. Checked C
  7. Formal Semantics of MSWASM in Coq
  8. Extension for MSWASM on Module Interaction
  9. Type Safety in MSWASM
  10. Memory Safety in MSWASM
  11. Aegis Pipeline
  12. Limitations
  13. Aegis Pipeline In Action
  14. Additional Features
  15. Global variable handling
  16. ...and 11 more sections

Key Result

Theorem 1

A syntactically well-typed closed expression can never reach a stuck state during its execution, where stuckness represents any error including spatial safety.

Figures (6)

  • Figure 1: MSWASM Syntax and Semantic of WASM with MSWASM Extension highlighted michael2023mswasm. We add h.null, shown in pink, to the formal syntax to facilitate our proofs.
  • Figure 2: (MS)WASM Module Syntax, adapted from rao2023iris
  • Figure 3: Overview of AEGIS Pipeline
  • Figure 4: Code example (C to MSWASM to Checked C)
  • Figure 5: Runtime and memory usage.
  • ...and 1 more figures

Theorems & Definitions (6)

  • Theorem 1: Type Safety for Closed Expression
  • Theorem 2: Type Safety for Closed Module
  • Definition 1: Reachable, and Maximal Reachable
  • Theorem 3: Local Handle Isolation
  • Example 1
  • Theorem 4: Local Handle Isolation for Module