Construction of a Semantic Model for a Typed Assembly Language

Typed Assembly Languages (TALs) can be used to validate the safety of assembly-language programs. However, typing rules are usually trusted as axioms. In this paper, we show how to build semantic models for typing judgments in TALs based on an induction technique, so that both the type-safety theorem and the typing rules can be proved as lemmas in a simple logic. We demonstrate this technique by giving a complete model to a sample TAL. This model allows a typing derivation to be interpreted as a machine-checkable safety proof at the machine level. 1 Overview Safety properties of machine code are of growing concern in both industry and academia. If machine code is compiled from a safe source language, compiler verification can ensure the safety of the machine code. However, it is generally prohibitive to do verification on an industrial-strength compiler due to its size and complexity. In this paper, we do validation directly on machine code. Necula introduced ProofCarrying Code (PCC)...

• Type: Conference
• Year: 2004
• Where: VMCAI
• Authors: Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao Wu
• Keywords: Machine Code, Software Engineering, Typed Assembly Language, Typing Rule, VMCAI 2004