My paper with Chris Hawblitzel "Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System" appeared as a Research Highlight (read here) of the Communications of the Association of Computing Machinery (CACM) in December. This is a shortened version of our 2010 paper appearing at the Programming Language Design and Implementation (PLDI) conference altered for a more general audience.
This paper describes the Verve operating system, the first operating system verified end-to-end and automatically for type safety. This means that programs running in Verve cannot suffer from whole classes of memory-related errors. The main idea of Verve is to implement the operating system in a type-safe language (C#), write a specification for the memory interface between the type-safe parts and the lower-level parts (the C# code does not mess up the stack; the low-level code does not mess up the heap), and verify the low-level parts of the system (in our case, using Boogie that translates to x86 assembly).
An exciting thing is that Xavier Leroy, who is responsible for both OCaml and the CompCert verified C compiler, wrote the Technical Perspective, "Safety First!" He writes, "The formal verification of high-assurance software is making great progress lately. Yang and Hawblitzel's work, along with other recent breakthroughs in software verification such as the seL4 verified microkernel of Klein et al. (see Communications, June 2010, p. 107), were unthinkable 10 years ago. Little by little, one point at a time, these results sketch a promised land where, with mathematical certainty, software does behave properly after all."
Another exciting thing for current graduate students interested in this work is that my Microsoft Research mentor Chris Hawblitzel is looking for a summer intern to work on adding concurrency to Verve. Not only was Chris Hawblitzel amazing for helping me learn everything I needed for this project, but he was also a fun mentor. I recommend that you contact him ASAP if you are interested in working with his this summer.
1 comment:
Creating a personal statement can be an incredibly important task. In many cases it can hurt you much more than it can help you. There have been a lot of debate surrounding the importance of personal statements, because they often are a much larger potential detriment than a potential advantage. See more pharmacy personal statement example
Post a Comment