6.888: Certified Systems Software
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
(email@example.com) and describe: (1) your background, (2) the
projects you are thinking of working on, and (3) whether you plan to
take the IAP class.
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.
- Frans Kaashoek
- Nickolai Zeldovich
To contact the course staff, send email to firstname.lastname@example.org.