Typed
Assembly Language from an Optimizing Compiler
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.