Directed Proof Generation for Machine Code

File(s):

Author(s): Thakur, A.; Lim, J.; Lal, A.; Burton, A.; Driscoll, E.; Elder, M.; Andersen, T.; Andersen, T.; Reps, T.
Publisher: University of Wisconsin-Madison Department of Computer Sciences
Date: Mar 15, 2012
Abstract: 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.
Permanent link: http://digital.library.wisc.edu/1793/60698
Export: Export to RefWorks