代碼分析技術程序靜態分析01分析技術實踐靜態分析工具形式化方法使用簡介目錄03020405使用目的檢查表用法目錄0706基本信息程序靜態分析（ProgramStaticAnalysis）是指在不運行代碼的方式下，通過詞法分析、語法分析、控制流、數據流分析等技術對程序代碼進行掃描，驗證代碼是否滿足規范性、安全性、可靠性、可維護性等指標的一種代碼分析技術。靜態分析技術向模擬執行的技術發展以能夠發現更多傳統意義上動態測試才能發現的缺陷，例如符號執行、抽象解釋、值依賴分析等等并采用數學約束求解工具進行路徑約減或者可達性分析以減少誤報增加效率。靜態分析工具，無論從科研角度還是實用性角度還有很大的提高余地，國際最好分析工具誤報率在5-10%之間，能夠報出的缺陷種類也僅有幾百種。我國較好靜態分析工具較少，一些研究所與高校正在致力于在此方面的研究和開發（成果較突出的如北京大學、中科院、清華大學等）。分析技術實踐常用靜態分析靜態分析特點分析技術實踐靜態分析特點程序靜態分析是與程序動態分析相對應的代碼分析技術，它通過對代碼的自動掃描發現隱含的程序問題，主要具有以下特點：（1）不實際執行程序。動態分析是通過在真實或模擬環境中執行程序進行分析的方法，多用于性能測試、功能測試、內存泄漏測試等方面。與之相反，靜態分析不運行代碼只是通過對代碼的靜態掃描對程序進行分析。（2）執行速度快、效率高。成熟的代碼靜態分析工具每秒可掃描上萬行代碼，相對于動態分析，具有檢測速度快、效率高的特點。（3）誤報率較高。代碼靜態分析是通過對程序掃描找到匹配某種規則模式的代碼從而發現代碼中存在的問題，例如可以定位strcpy（）這樣可能存在漏洞的函數，這樣有時會造成將一些正確代碼定位為缺陷的問題，因此靜態分析有時存在誤報率較高的缺陷，可結合動態分析方法進行修正。常用靜態分析（1）詞法分析：從左至右一個字符一個字符的讀入源程序，對構成源程序的字符流進行掃描，通過使用正則表達式匹配方法將源代碼轉換為等價的符號（Token）流，生成相關符號列表，Lex為常用詞法分析工具。（2）語法分析：判斷源程序結構上是否正確，通過使用上下文無關語法將相關符號整理為語法樹，Yacc為常用工具。（3）抽象語法樹分析：將程序組織成樹形結構，樹中相關節點代表了程序中的相關代碼，已有javacc/Antlra等抽象語法樹生成工具。（4）語義分析：對結構上正確的源程序進行上下文有關性質的審查。（5）控制流分析：生成有向控制流圖，用節點表示基本代碼塊，節點間的有向邊代表控制流路徑，反向邊表示可能存在的循環；還可生成函數調用關系圖，表示函數間的嵌套關系。（6）數據流分析：對控制流圖進行遍歷，記錄變量的初始化點和引用點，保存切片相關數據信息。（7）污點分析：基于數據流圖判斷源代碼中哪些變量可能受到攻擊，是驗證程序輸入、識別代碼表達缺陷的關鍵。（8）無效代碼分析，根據控制流圖可分析孤立的節點部分為無效代碼。形式化方法形式化方法程序分析中的形式化方法一般指利用純粹嚴格的數學方法對軟件、硬件進行分析的理論及技術。這些數學方法包括符號語義、公理語義、操作語義和抽象解釋。1952年提出的Rice定理指出，任何關于程序分析的問題都是不可判定的。因此，不存在任何一種機械化的方法能夠證明程序的完全正確性。然而，針對大多數的不可判定問題，仍然可以試圖找到它們的一些近似解。形式化靜態分析中用到的實現技術有：模型檢查假設系統是有限狀態的、或者可以通過抽象歸結為有限狀態。抽象解釋將每條語句的影響模型化為一個抽象機器的狀態。相比實際系統，抽象機器更簡單更容易分析，但其代價是喪失了分析的完備性（并不是原始系統中的每種性質在抽象機器中都是保留的）。抽象解釋當且僅當抽象機器中的每一個性質都能與原始系統中的性質正確映射時，才被稱作可靠（sound）的。斷言在霍恩邏輯中首次被提出。存在一些針對特定程序設計語言的工具，例如ESC/JAVA和ESC/JAVA2中分別使用的SPARK語言和JML語言。靜態分析工具靜態分析工具Meta-Compilation（Coverity）由Stanford大學的DawsonEngler副教授等研究開發，該靜態分析工具允許用戶使用一種稱作metal的狀態機語言編寫自定義的時序規則，從而實現了靜態分析工具的可擴展性。MC的實際效果非常優秀，號稱在Linux內核中找出來數百個安全漏洞。MC已經商業化，屬于CoverityInc.2014年被Synopsys收購。學術領域比較認可的靜態分析工具，其技術處于領先地位。mygcc由一個法國人N.Volanschi開發，其思想來源于MC，試圖將自定義的錯誤檢測集成到編譯時。Klocwork國內用的最為廣泛的靜態分析工具，由加拿大北電于1996年研發，是中國最早的能夠檢測語義缺陷的靜態分析工具。截止到2015年其版本號為V10,也就是大家常說的K10LDRATestbed英國的編碼規則類檢測工具，前身為Liverpool大學開發，能夠支持C/C++數千種條目的規則檢測，包括MISRAC/C++,GJB5369等，是最早進入中國市場的靜態分析工具，在軍隊、軍工廣泛使用，但其技術僅支持風格類檢測，無法進行語義缺陷分析，導致一些常用的運行時缺陷無法發現或者較高誤漏報，由此市場占有率逐步下降。使用簡介使用簡介在代碼構建過程中使用靜態分析工具有助于發現代碼缺陷，并提高代碼的質量。本節四個代碼靜態分析工具的使用：Findbugs、PMD、Checkstyle、BlueMorpho。前三個工具各有不同的特點，針對開放平臺技術。如java,,C++.聯合起來使用有助于減少誤報錯誤，提高報告的準確率。第四個工具有助于理解大規模復雜業務邏輯的COBOL遺留系統.除包含詞法，語法，控制流，數據流分析技術外還引入了人工智能技術，可自動推薦業務描述，生成業務文檔。使用目的使用目的這三個工具檢查的側重點各有不同：本文中三個工具各自的版本分別是：FindBugs0.85、PMD2.0和CheckStyle3.3。這三個工具都可以從sourceforge下載，而且它們都為Eclipse提供了相應的plugin。用法用法關于IDE以及plugin如何使用在此不做介紹，本文主要它們如何與ant配合使用，使這些工具成為每次構建過程中的有機組成。FindBugsFindBugs的運行環境可能是這四個工具之中最苛刻的了。它工作在j2se1.4.0或以后的版本中，需要至少256MB內存。它的安裝非常簡單，下載之后簡單的解壓即可。為了與ant配合使用，它提供了對應的anttask。PMDPMD的運行環境是j2se1.3或以后版本，安裝過程同樣也是解壓即可。對應anttask的使用：1.把lib中所有的jar復制到項目的classpath中。2.將pmd-中的rulesets解壓到指定目錄，這里面定義了分析所需要的規則集合。3.修改build.xml文件。在這一版本中，提供了2個anttask。一個是pmd使用規則集合進行分析；另一個是檢查代碼中Copy&Paste代碼。檢查表檢查表-為每個工具建立自己的目錄和classpath變量。由于這些工具大多都使用了相同的開源軟件，很容易會因為使用相同軟件包的不同版本而相互干擾。這種問題非常隱蔽，在這種問題上花費時間和精力是非常不值得的。通過建立不同的目錄和classpath，然后在對應的anttask中引用各自的classpath，可以有效的避免它。-將這些工具納入項目的配置