The Processing Of External Enviroments In Symbolic Execution

With the development of software testing, much higher requirements in codecoverage analysis is needed and system reliability validations are becoming more rigidthan ever before. Dynamic Symbolic Execution (DSE) is a novel approach in softwaretesting and program verification which instruments binary image of program at runtimethus makes the testing results more accurate and universal to common usage. Symbolicexecution is based on the theories of automation and formalization which usuallycombined with model checking and program abstraction to get thorough coverage insoftware testing.Earlier on, DSE can only be applied to analyze linear programs and simplevariables, but with the progress of solving theory, DSE can handle more complexsituation such as procedure calls and structures. But inherently, DSE still has manydrawbacks needs to be overcome. Among them, path explosion and external functioncalls are the most prominent. Execution paths of a program grows exponentially with itsscale, therefore it’s not practical to solve such an astronomical problem, especially forlarge applications, this is the so called scalability bottle neck. Programs often interactwith external environments, on the one hand, totally symbolize would increase thescope of research rapidly which leads to path explosion in the end. On the other hand,it’s not always possible to know the calling signatures of external functions. Therebyanalyzers have no way to understand what happened for those black boxes.This thesis mainly focuses on the handling of external function calls in DSE. Thereare two reasons for choosing this topic: firstly, it’s widely believed that elegantproceeding of external function calls would significantly reduce the scale of programneed to be analyzed accordingly would mitigate the path explosion problem. Secondly,to establish reliable results via DSE, external function calls are an inevitable hurdle tocross in search of more accurate analysis. Unfortunately, present handlings of externalfunction calls in DSE using modeling or hybrid executions are either insufficient orinadequate.Here we propose a new approach dealing with external function calls in DSE, this paper mainly contributes at:Divide handling of external function calls in DSE into six models. Based on theanalyzing of these models, this paper proposes a new hybrid model which distinguishesfrom former ones in performance and accuracy. This hybrid model creatively divide theexecution space into concrete and symbolic, combined with delay concretization toachieve only necessary concretization to avoid premature ones which lead to falsepositive and data dependence to assist higher coverage. Later on, a prototype systemSMArt Fuzzing tool for Windows native Executables or SMAFE for short,is built oninstrument platform Pin and SMT solver STP to validate our proposal. Results areanalyzed, especially for the divergence of testing paths.