文章目錄

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

---

前言

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

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 屬性，并不能準確判斷程序是否滿足這些屬性。所以為了得到一些東西，就應該舍棄一些別的東西。

Sound & Complete

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

Sound 示例

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

??????在靜態分析中，下面的代碼執行完畢之后 a 的值為多少？

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

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

小結

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

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

靜態分析示例

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

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

抽象

??????即對程序中出現的具體的值進行抽象。如下所示：左側為具體的語句，右側為抽象的結果

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

過近似

??????在將程序中的語句抽象完之后，然后在抽象后的結果上進行過近似操作

轉換函數（Transfer Functions）

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

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

??????右側是一個程序中存在的具體語句，注意：對變量符號的判斷是在已經抽象的基礎上進行的。最后得到了三處未定義的地方，第一處為除0，第二處的數組下標為負值，第三處的數組下標可能為負值。其中第三處的未定義是誤報，因為在程序的具體執行中，我們可以輕易的計算出 a 的值為9，在實際執行中并不是負值，即語句是正確的。

控制流處理（Control Flow handling）

??????控制流處理通常處理：在程序存在分支的情況下，匯合點處變量的符號如何來判斷。
??????如上圖所示：左邊是具體的語句，從語句 x = 1 ; 開始程序進入到兩個不同的路徑里面，分支的匯合點為語句 z = x + y ; ?？梢钥吹阶筮吢窂降玫降膟為正，而右邊路徑得到的y為負，那么得到匯合點處變量y的值為不確定(T)。

總結

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

總結

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

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。