Principal Investigator Nickolai Zeldovich
Co-investigator M Kaashoek
Developing OS kernels that can provide strong security guarantees, through the use of high-level languages like Go, or through formal proofs of correctness using a proof assistant like Coq.