6.888: Certified Systems Software

General information

6.888 is a graduate seminar on research in certified systems software. The goal of the class is to get the students to build provably correct software. The structure of the class will consist of students presenting research papers during lecture, and students working on a significant research project. We expect students to start working on the project in the first week or two, and continue for the entire semester, culminating in a draft research paper. Examples of project include building a certified file system, distributed key-value store, in-kernel interpreter, simple OS kernel, etc.

We expect projects will build on tools such as Coq, Dafny, and Bedrock. To get students up to speed with these tools, we will offer a week-long intensive IAP class on Coq (January 26-30, 2015), using parts of the Software Foundations textbook. (The IAP class is not offered for credit, and does not have a subject number.)

If you would like to take this class, please send email to the instructors (6888-staff@csail.mit.edu) and describe: (1) your background, (2) the projects you are thinking of working on, and (3) whether you plan to take the IAP class.

Schedule

This class will meet TR2:30-4 in 35-310.

Reading list ideas

• Comprehensive Formal Verification of an OS Microkernel, Klein et al, TOCS 2014.
• Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System, Yang et al, PLDI 2010.
• Ironclad Apps: End-to-End Security via Automated Full-System Verification, Hawblitzel et al, OSDI 2014.
• Formal verification of a realistic compiler, Xavier Leroy, CACM 2009.
• Jitk: A Trustworthy In-Kernel Interpreter Infrastructure, Wang et al, OSDI 2014.
• From Network Interface to Multithreaded Web Applications, Adam Chlipala, POPL 2015.
• Deep Specifications and Certified Abstraction Layers, Gu et al, POPL 2015.
• RockSalt: Better, Faster, Stronger SFI for the x86, Morrisett et al, PLDI 2012.
• Developing Correctly Replicated Databases Using Formal Tools, Schiper et al, DSN 2014.
• Automating Formal Proofs for Reactive Systems, Ricketts et al, PLDI 2014.
• User-Guided Device Driver Synthesis, Ryzhyk et al, OSDI 2014.
• Software Dataplane Verification, Dobrescu et al, NSDI 2014.
• Automated and modular refinement reasoning for concurrent programs, Hawblitzel et al. MSR-TR-2015-8.
• Compositional CompCert, Stewart et al, POPL 2015.
• Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework, Vasudevan et al, IEEE Security & Privacy 2013.
• Toward a Verified Relational Database Management System, Malecha et al, POPL 2010.
• Verdi: A Framework for Implementing and Formally Verifying Distributed Systems, Wilcox et al, PLDI 2015.

Final projects

• Ejitk: Extending Jitk to eBPF (Louis Sobel)
• Implementing a Verified On-Disk Hash Table (Stephanie Wang)
• Automatic Concurrency Transformations for Query Structures (Anders Kaseorg)
• Modeling High-Level Public-Key Cryptography in Coq (Andres Erbsen)
• FSCQ Final Report (Daniel Ziegler)
• Memory-Safe Microcontroller Applications with the Bedrock Structured Programming System (thesis draft) (Benjamin Barenblat)
• Modular Full-System Verification of Hardware (Muralidaran Vijayaraghavan and Joonwon Choi)
• Building a file system with FSCQ infrastructure (Haogang Chen)
• Towards A Certified Peer-to-Peer Lookup System (Anish Athalye)
• VerifiedDSP: Verifying Digital Signal Processing Designs in Coq (Jeremy Rubin)
• Extracting parallelism in OS kernels using type-safe languages (Cody Cutler)
• Complexity Recursive Types (Peng Wang)

Staff

• Frans Kaashoek
• Nickolai Zeldovich

To contact the course staff, send email to 6888-staff@csail.mit.edu.