邹权臣， 吴润浦， 马金鑫， 王欣， 辛伟， 侯长玉， 李美聪

(1.中国信息安全测评中心，北京 100085； 2. 360安全研究院，北京 100016；3. 北京中测安华科技有限公司，北京 100085)

在符号执行中，对路径约束条件的可达性判定以及生成实际的测试输入都严重依赖于可满足模理论(SMT)求解器. 虽然当前的SMT求解器已经能够处理较大型的约束，但对复杂约束的处理能力不足，而且随着约束体积的增大，求解的效率会越显低下；这使得约束求解问题成为了符号执行中的主要瓶颈问题之一.

约束求解问题的研究关系着符号执行的效率和性能，影响着符号执行应用到大型应用程序中. 同时，这方面的研究对漏洞挖掘、自动化网络攻防等领域也具有非常重要的意义.

本文介绍了符号执行和约束求解的基本概念，并分析了符号执行中约束求解问题的由来，对近年来的约束求解问题研究进展进行了归类，展望和总结.

1 符号执行与约束求解

1.1 SMT理论

可满足模理论(satisfiability modulo theories， SMT)主要用于自动化演绎的研究方法，是为了检验基于逻辑理论的一阶谓词公式的可满足性而提出[1]，已经被广泛应用于模型检测、自动化测试生成等计算机科学领域. 典型的应用理论主要包括了各种形式的算术运算、数组、有限集、比特向量、代数数据类型(algebraic datatypes)、字符串、浮点数以及各种理论的结合等.

相对于SAT(boolean satisfiability problem)求解器，SMT求解器不仅仅支持布尔运算符，而且在使用SMT求解器解决问题的时候不需要把问题转化成复杂的CNF(conjunctive normal form)范式，能大幅度简……