軟體缺陷模式

基本介紹

• 中文名：
• 外文名：

定義

軟體缺陷概念

模式概念

缺陷模式滿足條件

(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 函式使用檢查、代碼格式錯誤以及性能因素檢查等軟體缺陷。