Sciweavers

Share
SCAM
2008
IEEE

Automated Detection of Code Vulnerabilities Based on Program Analysis and Model Checking

9 years 5 months ago
Automated Detection of Code Vulnerabilities Based on Program Analysis and Model Checking
Ensuring the correctness and reliability of software systems is one of the main problems in software development. Model checking, a static analysis method, is preponderant in improving the precision of vulnerabilities detection. However, when applied to buffer overflow and other bugs, it is hard to automatically construct the model for detecting the vulnerabilities. To address this problem we propose an approach that combines constraint based analysis and model checking together. We trace the memory size of buffer-related variables and instrument the code with corresponding constraint assertions before the potential vulnerable points by constraint based analysis. Then the problem of detecting vulnerabilities is converted into the problem of detecting vulnerabilities to verifying the reach ability of these assertions by model checking. In order to reduce the cost of model checking, program slicing is introduced to reduce the code size. CodeAuditor is a prototype implementation of our a...
Lei Wang, Qiang Zhang, PengChao Zhao
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where SCAM
Authors Lei Wang, Qiang Zhang, PengChao Zhao
Comments (0)
books