Model Checking x86 Executables with CodeSurfer/x86 and WPDS++
作者： G. Balakrishnan , T. Reps , N. Kidd , A. Lal , J. Lim
DOI: 10.1007/11513988_17
关键词: x86 、 Model checking 、 Executable 、 Programming language 、 Computer science 、 PATH (variable) 、 Operating system 、 Reachability 、 Call graph
摘要: This paper presents a toolset for model checking x86 executables. The members of the are CodeSurfer/x86, WPDS++, and Path Inspector. CodeSurfer/x86 is used to extract from an executable in form weighted pushdown system. WPDS++ library answering generalized reachability queries on systems. Inspector software checker built top CodeSurfer that supports safety about program's possible control configurations.
springer.com
core.ac.uk
acm.org 
sci-hub.se 参考文章(15)
Thomas W. Reps, Nicholas Kidd, David Melski, Akash Lal, WPDS++: A C++ library for weighted pushdown systems ,(2005)
Drew Dean, David A. Wagner, Hao Chen, Model Checking One Million Lines of C Code. network and distributed system security symposium. ,(2004)
Akash Lal, Thomas Reps, Gogul Balakrishnan, Extended Weighted Pushdown Systems Computer Aided Verification. pp. 434- 448 ,(2005) , 10.1007/11513988_44
Mihai Christodorescu, Somesh Jha, Static analysis of executables to detect malicious patterns usenix security symposium. pp. 12- 12 ,(2003) , 10.21236/ADA449067
Gogul Balakrishnan, Thomas Reps, Analyzing Memory Accesses in x86 Executables compiler construction. pp. 5- 23 ,(2006) , 10.1007/978-3-540-24723-4_2
Peter Leven, Tilman Mehler, Stefan Edelkamp, Directed Error Detection in C++ with the Assembly-Level Model Checker StEAM international workshop on model checking software. pp. 39- 56 ,(2004) , 10.1007/978-3-540-24732-6_4
Matthew B. Dwyer, George S. Avrunin, James C. Corbett, Patterns in property specifications for finite-state verification international conference on software engineering. pp. 411- 420 ,(1999) , 10.1145/302405.302672
Steven S. Muchnick, Neil D. Jones, Program Flow Analysis: Theory and Application Prentice Hall Professional Technical Reference. ,(1981)
Mooly Sagiv, Thomas Reps, Susan Horwitz, Precise interprocedural dataflow analysis with applications to constant propagation Theoretical Computer Science. ,vol. 167, pp. 131- 170 ,(1996) , 10.1016/0304-3975(96)00072-2
Patrice Godefroid, Model checking for programming languages using VeriSoft symposium on principles of programming languages. pp. 174- 186 ,(1997) , 10.1145/263699.263717