定義
軟體缺陷模式是對發生的不斷重複的或類似的軟體缺陷中發現和抽象出的規律描述。
此定義適用於軟體生命周期中任何階段引入的軟體缺陷。
軟體缺陷概念
軟體缺陷的定義繁多,以下介紹幾個比較常用的軟體缺陷的定義:
(1)國標GB/T11457-89“軟體工程術語”是等同採用IEEE STD729-1983制定的,IEEE軟體工程術語中對軟體缺陷(software defect)的定義為:1)從產品內部看,軟體缺陷是軟體產品開發或維護過程中所存在的錯誤、偏差等各種問題;2)從外部看,軟體缺陷是系統所需要實現的某種功能的失效或違背。
(2)SW-CMM是這樣定義軟體缺陷的:”系統或系統成分中的能造成它們無法實現其被要求的功能的缺點。如果在執行過程中遇到缺陷,它可能導致系統的失效”。
(3)在IEEE的軟體可信性度量的標準辭彙(IEEE982.1-2005 Standard Dictionary of Measures of the SoftwareAspects of Dependability)中對軟體缺陷的定義為:一個通用術語,涉及軟體故障原因和失效影響。
(4)國內軟體可靠性工程領域廣泛使用的定義為:軟體缺陷是存在於軟體中的、不期望的或不可接受的偏差,其結果是當軟體運行於某一特定條件時將出現軟體故障(即軟體缺陷被激活),軟體缺陷以一種靜態的形式存在於軟體的內部,是軟體開發過程中人為錯誤的結果。軟體缺陷的例子有:數組下標不對、循環變數初值設定有誤、異常處理方法有誤等。
模式概念
模式這一概念最早出現在城市建築領域,ChristopherAlexander的一本關於建築的書中明確給出了模式的概念,他說:“每一個模式描述了一個在我們周圍不斷重複發生的問題,以及該問題的解決方案的核心,這樣你就能一次又一次地使用該方案而不必做重複勞動”,他使用模式這一概念來解決建築中的一些問題。隨後,模式在構造複雜系統時的重要性逐漸在其他領域中得到認可。模式是針對複雜系統中重複出現的問題而提出來的。有經驗的專家在解決問題時,通常先考慮以前解決過的相似問題,並重用其解法的精華來解決問題,這個不斷被引用的解法就是通常說的模式。
缺陷模式滿足條件
缺陷模式滿足的條件如下:
(1)軟體缺陷模式在實際工程中是存在的 。
(2)依據缺陷模式所定義缺陷的數量有限。
(3) 至少存在一種算法,能夠利用缺陷模式匹配算法檢測出所定義的軟體缺陷。
靜態軟體缺陷檢測技術
詞法分析
詞法分析是對源程式進行詞法分析,將其轉化成單詞流,然後與已定義的模式進行匹配,若匹配成功,則認為是缺陷,其原理和實現比較簡單。詞法分析只能檢測出固定的軟體缺陷,檢測出的數量很有限,而且不能保證漏報率和誤報率。
類型推導
類型推導是指利用機器自動推導的程式推導出程式中變數與函式的類型。主要的思想是將程式中的數據劃分為不同的集合,每個集合按照一定規則,若將每個固定的集合作為一種類型,就能利用類型理論中的算法對其進行推導,其目的是保證每個推導操作都是針對合適的對象類型進行的,從而保證操作的有效性。類型推導主要適用和控制流無關的分析,能夠處理大規模程式,且具有良好的擴展性,但是它不能很好的解決與控制流相關的分析。
模型檢測
模型檢測是由 Clarke、Emerson、Savakis、Quenelle 在 1981 年提出的,主要的思想是對軟體系統構造狀態機或者構造相應的抽象模型,然後在對構造後的系統進行遍歷,驗證系統的某種性質,是一種驗證有限狀態並發系統的方法。該方法能夠對程式中的複雜語義進行檢測,從而能夠準確而高效的定位出程式中的缺陷。模型檢測在很多方面得到了很好的套用,但是在軟體測試中,由於軟體自身具有高度的複雜性,所以該方法只能對程式某個特性構造抽象模型進行檢測。
定理證明
定理證明是程式驗證技術中常用的技術,是一種基於語義程式的驗證技術。主要的思想是將驗證求解的方法轉化為數學上的定理證明,然後判斷程式的抽象公式是否滿足某個特定的屬性。由於定理證明在處理有理數域和整數域上的運算極其的複雜,且在定理判斷的過程中需要人工添加很多注釋條件,不能自動的或半自動的判定缺陷程式缺陷,因而不能夠得到廣泛的運用。
符號執行
符號執行是一種白盒測試方法,其主要的思想是用抽象符號來表示程式中變數的值,進而模擬程式的執行,通過將程式的所有執行路徑抽象成符號表達式,然後對每個特定的路徑輸入抽象符號,通過約束求解輸出每個符號,最後判斷程式的行為是否錯誤。按照模擬程式的所有執行路徑,求得跟蹤變數所有可能的值,進而發現程式中的邏輯錯誤。但是隨著程式規模的擴大,執行路徑的數目很多,不能跟蹤所有路徑下變數可能的值,因此不能對所有路徑進行分析。
抽象解釋
抽象解釋理論是由 R.Cousot 和 P.Cousot 提出的一種算法,該算法通過選取逼近程式不動點語義來對程式進行分析。求解程式最小不動點一般是不可判定的,程式的輸入和輸出不可判定性使得無法求解程式的最小不動點。因此需要尋找到一個合適的抽象函式,作用於特定的抽象域,對某個特定的屬性進行考察。雖然抽象區間域沒有具體域準確,但是它減少了計算的規模和難度,增加了計算的可能性。如果找到抽象域上的最小不動點,就可以將映射後的具體域作為函式的最小不動點。
基於規則的檢查
基於規則的檢查是指不同的應用程式中,可能存在不同的編碼規則,我們可以首先利用規則處理器來處理具體的規則,然後將其轉化為程式的內部表示,最後將其用於程式的靜態分析。基於規則檢查的優點是對不同的系統進行分析時,可以利用相對應的規則進行檢查,然後定為出程式中的軟體缺陷。但是由於規則數量有限,只能分析少量特定類型的軟體缺陷,不能檢測大部分的缺陷。
常用的靜態缺陷檢測工具
PolySpace Verifier
PolySpace Verifier是由 PolySpace 公司開發,用於檢測運行時軟體缺陷。該軟體是利用顏色進行缺陷級別的分類,橙色代表程式中可能存在缺陷,紅色代表軟體缺陷,灰色代表無法執行的代碼,綠色代表程式中沒有軟體缺陷。它能夠檢測,空指針引用、未初始化局部變數、數組越界、緩衝區溢出等軟體缺陷。
Splint
Splint是開源的靜態軟體缺陷檢測工具,用於檢測用標準C實現的軟體缺陷。通過在原始碼中添加關於函式、參數和類型的格式化注釋,實現了未使用的聲明、類型不一致、使用未定義變數、記憶體泄露、不可達代碼、函式返回值、無限循環、危險的別名等軟體缺陷。
Klocwork K8
Klocwork K8是由 Klocwork 公司開發的,支持 C/C++,JAVA,它能檢測緩衝區溢出、記憶體泄露、安全漏洞等軟體缺陷。
Findbugs
Findbugs是一個基於 java 語言的靜態分析工具,它主要檢查類或者 JAR 檔案。其主要思想是利用位元組碼與軟體缺陷模式對比來尋找矛盾點,從而發現程式中的軟體缺陷。它提供了自定義檢測器功能,利用 Byte Code Engineering Library實現基於 visitor 模式位元組碼的掃描,並且通過載入 xml 檔案的方式進行管理。
Coverity Prevent
Coverity Prevent是由 Coverity 公司研發的,支持 C/C++,java 語言的靜態缺陷檢測工具。它能夠檢測多種軟體缺陷,如空指針引用、釋放後指針引用、多次釋放指針引用、未初始化變數、緩衝區溢出、整形溢出,安全編碼等軟體缺陷。
PMD
PMD是一款採用 BSD 協定發布的 Java 程式代碼檢查工具,其核心是 javacc解析器。該工具可以做到檢查 Java 代碼中是否含有未使用的變數、是否含有空的抓取塊、是否含有不必要的對象、複雜表達式、複雜代碼等軟體缺陷。而且其易於擴展,利用 xpath 或者 java 語言編寫新的缺陷檢測器。
CodeSonar
CodeSonar是由 Gramma Tech 公司開發的 C/C++代碼靜態缺陷檢測工具,可以檢測出導致系統崩潰、記憶體衝突的各種嚴重的錯誤,包括空指針引用、緩衝區溢出等軟體缺陷。它還可以分析全部的程式,考慮不同檔案中不同函式之間的調用關係,可以檢測出傳統測試方法很難發現的錯誤。
Inspector
Inspector是由 Reasoning 公司開發的 C/C++代碼靜態缺陷檢測工具。它能夠檢測出不可達代碼、記憶體釋放異常等軟體缺陷。能很好的檢測出八類軟體缺陷,但該工具漏報率和誤報率比較高。
SafePro
SafePro是由北京航空航天大學研發的 C/C++等語言的靜態軟體測試工具。通過對程式的靜態分析,能夠提供程式數據流,控制流,程式語句覆蓋測試、分支測試等方面的信息,使得用戶可以快捷有效的理解程式結構,發現程式中的軟體缺陷,提高軟體質量。該系統是個高度擴展的系統,用戶可以變形 xml 或者java 語言對其進行擴展。
PG_Relief
PG_Relief是由富士通公司和南京大學合作開發的 C/C++靜態軟體缺陷檢測系統和度量統計系統,通過對程式進行靜態分析,查找程式中可能存在的缺陷,最後統計程式的複雜度和規模。
Object Broser
Object Broser是由 System Integrator Corporation 公司和北京科技大學合作開發的 java 語言靜態缺陷檢測工具。通過對 java 程式進行分析,檢測程式中的可能缺陷,並對部分缺陷自動改進,減少軟體缺陷機率,並統計程式的複雜度和規模。
Cppcheck
Cppcheck 是一種開源的 C/C++代碼缺陷靜態檢查工具。不同於 C/C++編譯器及其它分析工具,Cppcheck 只檢查編譯器檢查不出來的 bug,不檢查語法錯誤。它能檢測出自動變數檢查、數組邊界檢查、class 類檢查、過期的函式,廢棄函式檢查、異常記憶體使用,釋放檢查、記憶體泄露檢查、作業系統資源釋放檢查、異常STL 函式使用檢查、代碼格式錯誤以及性能因素檢查等軟體缺陷。