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. © 2010 Springer-Verlag.
CITATION STYLE
Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., … Reps, T. (2010). Directed proof generation for machine code. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6174 LNCS, pp. 288–305). https://doi.org/10.1007/978-3-642-14295-6_27
Mendeley helps you to discover research relevant for your work.