**CSE 291-P: Language-Based Security** [*Deian Stefan*](https://cseweb.ucsd.edu/~dstefan/) About ============================================================== This is a graduate course on language-based security. Most software we rely upon is plagued by security vulnerabilities — the common occurrence of large-scale private data theft alone serves to highlight the magnitude of the problem. Yet the rise of new application domains and platforms is making software ever more integral to daily life. It is prudent for us to build more secure software systems. One promising approach to building secure systems is to leverage ideas from the programming languages community. The recent industry trend of adopting new languages, type systems, and verification tools also makes this approach very timely. This research course explores the use of various programming languages, program analysis, and program verification techniques to (1) enforce security, and (2) to rigorously specify and reason about security. We will study secure runtime systems (e.g., operating systems, web servers, web browsers) and the underlying techniques used to make them secure (e.g., language-level information flow control, static checkers, symbolic execution, and refinement types). This is a research-oriented class: students are expected to read papers in depth, pickup the background on their won, and work on a relatively large research project. Lectures: : MWF 3:00 - 3:50pm Staff: : **Instructor**: Deian Stefan : **TA**: Lydia Zoghbi Office hours: : **Deian**: Friday 3:50-4:50pm Class discussion: : We'll use the CSE slack channel `cse291p-wi26` Grade: : We'll use the CSE slack channel `cse291p-wi26` Calendar and Readings ============================================================== Mon Jan 5 2026: Introduction - *Reading*: Wed Jan 7 2026: IFC - *Reading*: [Language-Based Information-Flow Security](./papers/sm-jsac03.pdf) by Andrei Sabelfeld and Andrew C. Myers Fri Jan 9 2026: IFC - *Reading*: [A sound type system for secure flow analysis](./papers/volpano96.pdf) by Dennis Volpano, et al. Mon Jan 12 2026: IFC - *Reading*: [Flexible Dynamic Information Flow Control in the Presence of Exceptions](https://cseweb.ucsd.edu/~dstefan/pubs/stefan:2017:flexible.pdf) by Deian Stefan, et al. - *Reading (optional)*: [Co-Inflow: Coarse-grained Information Flow Control for Java-like Languages](https://jianxiang.info/pub/SP21.pdf) by Jian Xiang and Stephen Chong Wed Jan 14 2026: IFC - *Reading*: [Addressing Covert Termination and Timing Channels in Concurrent Information Flow Systems](https://cseweb.ucsd.edu/~dstefan/pubs/stefan:2012:addressing.pdf) Fri Jan 16 2026: IFC (cont) Mon Jan 19 2026: No class (MLK day) Wed Jan 21 2026: Applications of IFC (sandboxing) - *Reading*: [Retrofitting Fine Grain Isolation in the Firefox Renderer](./papers/rlbox.pdf) by Shravan Narayan, et al. Fri Jan 23 2026: Applications of IFC (web) - **Due**: Projects proposals (problem statement and approach) - *Reading*: [STORM: Refinement Types for Secure Web Applications](./papers/storm.pdf) by Nico Lehmann, et al. - *Reading (optional)*: [Hails: Protecting Data Privacy in Untrusted Web Applications](https://cseweb.ucsd.edu/~dstefan/pubs/giffin:2012:hails.pdf) by Daniel B. Giffin et al. Mon Jan 26 2026: Crypto - *Reading*: [OwlC: Compiling Security Protocols to Verified, Secure, High-Performance Libraries](https://www.andrew.cmu.edu/user/bparno/papers/owlc.pdf) by Pratap Singh, et al. Wed Jan 28 2026: Crypto - *Reading*: [FaCT: A DSL for timing-sensitive computation](https://cseweb.ucsd.edu/~dstefan/pubs/cauligi:2019:fact.pdf) by Sunjay Cauligi, et al. Fri Jan 30 2026: Crypto - *Reading (optional):* [Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust](./papers/bhargavan25.pdf) by Karthikeyan Bhargavan, et al. Mon Feb 2 2026: Wasm - *Reading*: [Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection](./papers/crocus.pdf) by Alexa VanHattum et al. Wed Feb 4 2026: Wasm - *Reading*: [Доверя́й, но проверя́й: SFI safety for native-compiled Wasm](https://cseweb.ucsd.edu/~dstefan/pubs/johnson:2021:veriwasm.pdf) by Evan Johnson, et al. Fri Feb 6 2026: Wasm - **Due**: Projects updates (what did you do, what went well, what didn't go well, what's next) - *Reading (optional)*: [WaVe: a verifiably secure WebAssembly sandboxing runtime.](https://cseweb.ucsd.edu/~dstefan/pubs/johnson:2023:wave.pdf) by Evan Johnson, et al. Mon Feb 9 2026: Secure Compilers - *Reading* [Formal Certification of a Compiler Back-end](./papers/compcert.pdf) by Xavier Leroy Wed Feb 11 2026: Secure Compilers - *Reading*: [Alive2: bounded translation validation for LLVM](https://users.cs.utah.edu/~regehr/alive2-pldi21.pdf) by Nuno P. Lopes, et al. Fri Feb 13 2026: Secure Compilers (cont) - *Reading (optional)*: [Future Directions for Optimizing Compilers](https://arxiv.org/pdf/1809.02161) by Nuno P. Lopes and John Regehr - *Reading (optional)*: [The Next 700 Compiler Correctness Theorems](https://www.ccs.neu.edu/home/amal/papers/next700ccc.pdf) by Daniel Patterson and Amal Ahmed Mon Feb 16 2026: No class (Presidents' day) Wed Feb 18 2026: Midterm review Fri Feb 20 2026: Midterm - **Due**: Projects updates (what did you do, what went well, what didn't go well, what's next) Mon Feb 23 2026: Symbolic Execution - *Reading*: [EXE: Automatically generating inputs of death](./papers/exe.pdf) Wed Feb 25 2026: Symbolic Execution - *Reading*: [Icarus: Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution](https://cseweb.ucsd.edu/~dstefan/pubs/smith:2024:icarus.pdf) by Naomi Smith, et al. Fri Feb 27 2026: Symbolic Execution (cont) - *Reading (optional)*: [Sys: a Static/Symbolic Tool for Finding Good Bugs in Good (Browser) Code](https://cseweb.ucsd.edu/~dstefan/pubs/brown:2020:sys.pdf) by Fraser Brown, et al. Mon Mar 2 2026: Static Analysis - *Reading*: [How to Build Static Checking Systems Using Orders of Magnitude Less Code](./papers/microchex.pdf) by Fraser Brown, et al. Wed Mar 4 2026: Static Analysis - *Reading*: [Finding Real Bugs in Big Programs with Incorrectness Logic](https://dl.acm.org/doi/epdf/10.1145/3527325) by Quang Loc Le, et al. Fri Mar 6 2026: Static Analysis (cont) - **Due**: Projects updates (game plan for the last stretch) Mon Mar 9 2026: Fuzzing - *Reading*: [FUZZILLI: Fuzzing for JavaScript JIT Compiler Vulnerabilities](./papers/fuzzilli.pdf) by Samuel Groß, et al. Wed Mar 11 2026: Fin - *Reading*: [Automated Exploit Generation for Node.js Packages](https://dl.acm.org/doi/epdf/10.1145/3729304) by Filipe Marques, et al. - *Reading (optional)*: [Automatic exploit generation](https://dl.acm.org/doi/epdf/10.1145/2560217.2560219) by Thanassis Avgerinos, et al. Fri Mar 13 2026: Fuzzing - *Reading*: [Nyx: Greybox Hypervisor Fuzzing using Fast Snapshots and Affine Types](https://www.usenix.org/system/files/sec21-schumilo.pdf) by Sergej Schumilo, et al. Evaluation ============================================================== 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, (2) midterm exam, and (3) research project. Participation (30%) -------------------------------------------------------------- You are expected to read the assigned paper(s). 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---participating in the discussion is key! Midterm exam (15%) -------------------------------------------------------------- There will be a midterm exam covering the material discussed in class and the assigned readings. The goal is not to test your memory, but rather your understanding---so expect questions that require you to apply the concepts discussed in class to new languages/systems. Research project (55%) -------------------------------------------------------------- You will work on projects in groups of 3-5. 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 project. Many of the projects from [this CSE 227](https://plsyssec.github.io/cse227-spring25/) are relevant. At the end of the quarter, you are expected to turn in a short research paper (6-10 pages) and give a 7-10 minute talk. We will have periodic status updates to help you stay on track.