基于动态符号执行的二进制程序缺陷发现系统

Dynamic symbolic execution based defect detection system for binary programs

以对二进制程序进行自动化缺陷发现为目标,基于软件虚拟机的动态二进制翻译机制和污点传播机制,对符号计算需要关注的程序运行时语义信息提取、中间语言符号计算等机制进行了研究,改进了传统动态符号执行的路径调度部分,分析了程序缺陷的符号断言表达形式,构建了一个在线式的动态符号执行系统检测二进制程序中的缺陷。实验验证了该方法在实际程序缺陷发现中的有效性。

Aiming towards automatic defect detection for binary programs, based on software virtual machine＇ s dynamic bina- ry translation and taint propagation, this paper studied mechanisms necessary for symbolic execution including program＇ s run- time semantics＇ extraction, intermediate language based symbolic calculation, enhanced the path-scheduling mechanism in traditional dynamic symbolic execution, analyzed symbolic asserts＇ expressions for common program defects, with an online dynamic symbolic execution system built up detecting defects in binary programs. Experiments prove the method＇ s effective- ness in defect detection for real binary programs.