Font Size: a A A

Research And Improvements On Symbolic Execution

Posted on:2015-05-30Degree:MasterType:Thesis
Country:ChinaCandidate:B ChenFull Text:PDF
GTID:2308330482478944Subject:Computer software and theory
Abstract/Summary:PDF Full Text Request
With the continuous development of computer application, software is widely used in various areas in modern society as the carrier of information systems, and any vulnerability in software will cause highly serious failures. Software testing is the main program analysis to ensure the correctness, completeness, and quality of software. Recent research in software testing suffer from low code coverage problem. Symbolic execution is quickly becoming staple technique that have been gaining popularity in program analysis. In theory, symbolic execution is guaranteed to be effective in achieving high code coverage, yet this generally requires exponential resource which is not practical for many real-world programsThis thesis makes four major contributions.(1) We summarized the basic classification of symbolic execution, including the definition of each kind of symbolic execution, the way how it works and its shortcomings. We presented several recent representative tools that are based on symbolic execution, together with their impact in practice.(2) We researched and summarized the three major problems that reduce the effectiveness of symbolic execution. We presented an overview of techniques that addressed the three problems. We then described the applications of symbolic execution in the fields of test case generation, malware analysis, automatic input filter generation and vulnerability detection.(3) We proposed the three improvements based on offline symbolic execution for binary code’s vulnerability detection:selective symbolic execution, path selecting, and random and incorrect seed input to ease the path explosion and speed up the bug exploration.(4) We implemented Crashmaker, a dynamic symbolic execution tool based on Valgrind and constraints solver STP, integrated with our three improvements measures. We also presented detailed experiments with several Linux binary programs, the evaluation results showed that Crashmaker could effectively find more bugs in a more efficient way.
Keywords/Search Tags:symbolic execution, program analysis, vulnerability detection, automatic, binary code
PDF Full Text Request
Related items