基于符号执行与实际执行的二进制代码执行路径分析

Binary code execution path based on symbolic and actual program execution

应用符号执行方法能够获得程序输入和执行路径的对应关系,这种关系对于分析和测试程序的缺陷是十分重要的。符号执行在针对源码的安全审计中有着成功的应用,但由于其自身的特点导致其很难应用到二进制代码的分析中。该文提出了一种符号执行与实际执行结合的系统模型,解决了符号执行应用于二进制代码分析中的一些难点,在此基础上提出了利用符号执行进行二进制代码分析的新途径。

A system model that combines symbolic and actual execution was developed for path analyses of binary codes to find program bug.A debugger was built to dynamically load a program to obtain the binary code.The transformed system binary code is transformed into expressions containing more information than the assembly code which are useful for symbolic execution.The symbolic code is then executed with the actual code to obtain the path conditions.The symbolic execution analysis of the verification test program links the program's execution path to its unique input.Tests show that the system model can precisely analyze the relationships between the program input and its execution path.