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

  • Starts: 10:00 am on Monday, December 16, 2013
  • Ends: 11:00 am on Monday, December 16, 2013
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.
MCS 148

Back to Calendar