基于參數約束的分支覆蓋符號執行優化算法
2020年信息技術與網絡安全第1期
於家偉，李世明，畢雪潔，李秋月，高勝花
（1.哈爾濱師范大學 計算機科學與信息工程學院，黑龍江 哈爾濱 150025； 2.上海市信息安全綜合管理技術研究重點實驗室，上海 200240）
摘要： 軟件質量檢測常用的方法是軟件測試，符號執行作為主流的測試技術已被廣泛應用于學術界與工業界中。但是隨著程序規模的增大和函數調用的增加，因某些路徑約束條件的特殊性，而難以生成正確的測試用例，從而導致符號執行不能對所有路徑做到全覆蓋。為了提高符號執行在特殊約束條件對路徑的覆蓋率等問題，本文提出了基于參數約束的符號執行優化算法。首先，該算法通過搜索收集程序代碼中函數的特殊參數，然后利用這些特殊參數作為約束條件，最后將約束條件添加到路徑的約束集中。該算法使符號執行生成的測試用例更加精確，從而實現覆蓋特殊約束條件下的路徑分支，以提高符號執行的精確性和路徑覆蓋率。在開源符號執行平臺CREST中實驗并驗證上述優化算法，驗證及測試結果表明本文提出的算法能夠提高符號執行在特殊約束條件下對路徑的覆蓋率。
中圖分類號：TP311
文獻標識碼：A
DOI： 10.19358/j.issn.2096-5133.2020.01.003
引用格式：於家偉。基于參數約束的分支覆蓋符號執行優化算法［J］。信息技術與網絡安全，2020,39（1）：14-18.
文獻標識碼：A
DOI： 10.19358/j.issn.2096-5133.2020.01.003
引用格式：於家偉。基于參數約束的分支覆蓋符號執行優化算法［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 引言
軟件漏洞是軟件中潛藏的代碼缺陷，通過提高檢測代碼的覆蓋率可以提高漏洞的發現概率，而生成高覆蓋率的測試用例進行檢測漏洞時，若代碼執行通過率高時，可認為該程序在一定程度上是可靠的。
作為一種程序測試技術，符號執行在軟件測試、程序缺陷挖掘和測試用例生成中得到廣泛的研究和應用，其程序變量是以抽象符號形式來通過符號模擬程序運行并搜集路徑上的約束條件。此外，根據程序的語義、遍歷程序的路徑空間也可用來檢測程序是否滿足一定的安全特性。
輸入約束作為符號執行優化的方法之一，近年來業界已取得了一定成果。TRABISH D等人 結合靜態分析和符號切片技術使符號執行能夠搜索到更重要的路徑；GODEFROID P等人提出以調用該執行函數生成的摘要作為約束條件來減少代碼的重復執行；RAMOS D A等人將約束條件引入到KLEE中，通過檢查被測程序的單個功能而不是整個程序，提高了效率；WONG E等人提出了基于文檔輔助的建模方法，通過自然語言處理和試探法生成文檔并提取約束條件；郭曦等人通過分析路徑邏輯表達式和提取共享表達式來提高狀態合并的效率；安靖等人通過生成外部調用函數摘要來避免因多次測試外部調用而引起的路徑爆炸問題。
本文詳細內容請下載:http://www.jysgc.com/resource/share/2000003092
作者信息：
於家偉，李世明，畢雪潔，李秋月，高勝花
（1.哈爾濱師范大學 計算機科學與信息工程學院，黑龍江 哈爾濱 150025；2.上海市信息安全綜合管理技術研究重點實驗室，上海 200240）
此內容為AET網站原創，未經授權禁止轉載。