程序靜態分析

程序靜態分析

程序靜態分析（Program Static Analysis）是指在不運行代碼的方式下，通過詞法分析、語法分析、控制流、數據流分析等技術對程序代碼進行掃描，驗證代碼是否滿足規範性、安全性、可靠性、可維護性等指標的一種代碼分析技術。

目前靜態分析技術向模擬執行的技術發展以能夠發現更多傳統意義上動態測試才能發現的缺陷，例如符號執行、抽象解釋、值依賴分析等等並採用數學約束求解工具進行路徑約減或者可達性分析以減少誤報增加效率。目前的靜態分析工具，無論從科研角度還是實用性角度還有很大的提高餘地，國際最好分析工具誤報率在5-10%之間，能夠報出的缺陷種類也僅有幾百種。我國較好靜態分析工具較少，一些高校正在致力於在此方面的研究和開發（成果較突出的如北京大學等）。

目錄
1分析技術及實踐 靜態分析特點 常用靜態分析技術 2形式化方法
3著名的靜態分析工具 4使用簡介 5使用目的 6用法 FindBugs
PMD CheckStyle BlueMorpho(閃蝶) 7檢查表

分析技術及實踐

程序靜態分析（Program Static Analysis）可以幫助軟體開發人員、質量保證人員查找代碼中存在的結構性錯誤、安全漏洞等問題，從而保證軟體的整體質量。還可以用於幫助軟體開發人員快速理解文檔殘缺的大規模軟體系統以及系統業務邏輯抽取等系統文檔化等領域。如開發20年以上的金融核心COBOL系統，動輒上千萬行代碼的系統規模。對於理解這樣規模的系統，基於程序靜態分析的輔助理解工具就能發揮積極作用。
本文首先對程序靜態分析的特點、常用靜態分析技術、靜態分析實現方式進行描述，然後通過一個實例講解了程序靜態分析的執行過程。

靜態分析特點

程序靜態分析是與程序動態分析相對應的代碼分析技術，它通過對代碼的自動掃描發現隱含的程序問題，主要具有以下特點：
（1）不實際執行程序。動態分析是通過在真實或模擬環境中執行程序進行分析的方法，多用於 性能測試、功能測試、內存泄漏測試等方面。與之相反，靜態分析不運行代碼只是通過對代碼的靜態掃描對程序進行分析。
（2）執行速度快、效率高。目前成熟的代碼靜態分析工具每秒可掃描上萬行代碼，相對於動態分析，具有檢測速度快、效率高的特點。
（3）誤報率較高。代碼靜態分析是通過對程序掃描找到匹配某種規則模式的代碼從而發現代碼中存在的問題，例如可以定位strcpy（）這樣可能存在漏洞的函數，這樣有時會造成將一些正確代碼定位為缺陷的問題，因此靜態分析有時存在誤報率較高的缺陷，可結合動態分析方法進行修正。

常用靜態分析技術

（1）詞法分析：從左至右一個字元一個字元的讀入源程序，對構成源程序的字元流進行掃描，通過使用正則表達式匹配方法將源代碼轉換為等價的符號（Token）流，生成相關符號列表，Lex為常用詞法分析工具。
（2）語法分析：判斷源程序結構上是否正確，通過使用上下文無關語法將相關符號整理為語法樹， Yacc為常用工具。
（3）抽象語法樹分析：將程序組織成樹形結構，樹中相關節點代表了程序中的相關代碼，目前已有javacc/ Antlra等抽象語法樹生成工具。
（4）語義分析：對結構上正確的源程序進行上下文有關性質的審查。
（5）控制流分析：生成有向控制流圖，用節點表示基本代碼塊，節點間的有向邊代表控制流路徑，反向邊表示可能存在的循環；還可生成函數調用關係圖，表示函數間的嵌套關係。
（6）數據流分析：對控制流圖進行遍歷，記錄變數的初始化點和引用點，保存切片相關數據信息。
（7）污點分析：基於數據流圖判斷源代碼中哪些變數可能受到攻擊，是驗證程序輸入、識別代碼表達缺陷的關鍵。
（8）無效代碼分析，根據控制流圖可分析孤立的節點部分為無效代碼。
程序靜態分析是在不執行程序的情況下對其進行分析的技術，簡稱為靜態分析。而程序動態分析則是另外一種程序分析策略，需要實際執行程序。大多數情況下，靜態分析的輸入都是源程序代碼，只有極少數情況會使用目標代碼。靜態分析這一術語一般用來形容自動化工具的分析，而人工分析則往往叫做程序理解。
靜態分析越來越多地被應用到程序優化、軟體錯誤檢測和系統理解領域。Coverity Inc.的軟體質量檢測產品就是利用靜態分析技術進行錯誤檢測的成功代表。國內某軟體公司的閃蝶（BlueMropho）代碼分析平台，是利用程序靜態分析技術專註於大型機遺留系統的代碼理解領域，尤其擅長分析千萬行代碼規模級的COBOL系統。

形式化方法

程序分析中的形式化方法一般指利用純粹嚴格的數學方法對軟體、硬體進行分析的理論及技術。這些數學方法包括符號語義、公理語義、操作語義和抽象解釋。
1952年提出的Rice定理指出，任何關於程序分析的問題都是不可判定的。因此，不存在任何一種機械化的方法能夠證明程序的完全正確性。然而，針對大多數的不可判定問題，仍然可以試圖找到它們的一些近似解。
形式化靜態分析中用到的實現技術有：
模型檢查假設系統是有限狀態的、或者可以通過抽象歸結為有限狀態。
抽象解釋將每條語句的影響模型化為一個抽象機器的狀態。相比實際系統，抽象機器更簡單更容易分析，但其代價是喪失了分析的完備性（並不是原始系統中的每種性質在抽象機器中都是保留的）。抽象解釋當且僅當抽象機器中的每一個性質都能與原始系統中的性質正確映射時，才被稱作可靠（sound）的。
斷言在霍恩邏輯中首次被提出。目前存在一些針對特定程序設計語言的工具，例如ESC/JAVA和ESC/JAVA2中分別使用的SPARK語言和JML語言。

著名的靜態分析工具

Meta-Compilation（Coverity）
由Stanford大學的Dawson Engler副教授等研究開發，該靜態分析工具允許用戶使用一種稱作metal的狀態機語言編寫自定義的時序規則，從而實現了靜態分析工具的可擴展性。MC的實際效果非常優秀，號稱在Linux內核中找出來數百個安全漏洞。MC目前已經商業化，屬於Coverity Inc.2014年被Synopsys收購。目前學術領域比較認可的靜態分析工具，其技術處於領先地位。
mygcc 由一個法國人N. Volanschi開發，其思想來源於MC，試圖將自定義的錯誤檢測集成到編譯時。
Klocwork
國內用的最為廣泛的靜態分析工具，由加拿大北電於1996年研發，是中國最早的能夠檢測語義缺陷的靜態分析工具。截止到2015年其版本號為V10,也就是大家常說的K10
LDRA Testbed
英國的編碼規則類檢測工具，前身為Liverpool大學開發，能夠支持C/C++數千種條目的規則檢測，包括MISRA C/C++, GJB5369等，是最早進入中國市場的靜態分析工具，在軍隊、軍工廣泛使用，但其技術僅支持風格類檢測，無法進行語義缺陷分析，導致一些常用的運行時缺陷無法發現或者較高誤漏報，由此市場佔有率逐步下降。截止到2015年其版本號為9.5
HP Fortify
美國HP公司的支持安全漏洞類的檢測工具，能夠檢測C/C++/Java/PHP/ASP/JavaScript等多種語言，數千種檢測項，是國內使用最為廣泛的靜態分析工具。但該工具整體的誤報漏報率較高，雖然支持很多種安全漏洞，但需要用戶做很多的二次開發工作。
Cobot(庫博)
北京大學軟體工程中心研發的靜態分析工具，能夠支持編碼規則，語義缺陷的程序分析，能夠支持C/C++數千條規則和缺陷的檢測，是我國唯一可以稱的上是靜態分析產品的商業化工具。由於其自主知識產權，對國內的操作系統，編碼標準支持的較好，檢測精度也基本與上述工具持平，所以也得到了很多用戶的認可。2015年通過美國CWE-Compatible 認證，是中國首個也是唯一一個通過該認證的安全檢測產品。
Parasoft C++Test
美國Parasoft公司研發的支持C、C++靜態分析的工具，該工具除了可以檢測編碼規則外，還能檢測少量的語義缺陷，此外能夠進行測試用例生成。

使用簡介

在代碼構建過程中使用靜態分析工具有助於發現代碼缺陷，並提高代碼的質量。本節關注四個代碼靜態分析工具的使用：Findbugs、PMD、Checkstyle、BlueMorpho。前三個工具各有不同的特點，針對開放平台技術。如java, .net , C++. 聯合起來使用有助於減少誤報錯誤，提高報告的準確率。第四個工具有助於理解大規模複雜業務邏輯的COBOL遺留系統。除包含詞法，語法，控制流，數據流分析技術外還引入了人工智慧技術，可自動推薦業務描述，生成業務文檔。

使用目的

這三個工具檢查的側重點各有不同：
本文中三個工具各自的版本分別是：FindBugs 0.85、PMD 2.0和CheckStyle 3.3。這三個工具都可以從sourceforge下載，而且它們都為Eclipse提供了相應的plugin。

用法

關於IDE以及plugin如何使用在此不做介紹，本文主要關注它們如何與ant配合使用，使這些工具成為每次構建過程中的有機組成。

FindBugs

FindBugs的運行環境可能是這四個工具之中最苛刻的了。它工作在j2se1.4.0或以後的版本中，需要至少256MB內存。它的安裝非常簡單，下載之後簡單的解壓即可。為了與ant配合使用，它提供了對應的ant task。

PMD

PMD的運行環境是j2se1.3或以後版本，安裝過程同樣也是解壓即可。對應ant task的使用：
1. 把lib中所有的jar複製到項目的classpath中。
2. 將pmd-2.0.jar中的rulesets解壓到指定目錄，這裡面定義了分析所需要的規則集合。
3. 修改build.xml文件。在這一版本中，提供了2個ant task。一個是pmd使用規則集合進行分析；另一個是檢查代碼中Copy & Paste代碼。這2個任務對應的ant task使用：
PMD任務：
classpathref="classpath"/>
junit_lib/rulesets/imports.xml">
File="pmd_report.html"/>
4. 運行ant pmd和ant cpd即可。
5. 參數說明：
- formatter，指明輸出格式和文件。
- rulesetfiles，指明分析所需的規則文件，不同文件使用逗號分隔。
- failonerror，pmd執行出錯是否中止構建過程。
- failOnRuleViolation，如果與規則衝突，是否中止構建過程。
- classpath，pmd所需的classpath。
- printToConsole，在發現問題時是否列印到ant log或控制台。
- shortFilenames，在輸出報告中是否使用短文件名。
- targetjdk13，是否把目標定為jdk13，如不能使用assert。
- failuresPropertyName，在任務結束時，插入違反規則的號碼
- encoding，讀源文件時所採用的編碼，如utf-8。
關於規則集合的說明，以及如何自定義規則請參見pmd的文檔，文檔中已說得相當清楚。

CheckStyle

使用ant task：
1. 複製checkstyle-all-3.3.jar到項目的classpath中。
2. 修改build.xml文件：
classpath="${weblib.dir}/checkstyle-all-3.3.jar"/>