**CSE 291: Double Feature: Trustworthy Browsers // Secure Compilation using WebAssembly**
This a double feature graduate course on trustworthy browsers and WebAssembly.
The underlying theme between the two features is to build secure Web systems
using techniques from programming languages, compilers, and verification. This
is a research-oriented course: We will read (sometimes hot-off-the press)
research papers and work on a large research project spanning one or both of
**Trustworthy Browsers (Monday)**:
This feature will cover the design and implementation of modern browsers
security architectures. The feature will explore modern attack techniques on
browsers and study different techniques for addressing these classes of attack.
Students will carry out attacks on browsers (e.g., by exploiting JIT compiler
bugs) and build systems (e.g., sandboxing, bugfinding, static analyses, and
verification tools) to harden real world browsers.
**Secure Compilation using WebAssembly (Wednesday)**
This feature explores the use of secure compilations---a discipline that spans
programming languages, compiler design, verification, and hardware---to build
secure systems, and to rigorously specify and reason about security of these
systems. The feature will expose students to both formal approaches to secure
compilations---covering different attacker models, security criteria, and proof
techniques---and practical secure compiler design.
: Monday and Wednesday, 3:30--4:50pm, on Zoom
: **Instructor**: Deian Stefan
: **Teaching Assistant**: Shravan Narayan
: **Deian**: Tuesday, 3:00--4:00pm, or by appointment
: **Shravan**: By appointment
: See [course Canvas site](https://canvas.ucsd.edu/courses/25115). To facilitate
an open discussion, the in-class discussion will *not* be recorded.
: We'll use Discord for all class related communication (invite link is on Canvas).
Calendar and Readings
Mon Mar 29 2021: Course Intro
- [How to Read a Paper](papers/keshav:how.pdf) by S. Keshav
- [A Note on the Confinement Problem](papers/lampson:confinement.pdf) by B. Lampson
Wed Mar 31 2021: Wasm Intro
- [Bringing the Web up to Speed with WebAssembly](papers/haas:wasm.pdf) by A. Haas et al.
- [Everything Old is New Again: Binary Security of WebAssembly](papers/lehmann:old.pdf) by D. Lehmann et al.
- [Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing](https://www.youtube.com/watch?v=WddPA0U6v2A) by T. McMullen
- *Optional reading*:
- [Hijacking the control flow of a WebAssembly program](https://www.fastly.com/blog/hijacking-control-flow-webassembly) by J. Foote
- [WebAssembly doesn't make unsafe languages safe (yet)](https://00f.net/2018/11/25/webassembly-doesnt-make-unsafe-languages-safe/) by F. Denis
Mon Apr 5 2021: In-the-Wild Series
- [Introducing the In-the-Wild Series](https://googleprojectzero.blogspot.com/2021/01/introducing-in-wild-series.html) at least the first three posts.
Wed Apr 7 2021: Secure Compilation Intro
- [Formal Approaches to Secure Compilation:A Survey of Fully Abstract Compilation and Related Work](papers/patrignani:sc.pdf) by M. Patrignani et al.
Mon Apr 12 2021: Library isolation
- [Retrofitting Fine Grain Isolation in the Firefox Renderer](papers/narayan:retrofitting.pdf) by S. Narayan et al.
- *Additional reading*:
- [Principles and Implementation Techniques of Software-Based Fault Isolation](papers/tan:sfi.pdf) by G. Tan
- [The High-level Benefits of Low-level Sandboxing](papers/sammler:the-high-level.pdf) by M. Sammler et al.
Wed Apr 14 2021: Wasm binary verification
- [Доверя́й, но проверя́й: SFI safety for native-compiled Wasm](https://cseweb.ucsd.edu/~dstefan/pubs/johnson:2021:veriwasm.pdf) by E. Johnson et al.
Fri Apr 16 2021: Project proposal
- *Expectation*: At the very least, you should have a clear problem
statement, brief literature survey (e.g., to understand how and if this
done before), evaluation questions and approach, and brief risk
analysis (e.g., to understand the best and worst case outcome of the
- [*Submit the proposal here*](https://forms.gle/AZe73e4L6oxnqrih7) or email Deian pdf write up.
Mon Apr 19 2021: Process-based isolation
- [Site Isolation: Process Separation for Web Sites within the Browser](papers/reis:site.pdf) by C. Reis et al.
- *Optional reading*:
- [Designing and Implementing the OP and OP2 Web Browsers](papers/grier:op.pdf) by C. Grier et al.
Wed Apr 21 2021: Quark
- [Establishing Browser Security Guarantees through Formal Shim Verification](papers/jang:quark.pdf) by D. Jang et al.
- *Optional reading*:
- [Sound Modular Verification of C Code Executing in an Unverified Context](papers/agten:modular.pdf) by P. Agten et al.
Mon Apr 26 2021: Browser injection attacks
- [Hardening Firefox against Injection Attacks](papers/kerschbaumer:ff.pdf) by C. Kerschbaumer et al.
Wed Apr 28 2021: No class
Fri Apr 30 2021: Status update
Wed May 5 2021: JIT verification
- [Formally Verified Speculation and Deoptimization in a JIT Compiler](papers/barriere:jit.pdf) by A. Barriere et al.
- *Optional reading*:
- [Formal Certification of a Compiler Back-end](papers/leroy:compcert.pdf) by X. Leroy
Wed May 12 2021: PMAs and MS-Wasm
- [Position Paper: Bringing Memory Safety to WebAssembly](https://cseweb.ucsd.edu/~dstefan/pubs/disselkoen:2019:ms-wasm.pdf) by C. Disselkoen et al.
- [Secure Compilation to Protected Module Architectures](papers/patrignani:pma.pdf) by M. Patrignani et al.
- [CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization](papers/watson:cheri.pdf) by R. Watson et. al
Fri May 14 2021: Status update
Mon May 17 2021: Fuzzyfox
- [Trusted Browsers for Uncertain Times](papers/kohlbrenner:fuzzyfox.pdf) by D. Kohlbrenner and H. Shacham
Wed May 19 2021: Well-bracketedness
- [StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities](papers/skorstengaard:stktokens.pdf) by L. Skorstengaard et al.
- [Isolation Without Taxation: Near Zero Cost Transitions for SFI](https://arxiv.org/abs/2105.00033) by M. Kolosick et al.
Mon May 24 2021: [Watch an Oakland talk!](https://www.ieee-security.org/TC/SP2021/program.html)
Wed May 26 2021: Invited talk: Provably-Safe Software Sandboxing using Wasm by Jay Bosamiya
Mon May 31 2021: No class
Wed Jun 2 2021: Presentations
Since the primary goal of this course is to prepare to you to do research, the
evaluation for this course is simple: (1) class participation, including
leading a discussion, and (2) research project.
You are expected to read the assigned paper(s) before each meeting. In class we
will discuss the interesting parts of the paper(s). You are expected to do any
background reading on your own and come prepared with questions and an
evaluation of the paper. Beyond this, in groups of two you will lead the
discussion for one of the lectures.
Research project (65%)
You will work on projects in groups of 2-4. The goal of the project is to
conduct original research in security. You are encouraged to come up with your
own project idea, but we have a few ideas that are well-scoped for a quarter
At the end of the quarter, you are expected to turn in a short research paper
(6-10 pages) and give a 10 minute talk. We will have periodic status updates to
help you stay on track.