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 specification 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.

• Type: Conference
• Year: 2000
• Where: CADE
• Authors: Neophytos G. Michael, Andrew W. Appel
• Keywords: CADE 2000, Instruction, Logical Reasoning, Real Machine Architectures, Turn Require Axioms