Computer Science Speaking Skills Talk
— 3:00pm
Location:
6121
-
Gates and Hillman Centers
Speaker:
JAY BOSAMIYA
,
Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://www.jaybosamiya.com/
Provably-Safe Multilingual Software Sandboxing using WebAssembly
Many applications, from the Web to smart contracts, need to safely execute untrusted code. We observe that WebAssembly (Wasm) is ideally positioned to support such applications, since it promises safety and performance, while serving as a compiler target for many high-level languages.
However, Wasm’s safety guarantees are only as strong as the implementation that enforces them. Hence, we explore two distinct approaches to producing provably sandboxed Wasm code. One draws on traditional formal methods to produce mathematical, machine-checked proofs of safety. The second carefully embeds Wasm semantics in safe Rust code such that the Rust compiler can emit safe executable code with good performance.
Our implementation and evaluation of these two techniques indicate that leveraging Wasm gives us provably-safe multilingual sandboxing with performance comparable to standard, unsafe approaches.
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.
For More Information:
In-person