When: Wednesday, April 30, 3:30 p.m.- 5:00 p.m.

Where: 8220 Wean Hall

Chris Hawblizel, Microsoft Research

POP Seminar

Abstract:
Programming language safety can protect a computer from many forms of errant or malicious code. In this approach, a verifier and run-time system perform static and dynamic checks to ensure that a program performs no unsafe operations. Commonly used safe language platforms, such as Sun's Java Virtual Machine and Microsoft's Common Language Runtime, are large pieces of software, containing sophisticated just-in-time compilers and run-time systems. On the positive side, these platforms support fast execution of programs written in complex languages. On the negative side, because of their large size, it is difficult to ensure that these platforms enforce safety for all programs -- a single bug in a just-in-time compiler or garbage collector could open a vulnerability that allows unsafe execution.

Proof-carrying code (PCC) and typed assembly language (TAL) promise to reduce the amount of code that must be trusted to ensure safe execution. In the PCC/TAL approach, a vendor ships verifiable native code to the consumer, the consumer verifies the native code's safety directly, and no just-in-time compilation is required. In this talk, I will discuss how we modified a large-scale, optimizing compiler, called Bartok, to generate verifiable typed assembly language. Our measurements of a suite of C# benchmarks show that the generated TAL code runs less than 3% slower than the untyped assembly language generated by the unmodified compiler. Although we currently trust much of Bartok's run-time system, including its garbage collector, I will also present preliminary work on verifying garbage collectors using the BoogiePL language and Z3, an automated theorem prover.

Chris Hawblitzel is a researcher in the operating systems group at Microsoft Research

<< Back