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.