程式靜態分析（Program Static Analysis）是指在不運行代碼的方式下，通過詞法分析、語法分析、控制流、數據流分析等技術對程式代碼進行掃描，驗證代碼是否滿足規範性、安全性、可靠性、可維護性等指標的一種代碼分析技術。目前靜態分析技術向模擬執行的技術發展以能夠發現更多傳統意義上動態測試才能發現的缺陷，例如符號執行、抽象解釋、值依賴分析等等並採用數學約束求解工具進行路徑約減或者可達性分析以減少誤報增加效率。目前的靜態分析工具，無論從科研角度還是實用性角度還有很大的提高餘地，國際最好分析工具誤報率在5-10%之間，能夠報出的缺陷種類也僅有幾百種。我國較好靜態分析工具較少，一些高校正在致力於在此方面的研究和開發（成果較突出的如北京大學等）。
基本介紹
- 中文名：程式靜態分析
- 外文名：Program Static Analysis
- 目的：保證軟體的整體質量
- 特點：不實際執行程式
分析技術及實踐,靜態分析特點,常用靜態分析技術,形式化方法,著名的靜態分析工具,使用簡介,使用目的,用法,FindBugs,PMD,CheckStyle,BlueMorpho(閃蝶),檢查表,
分析技術及實踐
程式靜態分析（Program Static Analysis）可以幫助軟體開發人員、質量保證人員查找代碼中存在的結構性錯誤、安全漏洞等問題，從而保證軟體的整體質量。還可以用於幫助軟體開發人員快速理解文檔殘缺的大規模軟體系統以及系統業務邏輯抽取等系統文檔化等領域。 如開發20年以上的金融核心COBOL系統，動輒上千萬行代碼的系統規模。對於理解這樣規模的系統，基於程式靜態分析的輔助理解工具就能發揮積極作用。
本文首先對程式靜態分析的特點、常用靜態分析技術、靜態分析實現方式進行描述，然後通過一個實例講解了程式靜態分析的執行過程。
靜態分析特點
程式靜態分析是與程式動態分析相對應的代碼分析技術，它通過對代碼的自動掃描發現隱含的程式問題，主要具有以下特點：
（2）執行速度快、效率高。目前成熟的代碼靜態分析工具每秒可掃描上萬行代碼，相對於動態分析，具有檢測速度快、效率高的特點。
（3）誤報率較高。代碼靜態分析是通過對程式掃描找到匹配某種規則模式的代碼從而發現代碼中存在的問題，例如可以定位strcpy（）這樣可能存在漏洞的函式，這樣有時會造成將一些正確代碼定位為缺陷的問題，因此靜態分析有時存在誤報率較高的缺陷，可結合動態分析方法進行修正。
常用靜態分析技術
（2）語法分析：判斷源程式結構上是否正確，通過使用上下文無關語法將相關符號整理為語法樹， Yacc為常用工具。
（4）語義分析：對結構上正確的源程式進行上下文有關性質的審查。
（6）數據流分析：對控制流圖進行遍歷，記錄變數的初始化點和引用點，保存切片相關數據信息。
（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任務：
<target name="pmd">
<!-- 定義任務和任務所屬類所在的classpath引用 -->
<taskdef name="pmd" classname="net.sourceforge.pmd.ant.PMDTask"
classpathref="classpath"/>
<!-- 檢查使用的規則檔案 -->
<pmd rulesetfiles="junit_lib/rulesets/imports.xml">
<!-- 輸出格式和檔案名稱 -->
<formatter type="html" toFile="pmd_report.html"/>
<!-- pmd所需要依賴包的classpath引用 -->
<classpath refid="classpath"/>
<!-- 要檢查的項目源檔案根目錄 -->
<fileset dir="src">
<include name="**/*.java"/>
</fileset>
</pmd>
</target>
CPD任務：
<target name="cpd">
<!-- 定義任務和任務所屬類所在的classpath -->
<taskdef name="cpd" classname="net.sourceforge.pmd.cpd.CPDTask"
classpathref="classpath"/>
<!-- 指明輸出檔案和判斷屬於copy & paste的標準 -->
<cpd minimumTokenCount="100" outputFile="cpd.txtl">
<!-- 要檢查的項目源檔案根目錄 -->
<fileset dir="src">
<include name="**/*.java"/>
</fileset>
</cpd>
</target>
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檔案：
<taskdef resource="checkstyletask.properties"
classpath="${weblib.dir}/checkstyle-all-3.3.jar"/>
<target name="checkstyle" depends="init">
<!-- 指明checkstyle的分析所需的規則檔案 -->
<checkstyle config="checkstyle33.xml">
<!-- 要檢查的檔案 -->
<fileset dir="${src.code}" includes="**/*.java"/>
<!-- 指明輸出格式和檔案名稱 -->
<formatter type="xml" toFile="report.xml"/>
</checkstyle>
<!-- 將xml檔案轉換成html檔案 -->
<style in="report.xml" out="report.html" style="checkstyle-frames"/>
</target>
3. 運行ant checkstyle即可。
checkstyle的規則檔案，即項目的代碼規範，建議不要手工書寫。可以使用checkstyle plug in在Eclipse配置後再導出。Checkstyle提供了預設的xslt，用來進行xml的格式轉換。它們都放在contrib目錄中。Checkstyle同樣也提供了自定義的check，但與PMD相比，書寫要複雜。詳細情況請參見checkstyle的文檔。
BlueMorpho(閃蝶)
BlueMorpho是獨立運行的B/S程式，安裝簡單，無需額外配置參數檔案。
- 在Windows下運行Bluemorpho windows安裝包,注意有32位和64位兩個版本,
- 安裝完成後，在開始-程式-BlueMorpho資料夾里運行Sart bluemorho server啟動分析server.
- Server啟動後，在開始-程式-BlueMorpho資料夾里運行BlueMorpho即可訪問閃蝶源碼分析平台。
- BlueMoropho提供兩種方式上傳source code, 手工上傳和同步從Mainframe下載COBOL源碼。
- 代碼上傳或下載到BlueMorpho以後，即可點擊任意程式進行源碼分析。
檢查表
- 為每個工具建立自己的目錄和classpath變數。由於這些工具大多都使用了相同的開源軟體，很容易會因為使用相同軟體包的不同版本而相互干擾。這種問題非常隱蔽，在這種問題上花費時間和精力是非常不值得的。通過建立不同的目錄和classpath，然後在對應的ant task中引用各自的classpath，可以有效的避免它。
