Directed Proof Generation for Machine Code

Thakur, Aditya V. and Lim, Junghee and Lal, Akash and Burton, Amanda and Driscoll, Evan and Elder, Matt and Andersen, Tycho and Reps, Thomas W.
22nd International Conference on Computer Aided Verification (CAV), 2010

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.

PDF     Springer©    

@inproceedings{thakur_etal_CAV10,
  author = {Thakur, Aditya V. and Lim, Junghee and Lal, Akash and Burton, Amanda and Driscoll, Evan and Elder, Matt and Andersen, Tycho and Reps, Thomas W.},
  title = {Directed Proof Generation for Machine Code},
  booktitle = {22nd International Conference on Computer Aided Verification ({CAV})},
  year = {2010},
  pages = {288--305},
  publisher = {Springer},
  doi = {10.1007/978-3-642-14295-6_27}
}