基于静态符号执行的数值软件缺陷检测方法及装置

专利主权项内容

1.一种基于静态符号执行的数值软件缺陷检测方法，其特征在于，该方法包括：输入所述待测程序，解析待测程序的抽象语法树，构造控制流图；将缺陷检测器加载至符号执行引擎，置于所述待测程序的控制流入口，其中，所述缺陷检测器中含有基于缺陷定义设定的缺陷产生条件，所述缺陷产生条件包括基于浮点缺陷定义设定的浮点缺陷产生条件，所述符号执行引擎含有支持浮点类型的部分，所述支持浮点类型的部分包括支持浮点类型的符号值表示、支持浮点类型操作的表达式表示、支持浮点类型的内存表示、支持浮点类型的约束求解器和数学函数建模模块，所述数学函数建模模块用于对数学函数进行建模以使得数据函数能够被所述符号执行引擎识别；由符号执行引擎通过路径敏感方式遍历所述控制流图，逐路径符号化地执行待测程序，以获得变量或表达式的约束范围并收集程序中的语义信息，并在通过路径敏感方式执行待测程序过程中生成用于记录待测程序的每个节点的状态的扩展图；在符号化地执行待测程序的过程中，在当前分支路径的输入含有数学函数的情况下，将数学函数与符号值进行绑定，并在数学函数的输入参数为浮点类型参数的情况下，基于函数输出属性对输入的数学函数进行分类，基于分类结果计算输入参数对应的输出值域范围，将该值域范围作为约束范围与数学函数的符号值进行绑定，并基于绑定的值域范围生成分支路径的新的状态，并将生成的新状态添加至扩展图中；基于符号值或表达式的约束范围使用基于范围的第一约束求解器来进行约束求解来探索所述待测程序中的可达路径，并使用第二约束求解器来验证基于范围的第一约束求解器的约束求解结果，由缺陷检测器基于经验证的约束求解结果探索所述待测程序中的可达路径，得到浮点缺陷检测结果。