Directed Proof Generation for Machine Code
A. Thakur, J. Lim, A. Lal, A. Burton, E. Driscoll, M. Elder,
T. Andersen, and T. Reps
We present the algorithms used in McVeto
(Machine-Code VErification TOol),
a tool to check whether a stripped machine-code program
satisfies a safety property. The verification problem that McVeto
addresses is challenging because it cannot assume that it has access
to (i) certain structures commonly relied on by source-code
verification tools, such as control-flow graphs and call-graphs, and
(ii) meta-data, such as information about variables, types, and
aliasing. It cannot even rely on out-of-scope local variables and
return addresses being protected from the program's actions. What
distinguishes McVeto from other work on software model checking is
that it shows how verification of machine-code can be performed, while
avoiding conventional techniques that would be unsound if applied at
the machine-code level.
(Click here to access the paper:
CAV 10 version;
Extended version (TR-1669);
(c) Springer-Verlag.)