~/talk

MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code

on YouTube 25m
Talkat POPL 2023 · 2023-01-15..01-21· [webassembly]

speakers

name:Alexandra E. Michael
links:none on file
name:Anitha Gollamudi
links:none on file
name:Jay Bosamiya
links:none on file
name:Evan Johnson
links:none on file
name:Aidan Denlinger
links:none on file
name:Craig Disselkoen
bluesky:craigdissel.bsky.social
name:Conrad Watt
links:none on file
name:Bryan Parno
website:https://www.andrew.cmu.edu/user/bparno/
name:Marco Patrignani
links:none on file
name:Marco Vassena
links:none on file
name:Deian Stefan
links:none on file

resources

video:https://youtu.be/uBqi4T0tnd8
slides:none on file

summary

Extends Wasm with segmented memory and unforgeable handles that carry colored provenance, a formal semantics, and a proof that well-typed MSWasm modules are robustly memory safe even when linked with adversarial modules. Provides a formal C-to-MSWasm compiler (extends Clang) that either preserves safe C semantics or guarantees a trap at the first C memory violation. Implements three compilers and reports overheads from 22% (spatial software) up to 198% (full software), and 51.7% with hardware capabilities.

AI-written summary · about

chapters (20)

  1. 0:00MSWasm: Soundly Enforcing Memory- Safe Execution of Unsafe Code
  2. 0:29WebAssembly
  3. 1:42But, Little Protection Within Sandbox!
  4. 2:22Vulnerabilities Persist Across Compilation
  5. 3:37Compiler Could Insert Inlined Memory Safety Checks
  6. 5:38Why are Inlined Memory Safety Checks Slow?
  7. 6:21Our Solution: MSWasm
  8. 8:35Allocating a Segment
  9. 9:32Handle Arithmetic
  10. 10:21Accessing a Segment
  11. 11:27How to Enforce Memory Safety via Compilation?
  12. 11:55Recall: Buffer Overflow Persists Across Compilation to Wasm
  13. 12:20Compilation to MSWasm Without Buffer Overflows
  14. 13:20What is Memory Safety, Formally?
  15. 14:25Recall: Limitations of Inlined Memory Safety Checks
  16. 14:51MSWasm is Robustly Memory Safe
  17. 15:35Language-Agnostic Memory Safety Monitor
  18. 17:52Implementation
  19. 18:46Evaluation: Can MSWasm Leverage Platform-Specific Features? Yes.
  20. 20:51MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.