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

Binary code execution path based on symbolic and actual program execution

作　　者：崔宝江[1] 国鹏飞[1] 王建新[2] 

机构地区：[1]北京邮电大学计算机学院,北京100876 [2]北京林业大学信息学院,北京100083

出　　处：《清华大学学报（自然科学版）》2009年第S2期2186-2192,共7页Journal of Tsinghua University(Science and Technology)

基　　金：国家"八六三"高技术项目(2007AA01Z466)

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

关 键 词：符号执行 机器指令解析 路径约束 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]