Bounded Model Checking Security Properties of Executables

Introduce model checking method to vulnerability analysis of executables.This paper formally modeled binary executables,then adapted model checking technology to verify security properties of executables,and developed a useful model checker.Memory leak and stack buffer overflow vulnerability as example properties,were abstracted to temporal logic formula,and then model checker verified whether the properties are satisfiable.The checking result as expected are sound and prove that bounded model checking is an effective static analysis method.