Font Size: a A A

Research On Accuracy Of Data Flow In Static Analysis Based On Defect Pattern

Posted on:2018-06-30Degree:MasterType:Thesis
Country:ChinaCandidate:S R LiuFull Text:PDF
GTID:2348330518995405Subject:Intelligent Science and Technology
Abstract/Summary:PDF Full Text Request
With the rapid development of the Internet, information technology has covered many aspects of life, but also brought a lot of problems, such as information disclosure and economic losses caused by hacker attacks.Therefore, the research of trusted software has become a top priority. Static analysis is an effective way of discovering source code defects and improving the quality of source code. However, static analysis can not collect enough data flow information because of not running code, so the accuracy of the analysis result is low. Symbolic execution technology can collect enough data flow information through simulating program execution, thereby increasing the accuracy of static analysis and making up for the weakness of static analysis tools.In order to improve the accuracy of static analysis results, this paper design and implement a source code detection tool ABAZER-SE,which is based on the GCC abstract syntax tree. The ABAZER-SE combines symbolic execution and static analysis techniques to detect defects in the source code. The main research contents and achievements of this paper are as follows:(1)We study the encoding type of GCC abstract syntax tree, static analysis method and the working principle of symbolic execution technology. We analyze the characteristics of static analysis based on defect model, and put forward the scheme to improve the accuracy of detection result of static analysis by using symbolic execution.(2)We design a path exploration algorithm, statement analysis algorithm and key data structure for symbolic execution. We also design a specific linked list to deal with uncertain array index and indefinite pointer,which make the analysis result more accurate.(3)In order to achieve the semantic simulation of different statement types, we construct a memory model including stack, heap, and static. We can extract and store the data flow information from the memory model conveniently. We implement the form conversion of path constraints, So that the path condition can be easily solved.(4)We apply ABAZER-SE on three case studies: Juliet test benchmark?Toyota ITC static analysis benchmark and Coreutils, and compare with ABAZER, Cppcheck and KLEE. The experimental results show that it can effectively detect defects in software source code.
Keywords/Search Tags:symbolic execution, GCC, static analysis, precision, defects detection
PDF Full Text Request
Related items