1.本发明设计自动化软件测试中的符号执行方法领域，具体设计一种基于机器学习技术的符号执行框架。
背景技术：2.符号执行作为一种用于自动化软件测试的程序分析技术，在遍历程序的过程中，收集路径条件并将其转化成约束的形式，将其提供给约束求解器以获得可行的解决方案。然而，在将符号执行应用到大型且复杂的程序上时，仍然存在着可扩展性和实用性低的窘况。造成以上情况的主要原因是约束求解耗时过长。约束求解作为符号执行的关键推动者的同时也是其最主要的性能瓶颈，但它实际上是一个计算起来十分困难的问题。目前主流的符号执行引擎使用的约束求解器通常基于可满足性模理论(satisfiability modulo theory，smt)，即smt求解器，例如z3和cvc4。它们将符号执行过程中收集的路径约束转换成smt公式后，再通过smt求解器检查其可满足性，只有对可满足的路径约束输入触发其执行路径的输入值。在真实世界的程序中，通常包含大量的非线性结构、函数调用以及各种具有挑战性的理论。因此，实现在短时间内对具有挑战性的程序完成遍历并生成触发路径的输入值逐渐难以实现。现有的符号执行工具通过设置时间阈值的方式终止求解时间过程的路径约束，放弃超过时间阈值的求解过程，导致了大量的无效求解过程。
技术实现要素：3.针对现有技术的不足，本发明提出一种基于机器学习技术的符号执行方法，利用机器学习算法—k最近邻算法对路径约束的可解性进行分类，优先求解分类结果为可解的约束。具体技术方案如下：
4.基于机器学习技术的符号执行方法，该方法包括如下步骤：
5.步骤1：构建包含类别的路径约束特征数据集并为数据分配权重；具体如下步骤所示：
6.步骤1.1：利用符号执行工具在其自身设定的时间阈值t内测试m个程序(p1,p2,...,pm)，记录求解时长超过时间阈值t(t＜t)的路径约束所对应的smt-lib格式文件，并根据求解结果将其分为可解和不可解两类，c＝{c1,c2}；
7.步骤1.2：定义n个关键特征并对步骤1.1中得到的smt-lib格式文件提取特征，将各特征值映射至[0,1]的范围内，形成可以代表路径约束特点的特征向量x＝rn，得到样本库d＝{d1,d2,...,dn},其中n代表样本的总个数；
[0008]
步骤1.3：根据测试程序与历史程序(已经测试完成的程序)之间的相似性为步骤1.2中得到的样本库d中的各个样本赋予权重w(w1,w2,...,wn)。
[0009]
步骤2：加权knn利用步骤1中得到的样本库d学习路径约束与其可解性之间的关系，构建路径约束分类器；
[0010]
步骤3：对待测试程序进行符号执行的过程中，如果当前路径约束能在某个较小的
时间阈值t内成功求解，则与传统的符号执行过程相同，输出触发当前路径的输入值；如果没有完成求解过程，则触发步骤2中的路径约束分类器，转入步骤4；
[0011]
步骤4：在当前路径约束对应的smt-lib文件上提取特征，得到特征向量，并利用加权knn对其进行可解性的分类，如果分类结果为可解，则继续送入约束求解器中进行求解；如果不可解，则放弃当前求解过程，可以选择对所有路径都处理完成后再次进行求解；
[0012]
步骤5：将步骤4中经过求解验证的具有真实求解结果的路径约束添加到加权knn的样本库中，扩充数据集并根据预测损失更新样本权重，接着转入步骤3探索下一条程序路径，直至整个程序遍历结束。
[0013]
进一步的，步骤1.1中所述的可解性是指路径约束能否被约束求解器在时间阈值内完成求解并输出触发当前路径的具体输入值，可解指smt求解器返回sat的情况，而不可解则意味着smt求解器返回unknown和unsat两种情况。
[0014]
进一步的，所述的步骤1.3中计算测试程序与历史程序之间的相似性具体步骤为：
[0015]
步骤1.3.1：将测试程序与历史程序分别看作文本，利用文本嵌入工具word2vec对其进行嵌入，得到e(e,e1,e2,...,em)，并利用余弦相似度公式计算得到p与pi(i＝1,2,...,m)之间的相似度s(s1,s2,...,sm)，以此作为为样本数据赋予初始权重的基准，为来自同一程序的样本赋予相同的权重，余弦相似度计算公式如下所示：
[0016]
其中i表示历史程序的编号；
[0017]
步骤1.3.2：最后为了使权重总和为1，利用如下公式对步骤1.3.1中得到的所有样本的权重进行规范化：
[0018]
其中wi代表第i个样本对应的权重；
[0019]
进一步的，所述的步骤4中使用加权knn对约束的可解性分类的具体步骤包括：例如与样本库中样本di的距离为：
[0020][0021]
步骤4.2：对步骤4.1中的dist进行排序，并选出离pc最近的k个样本，将最近邻的k个样本及其相应的类别组成集合
[0022]
步骤4.3：基于权重w和距离dist计算出pc属于各类的概率pr，计算公式如下所示其中为指示函数，如下公式所示：其中表示dk中第i个样本的所属类别；
[0023]
步骤4.4：最终将pc归到最大pr所对应的类别，共有两种类别，可解和不可解。
[0024]
与最接近的现有技术相比，本发明的有益效果如下：
[0025]
1.本发明基于加权knn算法实现了路径约束可解性的分类器，并将其嵌入到符号
执行框架中，在符号执行的过程中，对于超过一定求解时间阈值的路径约束进行可解性的预测，如果其可解，则送入约束求解器中正常求解，如果分类结果为不可解，则暂时放弃当前求解过程，可以选择对所有路径都处理完成后求解，能够减少大量的无效求解过程，提高符号执行应用到大型程序时的实用性以及效率。
[0026]
2.本发明对加权knn样本库中的样本根据被测程序与历史程序之间的相似性赋予权重，并基于预测损失对权重进行更新，将在符号执行过程中产生的属于当前程序的路径约束添加至样本库中，有利于提高对路径约束可解性分类的准确性。
附图说明
[0027]
图1是本实施例基于机器学习技术的符号执行方法的流程示意图。
[0028]
图2是本实施例对路径约束可解性进行分类的流程示意图。
具体实施方式
[0029]
下面根据附图和优选的实施例进一步详细描述本发明，此处所描述的具体实施例仅用于解释本发明，但并不因此而限制本发明的保护范围。
[0030]
如图1所示，基于机器学习技术的符号执行方法，该方法包括如下步骤：
[0031]
步骤1：构建包含类别的路径约束特征数据集并为数据分配权重；具体如下步骤所示：
[0032]
步骤1.1：利用符号执行工具在其自身设定的时间阈值t内测试m个程序(p1,p2,...,pm)，记录求解时长超过时间阈值t(t＜t)的路径约束所对应的smt-lib格式文件，并根据求解结果将其分为可解和不可解两类，c＝{c1,c2}；
[0033]
进一步的，所述的可解性是指路径约束能否被约束求解器在时间阈值内完成求解并输出触发当前路径的具体输入值，可解指smt求解器返回sat的情况，而不可解则意味着smt求解器返回返回unknown和unsat两种情况。
[0034]
步骤1.2：定义n个关键特征并对步骤1.1中得到的smt-lib格式文件提取特征，将各特征值映射至[0,1]的范围内，形成可以代表路径约束特点的特征向量x＝rn，得到样本库d＝{d1,d2,...,dn},其中n代表样本的总个数；
[0035]
步骤1.3：根据测试程序与历史程序(已经测试完成的程序)之间的相似性为步骤1.2中得到的样本库d中的各个样本赋予权重w(w1,w2,...,wn)。
[0036]
计算测试程序与历史程序之间的相似性具体步骤为：
[0037]
步骤1.3.1：将测试程序与历史程序分别看作文本，利用文本嵌入工具word2vec对其进行嵌入，得到e(e,e1,e2,...,em)，并利用余弦相似度公式计算得到p与pi(i＝1,2,...,m)之间的相似度s(s1,s2,...,sm)，以此作为为样本数据赋予初始权重的基准，为来自同一程序的样本赋予相同的权重，余弦相似度计算公式如下所示：
[0038]
其中i表示历史程序的编号；
[0039]
步骤1.3.2：最后为了使权重总和为1，利用如下公式对步骤1.3.1中得到的所有样本的权重进行规范化：
[0040]
其中wi代表第i个样本对应的权重；
[0041]
步骤2：加权knn利用步骤1中得到的样本库d学习路径约束与其可解性之间的关系，构建路径约束分类器；
[0042]
步骤3：对待测试程序进行符号执行的过程中，如果当前路径约束能在某个较小的时间阈值t内成功求解，则与传统的符号执行过程相同，输出触发当前路径的输入值；如果没有完成求解过程，则触发步骤2中的路径约束分类器，转入步骤4；
[0043]
步骤4：在当前路径约束对应的smt-lib文件上提取特征，得到特征向量，并利用加权knn对其进行可解性的分类，如果分类结果为可解，则继续送入约束求解器中进行求解；如果不可解，则放弃当前求解过程，可以选择对所有路径都处理完成后再次进行求解；
[0044]
所述的使用加权knn对约束的可解性分类的具体步骤包括：例如与样本库中样本di的距离为：
[0045][0046]
步骤4.2：对步骤4.1中的dist进行排序，并选出离pc最近的k个样本，将最近邻的k个样本及其相应的类别组成集合
[0047]
步骤4.3：基于权重w和距离dist计算出pc属于各类的概率pr，计算公式如下所示其中为指示函数，如下公式所示：其中表示dk中第i个样本的所属类别；
[0048]
步骤4.4：最终将pc归到最大pr所对应的类别，共有两种类别，可解和不可解。
[0049]
步骤5：将步骤4中经过求解验证的具有真实求解结果的路径约束添加到加权knn的样本库中，扩充数据集并根据预测损失更新样本权重，接着转入步骤3探索下一条程序路径，直至整个程序遍历完成
[0050]
本实施例上述方法，在对程序进行软件测试的过程中，符号执行基于机器学习技术实现判断路径约束的可解性，可以快速预测约束模型的可解性，进而放弃求解预测结果为不可解的路径约束，避免不必要的约束求解过程，从而提高符号执行效率。
[0051]
实施例1：
[0052]
下面将首先列举使用符号执行工具angr作为基础嵌入路径约束分类器，对来自gnu coreutils 9.0中的10个程序进行测试，同时以angr对其进行符号执行作为原始求解时间对照。然后将说明符号执行引擎的整体测试结果，对本发明进一步详细说明。
[0053]
angr中设置smt约束求解器为z3，采用相同的时间阈值t为300秒，本发明中的时间阈值t设置为2秒，只对求解时长超过2秒的路径约束进行可解性的预测，如果结果为可解，则在300秒内再次对其求解。
[0054]
实验结果如表1所示。最终，与没集成路径约束可解性分类模块的符号执行工具angr相比，针对不同的程序本发明减少了20.7％到67.9％的时间开销。相比之下，在处理大
型程序时本发明具有更优的表现，并且本文所提出的路径约束可解性分类器可以与大多数符号执行引擎相结合，只要它们使用smt-lib规范。
[0055]
表1.符号执行时间对比
[0056][0057]
最后应当说明的是：以上所述仅是本发明的较佳实施例，并非对本发明作任何形式上的限制。尽管参照前述实例对本发明进行了详细的阐述，但是对于本领域的研究人员来说，其依然可以对前述各实例记载的技术方案进行小幅度修改，或者对其中部分技术特征进行同等替换。凡是在发明的精神和原则之内，所做的修改、等同变化以及修改等均应落在本发明技术方案包含的范围内。
技术特征：1.基于机器学习技术的符号执行方法，其特征在于，该方法包括以下步骤：步骤1：构建包含类别的路径约束特征数据集并为数据分配权重；具体如下步骤所示：步骤1.1：利用符号执行工具在其自身设定的时间阈值t内测试m个程序(p1,p2,...,p
m
)，记录求解时长超过时间阈值t(t＜t)的路径约束所对应的smt-lib格式文件，并根据求解结果将其分为可解和不可解两类，c＝{c1,c2}；步骤1.2：定义n个关键特征并对步骤1.1中得到的smt-lib格式文件提取特征，将各特征值映射至[0,1]的范围内，形成可以代表路径约束特点的特征向量x＝r
n
，得到样本库d＝{d1,d2,...,d
n
},其中n代表样本的总个数；步骤1.3：根据测试程序与历史程序(已经测试完成的程序)之间的相似性为步骤1.2中得到的样本库d中的各个样本赋予权重w(w1,w2,...,w
n
)。步骤2：加权knn利用步骤1中得到的样本库d学习路径约束与其可解性之间的关系，构建路径约束分类器；步骤3：对待测试程序进行符号执行的过程中，如果当前路径约束能在某个较小的时间阈值t内成功求解，则与传统的符号执行过程相同，输出触发当前路径的输入值；如果没有完成求解过程，则触发步骤2中的路径约束分类器，转入步骤4；步骤4：在当前路径约束对应的smt-lib文件上提取特征，得到特征向量，并利用加权knn对其进行可解性的分类，如果分类结果为可解，则继续送入约束求解器中进行求解；如果不可解，则放弃当前求解过程，对所有路径都处理完成后再次进行求解；步骤5：将步骤4中经过求解验证的具有真实求解结果的路径约束添加到加权knn的样本库中，扩充数据集并根据预测损失更新样本权重，接着转入步骤3探索下一条程序路径，直至整个程序遍历结束。2.根据权利要求1所述的基于机器学习技术的符号执行方法，其特征在于，步骤1.1中所述的可解性是指路径约束能否被约束求解器在时间阈值内完成求解并输出触发当前路径的具体输入值，可解指smt求解器返回sat的情况，而不可解则意味着smt求解器返回unknown和unsat两种情况。3.根据权利要求1所述的基于机器学习技术的符号执行方法，其特征在于，所述的步骤1.3中计算测试程序与历史程序之间的相似性具体步骤为：步骤1.3.1：将测试程序与历史程序分别看作文本，利用文本嵌入工具word2vec对其进行嵌入，得到e(e,e1,e2,...,e
m
)，并利用余弦相似度公式计算得到p与p
i
(i＝1,2,...,m)之间的相似度s(s1,s2,...,s
m
)，以此作为样本数据赋予初始权重的基准，为来自同一程序的样本赋予相同的权重，余弦相似度计算公式如下所示：其中i表示历史程序的编号；步骤1.3.2：最后为了使权重总和为1，利用如下公式对步骤1.3.1中得到的所有样本的权重进行规范化：其中w
i
代表第i个样本对应的权重。
4.根据权利要求1所述的基于机器学习技术的符号执行方法，其特征在于，所述的步骤4中使用加权knn对约束可解性分类的具体步骤包括：步骤4.1：首先利用欧氏距离计算当前路径约束pc与样本库中各个数据之间的距离dist，例如与样本库中样本d
i
的距离为：步骤4.2：对步骤4.1中的dist进行排序，并选出离pc最近的k个样本，将最近邻的k个样本及其相应的类别组成集合步骤4.3：基于权重w和距离dist计算出pc属于各类的概率pr，计算公式如下所示其中为指示函数，如下公式所示：其中表示d
k
中第i个样本的所属类别；步骤4.4：最终将pc归到最大pr所对应的类别，共有两种类别，可解和不可解。5.根据权利要求1所述的基于机器学习技术的符号执行方法，其特征在于，所述的步骤5中权重更新策略具体为：若预测结果与真实求解结果一致则相应的增加d
k
中与其同类样本的权重(w
i
'＝w
i
*(1+α),α∈(0,1),i＝1,...,n)，否则降低(w
i
'＝w
i
*(1-α),α∈(0,1),i＝1,...,n)，其中α设置为0.2，将具有真实求解结果的路径约束添加到样本库d中并为其赋予较高的权重β＝0.6，最后对所有样本的权重进行规范化。
技术总结本发明公开一种基于机器学习技术的符号执行方法，该方法利用机器学习技术—加权K最近邻算法(KNN)学习程序路径约束与其可解性之间的关系，并使用其对超过一定求解时间阈值的路径约束进行可解性的预测，从而指导符号执行引擎是否继续当前的求解过程，使用符号执行过程中产生的具有真实求解结果的路径约束填充样本库并根据程序间的相似性为样本库中的数据赋予以及根据预测误差更新权重。本发明在SMT-LIB格式的文件上提取特征，具有平台无关性，且能够减少符号执行过程中大量无效的约束求解过程，提高符号执行应用到大型程序时的实用性。用性。用性。
技术研发人员：李晓光 李知桦
受保护的技术使用者：辽宁大学
技术研发日：2022.07.26
技术公布日：2022/11/1
