Semantic foundations for typed assembly languages
Abstract
Typed Assembly Languages (TALs) are used to validate the safety of machine-language programs. The Foundational Proof-Carrying Code project seeks to verify the soundness of TALs using the smallest possible set of axioms: the axioms of a suitably expressive logic plus a specification of machine semantics. This article proposes general semantic foundations that permit modular proofs of the soundness of TALs. These semantic foundations include Typed Machine Language (TML), a type theory for specifying properties of low-level data with powerful and orthogonal type constructors, and L c , a compositional logic for specifying properties of machine instructions with simplified reasoning about unstructured control flow. Both of these components, whose semantics we specify using higher-order logic, are useful for proving the soundness of TALs. We demonstrate this by using TML and L c to verify the soundness of a low-level, typed assembly language, LTAL, which is the target of our core-ML-to-sparc compiler.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Mar 01, 2010
- Source ID
- 10.1145/1709093.1709094
Entities
People
- Amal Ahmed
- Andrew Appel
- Christopher D. Richards
- Daniel C. Wang
- Gang Tan
- Kedar N. Swadi
Organizations
- Agricultural Research Development Agency
- Defense Advanced Research Projects Agency
- Division of Computing and Communication Foundations
- National Science Foundation
- Princeton University