Model Checking x86 Executables with CodeSurfer/x86 and WPDS++
G. Balakrishnan, T. Reps, N. Kidd, A. Lal, J. Lim,
D. Melski, R. Gruian, S. Yong, C.-H. Chen, T. Teitelbaum
This paper presents a toolset for model checking x86 executables. The
members of the toolset are CodeSurfer/x86, WPDS++,
and the Path Inspector. CodeSurfer/x86 is used to extract a
model from an executable in the form of a weighted pushdown
system.
WPDS++ is a library for answering
generalized reachability queries on weighted pushdown systems. The
Path Inspector is a software model checker built on top of CodeSurfer
and WPDS++ that supports safety queries about the program's possible
control configurations.
(Click here to access the paper:
PostScript,
PDF.)