End-to-end verification of secure applications: Chris Hawblitzel, MSR

10:00 am on Monday, December 16, 2013
11:00 am on Monday, December 16, 2013
MCS 148
Abstract: Projects like seL4 and Verve have demonstrated the practicality of formally verifying the correctness of low-level operating system code and low-level run-time system code. In this talk, I'll describe how we're formally verifying high-level secure applications running on verified low-level code, producing an end-to-end verified system that correctly implements high-level application properties using low-level assembly language instructions. I'll focus on how we compile application code, written in the high-level language Dafny, to verified assembly language, and how we connect the verified compiled code to a verified garbage collector and verified OS services, provided by the Verve operating system. Bio: Chris Hawblitzel is a Researcher in the operating systems group at Microsoft Research. He received a B.A. in physics from UC-Berkeley in 1993, a Ph.D. in computer science from Cornell in 2000, and was an Assistant Professor at Dartmouth College from 2000 to 2004. At Microsoft, he currently works on compiler and operating system verification.