Typed Machine Language (Thesis)

Abstract:

With high-speed networks, mobile code applications have become common. One of the important considerations for users (code consumers) of such applications is the guarantee that the downloaded programs are safe. Proof-carrying code is one of the frameworks that allow code consumers to independently verify the safety of untrusted code.

For any such framework to be usable, however, significant trust must be placed in the correctness of that framework itself. The Proof-Carrying Code (PCC) project at Princeton addresses this issue, and aims to build a foundational PCC system that has a trusted component of a very small size. This system consists of a certifying compiler that generates the executable code, and a safety prover that generates the proof of the safety of this code.

The certifying compiler also generates hints that help the prover in generating
the safety proof. These hints are in the form of a typed assembly language program that corresponds to the output object-code program. Therefore, while the hints are specified as high-level type annotations,
the prover must prove the safety of machine-level programs that operate on memory and register banks.

In this thesis, I present Typed Machine Language (TML), which is used to bridge
this gap.TML is a calculus of type operators that can express constructs in high-level languages like core ML at a sufficiently low level to correspond directly to the concrete realisations of these type constructs at the machine level. These operators are expressive enough to be able to allow provably safe optimisations like array-bounds-check eliminations and sum-type discriminations. I shall first present a semantic model for these operators, and typing rules based on them. This model is then used to provide models for assembly-level instructions. The typing rules, along
with the instruction models provide an interface which allows typed assembly languages to be type checked without exposing the complex underlying semantic model.

Finally, I shall present a proof technique that shows how the typability of the
typed assembly languages can be connected to the safety of corresponding machine-level programs using the foundational semantic models for types and instructions provided by TML.