基于参数约束的分支覆盖符号执行优化算法
2020年信息技术与网络安全第1期
於家伟，李世明，毕雪洁，李秋月，高胜花
（1.哈尔滨师范大学 计算机科学与信息工程学院，黑龙江 哈尔滨 150025； 2.上海市信息安全综合管理技术研究重点实验室，上海 200240）
摘要： 软件质量检测常用的方法是软件测试，符号执行作为主流的测试技术已被广泛应用于学术界与工业界中。但是随着程序规模的增大和函数调用的增加，因某些路径约束条件的特殊性，而难以生成正确的测试用例，从而导致符号执行不能对所有路径做到全覆盖。为了提高符号执行在特殊约束条件对路径的覆盖率等问题，本文提出了基于参数约束的符号执行优化算法。首先，该算法通过搜索收集程序代码中函数的特殊参数，然后利用这些特殊参数作为约束条件，最后将约束条件添加到路径的约束集中。该算法使符号执行生成的测试用例更加精确，从而实现覆盖特殊约束条件下的路径分支，以提高符号执行的精确性和路径覆盖率。在开源符号执行平台CREST中实验并验证上述优化算法，验证及测试结果表明本文提出的算法能够提高符号执行在特殊约束条件下对路径的覆盖率。
中圖分類號：TP311
文獻標識碼：A
DOI： 10.19358/j.issn.2096-5133.2020.01.003
引用格式：於家偉?；趨导s束的分支覆蓋符號執(zhí)行優(yōu)化算法［J］。信息技術與網絡安全，2020,39（1）：14-18.
文獻標識碼：A
DOI： 10.19358/j.issn.2096-5133.2020.01.003
引用格式：於家偉?；趨导s束的分支覆蓋符號執(zhí)行優(yōu)化算法［J］。信息技術與網絡安全，2020,39（1）：14-18.
Optimization of branch covering symbol execution based on constraints
Yu Jiawei，Li Shiming，Bi Xuejie，Li Qiuyue，Gao Shenghua
（1.College of Computer Science and Information Engineering,Harbin Normal University,Harbin 150025,China;2.Shanghai Key Laboratory of Information Security Management Technology Research,Shanghai 200240,China）
Abstract： A common method for software quality inspection is software testing.Symbol execution as a mainstream testing technology has been widely used in academia and industry.However,with the increase in program size and function calls,due to the special nature of certain path constraints,it is difficult to generate correct test cases,which results in symbolic execution not being able to cover all paths.In order to improve the problem of symbol execution on the path coverage under special constraints,this paper proposes a symbolic execution optimization algorithm based on parameter constraints.Firstly,the algorithm collects special parameters of functions in the program code by searching,then uses these special parameters as constraints,and finally adds constraints to the constraint set of the path.This algorithm makes the test cases generated by symbol execution more accurate,so as to achieve path branch coverage under special constraints,to improve the accuracy of symbol execution and path coverage.Experiment is carried out to verify the above optimization algorithm in the open source symbol execution platform CREST.The results of verification and testing show that the algorithm proposed in this paper can improve the path coverage of symbol execution under special constraints.
Key words : symbolic execution;parameter constraint;test case;software test
0 引言
軟件漏洞是軟件中潛藏的代碼缺陷，通過提高檢測代碼的覆蓋率可以提高漏洞的發(fā)現概率，而生成高覆蓋率的測試用例進行檢測漏洞時，若代碼執(zhí)行通過率高時，可認為該程序在一定程度上是可靠的。
作為一種程序測試技術，符號執(zhí)行在軟件測試、程序缺陷挖掘和測試用例生成中得到廣泛的研究和應用，其程序變量是以抽象符號形式來通過符號模擬程序運行并搜集路徑上的約束條件。此外，根據程序的語義、遍歷程序的路徑空間也可用來檢測程序是否滿足一定的安全特性。
輸入約束作為符號執(zhí)行優(yōu)化的方法之一，近年來業(yè)界已取得了一定成果。TRABISH D等人 結合靜態(tài)分析和符號切片技術使符號執(zhí)行能夠搜索到更重要的路徑；GODEFROID P等人提出以調用該執(zhí)行函數生成的摘要作為約束條件來減少代碼的重復執(zhí)行；RAMOS D A等人將約束條件引入到KLEE中，通過檢查被測程序的單個功能而不是整個程序，提高了效率；WONG E等人提出了基于文檔輔助的建模方法，通過自然語言處理和試探法生成文檔并提取約束條件；郭曦等人通過分析路徑邏輯表達式和提取共享表達式來提高狀態(tài)合并的效率；安靖等人通過生成外部調用函數摘要來避免因多次測試外部調用而引起的路徑爆炸問題。
本文詳細內容請下載:http://m.ihrv.cn/resource/share/2000003092
作者信息：
於家偉，李世明，畢雪潔，李秋月，高勝花
（1.哈爾濱師范大學 計算機科學與信息工程學院，黑龍江 哈爾濱 150025；2.上海市信息安全綜合管理技術研究重點實驗室，上海 200240）
此內容為AET網站原創(chuàng)，未經授權禁止轉載。