Title: A low-level typed assembly language with a machine-checkable soundness proof
Abstract: To verify the safety of a machine-language program, the Proof-Carrying Code framework requires machine code accompanied by a proof of safety. Typed assembly languages provide a way to generate such safety proofs automatically. 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 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 type-checking algorithm is completely syntax-directed.
I also explain a prototype system that uses LTAL to compile core ML to Sparc code and generate safety proofs. I 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 a type system pervading the instruction selector and register allocator.
Publication Year: 2004
Publication Date: 2004-01-01
Language: en
Type: dissertation
Access and Citation
Cited By Count: 6
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot