Title: Bounded Model Checking Security Properties of Executables
Abstract: 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.
Publication Year: 2008
Publication Date: 2008-01-01
Language: en
Type: article
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot