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.