Formal verification of software typically consists in checking programs in a
high-level language against an abstract specification. Confidence on the
correctness of the actual program running on a machine also relies on the
soundness of the translation from the high-level language to the machine code,
i.e., the correctness of a compiler, including its code optimisation
techniques.
If one wishes to have confidence on the final code, another approach is object
code verification, i.e., verification of program code at assembly level. Now
the confidence in the implementation of a program on an actual machine is more
direct, relying on the correctness of the hardware model and no other software.
But, dealing with object code also has a price. It is, in a sense, further away
from its specification because it has to deal with a more concrete machine,
considering registers, limited memory, and so on. There is a vast shift in
granularity between code and specification.
The technique for object code verification we are developing emphasises the use
of abstraction, aided by a process algebraic framework. The concept of
simulation provides the tool with which abstractions on the process
algebraic representation of the program can be formalised.
However, the correctness proof takes place in higher-order logic (HOL),
which we believe presents a more amenable proof environment. Abstraction at
the logical level is obtained by unlifting results from the CCS level using
the CCS semantics. More precisely, let < be a simulation relation, and let
[[ ]]^s be the lifting operator for a particular sequence s of states, then
If P < Q then for all s . [[P]]^s implies [[Q]]^s .
The interaction between the logical and the algebraic level is fundamental for
our methodology.
We have implemented this approach in a proof system we call Holly. We use
Isabelle/HOL, in which we embedded a variation of Milner's Calculus of
Communicating Systems (CCS) as a process algebra. When verifying a program,
its object code is translated both into a representation in HOL and an
equivalent representation in CCS. At any point in a proof either deductions in
HOL or simulations in the process algebra can be used.
Holly demonstrates the concurrent use of a logical and an algebraic model to
make object code verification feasible. In this talk, we expand on the
interaction between these models, and highlight the interaction within an
example proof in Holly.