以導引式隨機測試方法探索軟體未規範實作功能

Abstract

軟體測試是軟體開發過程中確保軟體品質最重要的步驟之一， 因在軟體開發的過程中，我們無法保證程式不會發生錯誤。 近年來動靜態程式分析工具的發展已相當成熟，而在 2005 年，更發展出了結合動靜態分析法的導引式隨機測試法。 本論文實作了一個名為 ALERT，結合動靜態分析法的導引式隨機測試平台， 以及其上的軟體未規範實作功能探索模組，以導引式隨機測試方法探索軟體未規範實作功能。 藉由 SAT 模理論 (Satisfiability Modulo Theories) 的定理自動證明函式庫，分析特定的外部輸入所造成的程式流程， 並以控制程式堆疊空間，進一步地操作使用未初始化變數的程式執行結果。 本論文提出兩階段式執行測試方法：第一階段用動態分析工具分析原始程式，取得程式真實的執行資訊。 第二階段使用導引式隨機測試方法，配合第一階段所收集的執行資訊，做分析及推理。 推理所得的結果則為下一輪測試的輸入。 我們不斷重複這兩階段的測式分析，直到找出錯誤或將程式所有執行路徑全數列舉完畢。 我們將此一工具應用於尋找由未初始化變數所造成的程式未規範行為， 成功地萃取出傳統程式分析方法不能找出的軟體行為。 本論文提出的方法改善了現行導引式隨機測試方法中，因修改原始程式碼而造成測試時期和真正執行時期的差距， 提升了測試的精確度。

Testing is one of the most important phases of software quality assurance, for the process of software construction cannot guarantee the absence of bugs. Dynamic and static analysis tools are maturely developed in recent years. In 2005, the concept of concolic (combined word of concrete and symbolic) testing was proposed, which combines static and dynamic program analysis methods. In this thesis, we implement ALERT, a concolic testing framework and an Unspecified Software Feature (USF) Checker based on ALERT. By using automatic theorem prover library for satisfiability modulo theories, we can analyze and determine the inputs to direct program's execution along particular paths. With this mechanism, we can control the values in stack section. It can also be used to manipulate the values of uninitialized variables and to trigger specific behavior of the program. We present a two-phase testing algorithm in this thesis. In the first phase, we use dynamic analysis tool to retrieve real run-time information. In the second phase, we analyze the program by using concolic testing method with the data collected in the first phase. The result generated by the prover will be the input for the next testing run. This testing process iterates until a fault is found or all the program execution paths are enumerated. We use this tool to resolve unspecified program features caused by uninitialized variables. It successfully extracts the program behavior which cannot be found with traditional program analysis methods. The method in this thesis resolves the information lost problem caused by source code instrumentation in the process of testing and improves the accuracy of the test.