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
Abstract:
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.
Paper available as: PS or PDF [© Springer-Verlag]
|