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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol. 2985, pp. 5–23. Springer, Heidelberg (2004)
Chen, H., Dean, D., Wagner, D.: Model checking one million lines of C code. In: Symp. on Network and Distributed Systems Security (2004)
Christodorescu, M., Jha, S.: Static analysis of executables to detect malicious patterns. In: USENIX Security Symposium (2003)
CodeSurfer, GrammaTech., Inc., http://www.grammatech.com/products/codesurfer/
Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: Int. Conf. on Softw. Eng. (1999)
Fast library identification and recognition technology, DataRescue sa/nv, Liège, Belgium, http://www.datarescue.com/idabase/flirt.htm
Godefroid, P.: Model checking for programming languages using VeriSoft. In: ACM (ed.) Princ. of Prog. Lang., pp. 174–186. ACM Press, New York (1997)
IDAPro disassembler, http://www.datarescue.com/idabase/
Kidd, N., Reps, T., Melski, D., Lal, A.: WPDS++: A C++ library for weighted pushdown systems. Univ. of Wisconsin (2004)
Lal, A., Reps, T., Balakrishnan, G.: Extended weighted pushdown systems. In: Computer Aided Verif. (2005)
Leven, P., Mehler, T., Edelkamp, S.: Directed error detection in C++ with the assembly-level model checker StEAM. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 39–56. Springer, Heidelberg (2004)
Müller-Olm, M., Seidl, H.: Analysis of modular arithmetic. In: ESOP (2005)
Musuvathi, M., Park, D., Chou, A., Engler, D., Dill, D.: CMC: A pragmatic approach to model checking real code. In: Op. Syst. Design and Impl. (2002)
Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. of Comp. Prog. (2005) (To appear)
Sagiv, M., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comp. Sci. 167, 131–170 (1996)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Balakrishnan, G. et al. (2005). Model Checking x86 Executables with CodeSurfer/x86 and WPDS++. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_17
Download citation
DOI: https://doi.org/10.1007/11513988_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)