第九講靜態(tài)代碼的可信性分析概述

1、靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 1/45高級軟件工程高級軟件工程靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 2/45高級軟件工程高級軟件工程機(jī)能完整機(jī)能完整?易生何病易生何病?什么性格什么性格?道德水準(zhǔn)道德水準(zhǔn)?從靜態(tài)代碼分析動態(tài)特性：從靜態(tài)代碼分析動態(tài)特性：靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 3/45高級軟件工程高級軟件工程主要考慮如何發(fā)現(xiàn)代碼缺陷！主要考慮如何發(fā)現(xiàn)代碼缺陷！需要首先知道：需要首先知道： 可能存在什么樣的代碼缺陷！可能存在什么樣的代碼缺陷！缺陷缺陷 與與 約束約束: 什么是對的（約束：什么是對的（約束：Constraint） 什么是不對的

2、（缺陷：什么是不對的（缺陷：Defect）靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 4/45高級軟件工程高級軟件工程不論不論 是是 人工人工 還是還是 自動自動都需要：都需要： 利用利用 已有的缺陷知識已有的缺陷知識 查找查找 某個特定程序某個特定程序靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 5/45高級軟件工程高級軟件工程內(nèi)內(nèi) 容容一、靜態(tài)代碼缺陷查找的角色一、靜態(tài)代碼缺陷查找的角色二、靜態(tài)代碼缺陷基本類別二、靜態(tài)代碼缺陷基本類別三、靜態(tài)代碼缺陷查找的主要方法三、靜態(tài)代碼缺陷查找的主要方法 四、靜態(tài)代碼缺陷查找的常見工具四、靜態(tài)代碼缺陷查找的常見工具五、理論基礎(chǔ)：不動點(diǎn)五、理

3、論基礎(chǔ)：不動點(diǎn)靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 6/45高級軟件工程高級軟件工程Product (Artifact)AnalyzingDesigningCodingCompilingDeployingDeveloping ProcessMaintaining靜態(tài)分析靜態(tài)分析動態(tài)測試動態(tài)測試模型檢測模型檢測在線監(jiān)測在線監(jiān)測V&V一、靜態(tài)代碼缺陷查找的角色一、靜態(tài)代碼缺陷查找的角色Review!靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 7/45高級軟件工程高級軟件工程l離線運(yùn)行程序l應(yīng)用最廣泛的缺陷查找技術(shù)對功能性最有效工作量大：微軟（半數(shù)的測試人員？）自動程度難以

4、提高l基本分類黑盒白盒許多缺陷靠運(yùn)行很難暴露：死瑣等許多缺陷靠運(yùn)行很難暴露：死瑣等靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 8/45高級軟件工程高級軟件工程l不運(yùn)行程序(廣義測試包含這類活動)l靜態(tài)分析可以涉及更多的路徑組合測試一次只能有一個執(zhí)行軌跡l可以分析多種屬性死瑣？安全漏洞?性能屬性?l源碼？目標(biāo)碼？靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 9/45高級軟件工程高級軟件工程l當(dāng)系統(tǒng)正在為用戶提供服務(wù)時，一般不能當(dāng)系統(tǒng)正在為用戶提供服務(wù)時，一般不能進(jìn)行測試：輸入受限進(jìn)行測試：輸入受限l但可以進(jìn)行檢測，獲取各種狀態(tài)、事件但可以進(jìn)行檢測，獲取各種狀態(tài)、事件l進(jìn)行分析，并可能據(jù)

5、此調(diào)整目標(biāo)系統(tǒng)進(jìn)行分析，并可能據(jù)此調(diào)整目標(biāo)系統(tǒng)l盡量減少對系統(tǒng)的應(yīng)用盡量減少對系統(tǒng)的應(yīng)用l與靜態(tài)分析結(jié)合？與靜態(tài)分析結(jié)合？靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 10/45高級軟件工程高級軟件工程二、靜態(tài)代碼缺陷類別二、靜態(tài)代碼缺陷類別l與具體應(yīng)用“無關(guān)”詞法或者語法共性特性（共性特性（死鎖、空指針、內(nèi)存泄露、數(shù)組越界死鎖、空指針、內(nèi)存泄露、數(shù)組越界）公共庫用法（公共庫用法（順序、參數(shù)、接口實(shí)現(xiàn)，容錯，安全順序、參數(shù)、接口實(shí)現(xiàn)，容錯，安全）l與具體應(yīng)用“相關(guān)”類型定義（操作格式，不含其它信息（信息隱藏）類型約束（類型約束（調(diào)用的順序、參數(shù)值，接口實(shí)現(xiàn)調(diào)用的順序、參數(shù)值，接口實(shí)現(xiàn)）需求

6、相關(guān)（正確）靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 11/45高級軟件工程高級軟件工程l與具體應(yīng)用無關(guān)與具體應(yīng)用無關(guān)詞法或者語法：語言設(shè)計人員詞法或者語法：語言設(shè)計人員 共性特性：共性特性： 基礎(chǔ)知識基礎(chǔ)知識 公共庫用法：庫開發(fā)人員（形成文擋）公共庫用法：庫開發(fā)人員（形成文擋） 用戶整理用戶整理(分析實(shí)現(xiàn)代碼、分析使用代碼分析實(shí)現(xiàn)代碼、分析使用代碼) l與具體應(yīng)用相關(guān)與具體應(yīng)用相關(guān)類型定義：類型定義： 應(yīng)用設(shè)計人員應(yīng)用設(shè)計人員類型約束：類型約束： 應(yīng)用設(shè)計人員、編程人員應(yīng)用設(shè)計人員、編程人員需求相關(guān)：需求相關(guān)： 用戶用戶靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 12/45高級

7、軟件工程高級軟件工程1、靜態(tài)代碼分析2、編譯過程中的代碼缺陷查找3、形式化分析方法4、缺陷模式匹配三、靜態(tài)代碼缺陷查找的主要方法三、靜態(tài)代碼缺陷查找的主要方法靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 13/45高級軟件工程高級軟件工程l靜態(tài)代碼缺陷查找屬于靜態(tài)代碼分析的范疇l靜態(tài)代碼分析是在不運(yùn)行代碼的前提下，獲取關(guān)于程序信息的過程l靜態(tài)代碼分析還可以用于獲取設(shè)計結(jié)構(gòu)理解代碼功能演化代碼1、靜態(tài)代碼分析、靜態(tài)代碼分析靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 14/45高級軟件工程高級軟件工程給定一個程序，可以問許多問題：給定一個程序，可以問許多問題： 對于某個輸入，停機(jī)嗎對于某

8、個輸入，停機(jī)嗎? 執(zhí)行過程需要多少內(nèi)存執(zhí)行過程需要多少內(nèi)存? 對于某個輸入的輸出是什么對于某個輸入的輸出是什么? 變量 x 被使用前是否已經(jīng)初始化過了 變量 x 的值將來被讀取嗎? 變量 x 的值是否一直大于0？ 變量 x 的值取值范圍是多少？ 變量 x 的當(dāng)前值是什么時候賦予的? 指針p會是空嗎?靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 15/45高級軟件工程高級軟件工程Rices 定理定理 (1953) 非正式地指出：非正式地指出：所有關(guān)于程序所有關(guān)于程序“行為行為”的問題是不可判定的的問題是不可判定的(undecidable)例如：能否判定如下變量例如：能否判定如下變量 x 的值

9、的值?x = 17; if (TM(j) x = 18;第第 j 個圖靈機(jī)的停機(jī)問題是不可判定的個圖靈機(jī)的停機(jī)問題是不可判定的x的值也就不能判定的值也就不能判定靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 16/45高級軟件工程高級軟件工程在完備、準(zhǔn)確解難以求得的情況下只能追求部分、近似解這 是現(xiàn)實(shí)的道路 也是十分有用的道路主要途徑包括：類型檢驗(yàn)形式化方法缺陷模式匹配靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 17/45高級軟件工程高級軟件工程最基本的代碼分析l詞法分析l語法分析抽象語法樹 （AST）l類型檢驗(yàn)語義分析？變量賦值、調(diào)用操作、類型變換 等靜態(tài)代碼的可信性分析概述靜態(tài)代碼

10、的可信性分析概述 18/45高級軟件工程高級軟件工程l某些具有相同某些具有相同/相似特性實(shí)例的集合相似特性實(shí)例的集合值的集合？操作的集合？值的集合？操作的集合？l基本類型基本類型整數(shù)、實(shí)數(shù)、枚舉、字符、布爾整數(shù)、實(shí)數(shù)、枚舉、字符、布爾l自定義自定義結(jié)構(gòu)、抽象數(shù)據(jù)、面向?qū)ο蠼Y(jié)構(gòu)、抽象數(shù)據(jù)、面向?qū)ο鬄槭裁匆?？便于理解？為什么要引入？便于理解？幫助人們發(fā)現(xiàn)錯誤！幫助人們發(fā)現(xiàn)錯誤！l靜態(tài)類型化語言靜態(tài)類型化語言每個表達(dá)式在靜態(tài)程序分析時都是確定的每個表達(dá)式在靜態(tài)程序分析時都是確定的l強(qiáng)類型化語言強(qiáng)類型化語言所有表達(dá)式的類型是一致的（可以在運(yùn)行時檢驗(yàn)）所有表達(dá)式的類型是一致的（可以在運(yùn)行時檢驗(yàn)）實(shí)際

11、編寫代碼時，這是被編譯器檢查出來的一類常見錯誤！實(shí)際編寫代碼時，這是被編譯器檢查出來的一類常見錯誤！靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 19/45高級軟件工程高級軟件工程形式化軟件分析是一種基于數(shù)學(xué)的“自動化”技術(shù)：給出一個特定行為的精確描述，該技術(shù)可以“準(zhǔn)確地”對軟件的語義進(jìn)行推理(Model Checking)抽象解釋(Abstract Interpretation)定理證明(Theorem Proving)符號執(zhí)行(Symbolic Execution)靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 20/45高級軟件工程高級軟件工程l基于“有限狀態(tài)自動機(jī)”理論l從代碼中

12、抽取有限狀態(tài)轉(zhuǎn)換系統(tǒng)模型，用來表示目標(biāo)系統(tǒng)的行為l適合檢驗(yàn)“并發(fā)”等時序方面的特性l對于值域等類型的分析比較困難狀態(tài)爆炸靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 21/45高級軟件工程高級軟件工程抽象解釋抽象解釋l一種基于“格”理論的框架l許多形式化分析方法都可以被涵蓋其中l(wèi)主要適合 數(shù)據(jù)流分析（Data Flow Analysis）尤其是對循環(huán)、遞歸等l主要思想是對代碼進(jìn)行“近似”，將不可判定問題進(jìn)行模擬靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 22/45高級軟件工程高級軟件工程定理證明定理證明(Theorem Proving)l演繹方法（Deductive Methods）

13、l基于Floyd/Hoare 邏輯l用如下形式表示程序的狀態(tài)P C Q C: 可執(zhí)行代碼 P: Pre-condition，執(zhí)行前的狀態(tài)屬性 Q: Post-condition，執(zhí)行后的狀態(tài)屬性l利用推理/證明機(jī)制解決 語句復(fù)合問題靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 23/45高級軟件工程高級軟件工程l通過使用抽象的符號表示程序中變量的值來模擬程序的執(zhí)行，克服了變量的值難以確定的問題l跟蹤各路徑上變量的可能取值，有可能發(fā)現(xiàn)細(xì)微的邏輯錯誤l程序較大時，可能的路徑數(shù)目增長會很快。可以選取重要的路徑進(jìn)行分析靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 24/45高級軟件工程高級軟件

14、工程l事先收集足夠多的共性缺陷模式事先收集足夠多的共性缺陷模式l用戶僅輸入待檢測代碼就可以用戶僅輸入待檢測代碼就可以l與與”類型化類型化”方法關(guān)系密切方法關(guān)系密切l(wèi)比較實(shí)用比較實(shí)用l容易產(chǎn)生容易產(chǎn)生“誤報誤報”靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 25/45高級軟件工程高級軟件工程l準(zhǔn)確？準(zhǔn)確？漏報（漏報（False Negative, not Complete）誤報（誤報（False Positive, not Sound）l缺陷知識哪里來缺陷知識哪里來程序自帶程序自帶工具提供工具提供l基本方法基本方法基于形式化基于形式化基于缺陷模式基于缺陷模式靜態(tài)代碼的可信性分析概述靜態(tài)代碼的

15、可信性分析概述 26/45高級軟件工程高級軟件工程lJPF 模型檢測lBandera lSlam, BLAST, CMClESC/JavalASTREElPREfix定理證明定理證明(Theorem Proving)模型檢測模型檢測(Model Checking)抽象解釋抽象解釋(Abstract Interpretation)符號執(zhí)行符號執(zhí)行(Symbolic Execution)靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 27/45高級軟件工程高級軟件工程lJlint 主要采用數(shù)據(jù)流分析技術(shù)，速度快 沒有誤報lFindBugs 內(nèi)置較多的缺陷模式 有較好的應(yīng)用（google）lPMD

16、 格式為主，可以靈活增加新缺陷模式 以抽象語法樹為基礎(chǔ)建立 lCoverify 主要針對操作系統(tǒng)lCODA 正在開發(fā)中靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 28/45高級軟件工程高級軟件工程l各自優(yōu)勢不同l綜合使用多種分析方法l在準(zhǔn)確度與時間開銷上進(jìn)行折中l(wèi)集成？靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 29/45高級軟件工程高級軟件工程l擴(kuò)展類型思路l攜帶檢驗(yàn)信息（頭文件與配置文件）Java Annotation靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 30/45高級軟件工程高級軟件工程五、理論基礎(chǔ)：不動點(diǎn)五、理論基礎(chǔ)：不動點(diǎn)1、偏序2、格3、不動點(diǎn)靜態(tài)代碼的可信

17、性分析概述靜態(tài)代碼的可信性分析概述 31/45高級軟件工程高級軟件工程一個偏序是一個數(shù)學(xué)結(jié)構(gòu)一個偏序是一個數(shù)學(xué)結(jié)構(gòu): L = ( S, )其中，其中， S 是一個集合，是一個集合， (小于等于小于等于) 是是 S 上的一個二元上的一個二元關(guān)系關(guān)系，且滿足如下條件：且滿足如下條件： 自反(Reflexivity): x S : x x 傳遞(Transitivity): x, y, z S : x y y z x z 反對稱(Anti-symmetry): x, y S : x y y x x = y靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 32/45高級軟件工程高級軟件工程假設(shè) X S

18、. y S 是X的上界(upper bound), 記作 X y, 如果： x X : x y類似地： y S 是 X 的下界(lower bound), 記作 y X, 如果： x X : y x定義最小上界（least upper bound） X:X X (y S : X y X y)定義最大下界 （greatest lower bound） X： X X (y S : y X y X)靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 33/45高級軟件工程高級軟件工程一個格是一個偏序集一個格是一個偏序集 S，且滿足：，且滿足： 對于所有的子集對于所有的子集 X S， X 與與 X 都存

19、在都存在一個格一定有： 唯一的一個最大元素 (top) ： = S 唯一的一個最小元素(bottom)： = S.由于最小上界和最大下界的唯一性，可以將求 x 和 y 的最小上界和最大下界定義為 x 和 y 的二元運(yùn)算：最小上界: x y 最大下界: x y為什么？為什么？靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 34/45高級軟件工程高級軟件工程靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 35/45高級軟件工程高級軟件工程l對于任何一個有限集合 A，可以定義一個格 (2A,), 其中， = , = A, x y = x y, x y = x y 格的高度是從 到 的最長路徑。例

20、如：上面冪集格的高度是4。一般地：格 (2A,) 的高度是 |A|.靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 36/45高級軟件工程高級軟件工程一個函數(shù) f : L L 是單調(diào)的 (monotone), 當(dāng):x, y S : x y f(x) f(y)單調(diào)函數(shù)不一定是遞增的:常量函數(shù)也是單調(diào)的多個單調(diào)函數(shù)的復(fù)合仍然是單調(diào)函數(shù)如果將 與 看作函數(shù),則它們都是單調(diào)的靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 37/45高級軟件工程高級軟件工程對于一個高度有限的格 L 每個單調(diào)函數(shù) f 有唯一的一個最小不動點(diǎn): fix (f) = f i () i0那么: f (fix (f) = f

21、ix (f)證明: 1) f () 2) f () f 2 () 3) f () f 2 () 4) L 高度有限, 因此對于某個 k: f k () = f k+1 () 5) 靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 38/45高級軟件工程高級軟件工程計算一個不動點(diǎn)的時間復(fù)雜度依賴于 3 個因素: 格的高度 計算 f 的代價; 測試等價的代價.一個不動點(diǎn)的計算可以表示為格中,從 開始向上搜索的過程靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 39/45高級軟件工程高級軟件工程如果 L1,L2, . . . ,Ln 是有限高度的格,那么乘積( product)為為:L1 L2 .

22、 . . Ln = (x1, x2, . . . , xn) | xi Li其中 是逐點(diǎn)對應(yīng)的. 與 可以被逐點(diǎn)計算height (L1 . . . Ln) = height (L1) + . . . + height (Ln)靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 40/45高級軟件工程高級軟件工程和操作:L1 + L2 + . . . + Ln = (i, xi) | xi Li, , (i, x) (j, y) 當(dāng)且僅當(dāng): i = j 且 x y. height (L1 + . . . + Ln) = maxheight (Li).靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 41/45高級軟件工程高級軟件工程如果 L 是一個有限高度的格, 那么 lift (L) 是:高度： height (lift (L) = height (L) + 1.靜態(tài)代碼的可信性分析概述靜態(tài)代碼的可信性分析概述 42/45高級軟件工程高級軟件工程如果 A 是一個有限集合，那么 flat (A) :a1 a2 an 是一個高度為2的格靜態(tài)代碼的可信性分析概述靜態(tài)代碼