文章目錄

• 前言
• Static Analysis
• • Rice’s Theorem
  • Sound & Complete
  • Sound 示例
  • 小結(jié)
• 抽象和過近似（Abstraction + Over-approximate）
• • 靜態(tài)分析示例
  • 抽象
  • 過近似
  • • 轉(zhuǎn)換函數(shù)（Transfer Functions）
    • 控制流處理（Control Flow handling）
• 總結(jié)

---

前言

??????本系列文章源自于南大李老師的軟件分析課程，僅作為個人總結(jié)。
??????靜態(tài)程序分析（static program analysis），是一種方法或者技術(shù)用來在執(zhí)行一個程序之前對該程序的行為和某些感興趣的屬性進(jìn)行分析的手段。比如判斷：1，是否存在私有信息泄露？2，是否存在對空指針的間接引用？3，強(qiáng)制類型轉(zhuǎn)換是否安全？4，兩個變量是否可以指向同一塊內(nèi)存？5，斷言語句是否成功？6，是否存在死代碼需要進(jìn)行消除？

Static Analysis

Rice’s Theorem

??????“Any non-trivial property of the behavior of programs in a r.e. language is undecidable.”（r.e. (recursively enumerable) = recognizable by a Turing-machine）–Rice’s Theorem

??????也就是說，對于那些上面提到的 non-trivial 屬性，并不能準(zhǔn)確判斷程序是否滿足這些屬性。所以為了得到一些東西，就應(yīng)該舍棄一些別的東西。

Sound & Complete

??????假設(shè)一個程序存在7處地方和我們感興趣的某種屬性有關(guān)，我們想通過靜態(tài)分析方法找出它們：如果一個靜態(tài)分析方法具有 Sound 屬性時，指的是它常常會報出 N>=7 處結(jié)果（絕對包含有正確的7處），在其中有幾處地方是我們不感興趣的，屬于靜態(tài)分析方法判斷時產(chǎn)生了失誤，稱其為誤報（false-positive）；如果一個靜態(tài)分析方法具有 Sound 屬性時，指的是它常常會報出 N<=7 處結(jié)果（是正確的7處的子集），這N處地方都是我們想要的結(jié)果，但是還有幾處地方靜態(tài)分析并沒有找到，這也屬于靜態(tài)分析方法判斷時產(chǎn)生了失誤，稱其為漏報（false-negative）。前者稱其為過近似（Over-approximate），后者稱之為 Under-approximate。
??????一般采用的靜態(tài)分析方法都是犧牲掉 Complete ,保留 Sound 。這樣得到結(jié)果雖然會有誤報，但是這個結(jié)果中包含有所有的正確結(jié)果。即 Sound but not fully-precise static analysis 。

Sound 示例

??????對于下面的代碼：其中類 B 和 C 是 A 的子類，代碼中有兩條路徑可以到達(dá) B b’ = (B) a.fld;
??????對于 UnSound 的情況下，只會判斷某一條路徑（取決具體實(shí)現(xiàn)）比如僅僅判斷藍(lán)色路徑，認(rèn)為這段代碼是正確的。而在 Sound 的情況下，是要對兩條路徑都要進(jìn)行判斷的，因?yàn)椴淮_定程序執(zhí)行流具體會走哪條路徑，對藍(lán)色路徑判斷的結(jié)果為正確，對綠色路徑判斷的結(jié)果為錯誤，對于語句 B b’ = (B) a.fld; 是否能夠執(zhí)行成功并不能得到一個確切的結(jié)論。我們認(rèn)為前者得到的結(jié)論是不安全的，而后者得到的結(jié)論是安全的。

??????在靜態(tài)分析中，下面的代碼執(zhí)行完畢之后 a 的值為多少？

if(input)a=1;elsea=0;

??????答案是 a=1 or a=0，也可以精確的描述為：當(dāng) input 為真時，a=1；input 為假時，a=0。

小結(jié)

??????Static Analysis: ensure (or get close to) soundness, while making good trade-offs between analysis precision and analysis speed.

抽象和過近似（Abstraction + Over-approximate）

靜態(tài)分析示例

??????問題：判斷對于某個給定的程序中所有變量的符號。（+、- 或者 0）

??????下面分兩步來描述靜態(tài)分析處理該問題的步驟：

抽象

??????即對程序中出現(xiàn)的具體的值進(jìn)行抽象。如下所示：左側(cè)為具體的語句，右側(cè)為抽象的結(jié)果

??????v=10； ??????那么 v 對應(yīng)的符號為正(+)。
??????v=-9；??????? 那么 v 對應(yīng)的符號為負(fù)(-)。
??????v=0； ????????那么 v 對應(yīng)的符號為0(O)。
??????v=e?1:-1； 那么 v 對應(yīng)的符號為不知道(T)。（不清楚 e 的值為真或假）
??????v=e/0； ?????那么 v 對應(yīng)的符號為未定義(⊥)。（除0是一個未定義的運(yùn)算）

過近似

??????在將程序中的語句抽象完之后，然后在抽象后的結(jié)果上進(jìn)行過近似操作

轉(zhuǎn)換函數(shù)（Transfer Functions）

??????轉(zhuǎn)換函數(shù)是定義如何在抽象值上對不同的程序語句進(jìn)行評估，至于評估什么要根據(jù)程序中語句的語義和我們要分析的問題來決定。接下來以下面這個圖片進(jìn)行說明：

??????左側(cè)是轉(zhuǎn)換函數(shù)，或者說是轉(zhuǎn)換公式會更加確切點(diǎn)。包括有正數(shù)+負(fù)數(shù)=不知道；任何數(shù)/0=未定義 等等。轉(zhuǎn)換函數(shù)所表示的意義并不難理解。

??????右側(cè)是一個程序中存在的具體語句，注意：對變量符號的判斷是在已經(jīng)抽象的基礎(chǔ)上進(jìn)行的。最后得到了三處未定義的地方，第一處為除0，第二處的數(shù)組下標(biāo)為負(fù)值，第三處的數(shù)組下標(biāo)可能為負(fù)值。其中第三處的未定義是誤報，因?yàn)樵诔绦虻木唧w執(zhí)行中，我們可以輕易的計算出 a 的值為9，在實(shí)際執(zhí)行中并不是負(fù)值，即語句是正確的。

控制流處理（Control Flow handling）

??????控制流處理通常處理：在程序存在分支的情況下，匯合點(diǎn)處變量的符號如何來判斷。
??????如上圖所示：左邊是具體的語句，從語句 x = 1 ; 開始程序進(jìn)入到兩個不同的路徑里面，分支的匯合點(diǎn)為語句 z = x + y ; 。可以看到左邊路徑得到的y為正，而右邊路徑得到的y為負(fù)，那么得到匯合點(diǎn)處變量y的值為不確定(T)。

總結(jié)

??????這一部分簡單介紹了靜態(tài)分析的特點(diǎn)比如：不需要執(zhí)行程序，總是需要保持 Sound 及其原因，保持 Sound 的結(jié)果導(dǎo)致容易產(chǎn)生誤報。以及靜態(tài)分析處理程序的兩個重要步驟：抽象和過近似。后面會介紹靜態(tài)分析中 IR 的生成和 CFG 的建建立。未完待續(xù)~

總結(jié)

以上是生活随笔為你收集整理的静态程序分析chapter1 - 概述和两个重要步骤的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。