Automatic verification of object code against source code

An important step when applying formal methods to gain assurance of trusted systems is the verification of object code against source code. One way to mechanically verify that the object code faithfully implements the source code from which it is compiled is to verify the compiler. However, verifying the implementation of an industrial-strength compiler is a very difficult technical problem at the present time. For small fragments of code, it may be easier to verify the equivalence of the source and object code by reasoning about their behavior directly without dealing with the algorithm used for translation. In this paper, we describe a system for automatically verifying MC68020 object code against C source code. The semantics of a small subset of C and MC68020 object code are formalized in the logic of Nqthm (a.k.a. the Boyer-Moore theorem prover). After a large collection of lemmas about C and MC68020 semantics are made available, Nqthm is able to prove the correctness theorems automatically for a small class of programs. For practical use of the system to be possible, we wrote a front-end to Nqthm that generates correctness theorems, given the C source file as input. Using our front-end, we tested our system by verifying the object code produced by the GCC and CC compilers for some small programs