Sciweavers

Share
CADE
2000
Springer

Machine Instruction Syntax and Semantics in Higher Order Logic

8 years 10 months ago
Machine Instruction Syntax and Semantics in Higher Order Logic
Abstract. Proof-carrying code and other applications in computer security require machine-checkable proofs of properties of machine-language programs. These in turn require axioms about the opcode/operand encoding of machine instructions and the semantics of the encoded instructions. We show how to specify instruction encodings and semantics in higher-order logic, in a way that preserves the factoring of similar instructions in real machine architectures. We show how to automatically generate proofs of instruction decodings, global invariants from local invariants, Floyd-Hoare rules and predicate transformers, all from the speciļ¬cation of the instruction semantics. Our work is implemented in ML and Twelf, and all the theorems are checked in Twelf. A version of this paper is to appear at the 17th International Conference on Automated Deduction to be held between June 17-20, 2000 in Pittsburgh, Pennsylvania.
Neophytos G. Michael, Andrew W. Appel
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 2000
Where CADE
Authors Neophytos G. Michael, Andrew W. Appel
Comments (0)
books