A Low-Level Typed Assembly Language with a Machine-Checkable Soundness Proof (Thesis)

Abstract:

To reason about mobile machine code safety, Proof-Carrying Code framework requires machine code accompanied by a proof of safety. Typed assembly languages provide a way to automatically generate such safety proofs. But the soundness proofs of most existing typed assembly languages are hand-written and cannot be machine-checked, which is worrisome for such large calculi.

In this dissertation I will explain a low-level typed assembly language (LTAL) with a semantic model that proves LTAL's soundness with a machine-checkable proof. Compared to existing typed assembly languages, LTAL is more scalable and more secure; it has no macro instructions that hinder low-level optimizations such as instruction scheduling; its type constructors are expressive enough to capture dataflow information, support the compiler's choice of data representations and permit typed position-independent code; and its typed-checking algorithm is completely syntax-directed.

I will also explain a prototype system that uses LTAL to compile core ML to Sparc code and generate safety proofs. I will show how we were able to build type-preserving back end based on an untyped one, without restricting low-level optimizations and without knowledge of any type system pervading the instruction and selector and register allocator.