Directed proof generation for machine code
Computer Aided Verification: 22nd International Conference, CAV 2010 …, 2010•Springer
We present the algorithms used in McVeto (M achine-C ode VE rification TO ol), 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 …
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 …
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.
Springer