一、Programming Languages體系

靜態程式分析是程式語言中應用層面下的一個細分領域，它是一個非常重要的核心內容。

• 在理論部分，考慮的是如何設計一個語言的語法和語意，如何設計語言的型別系統等等問題。在過去十年中，語言核心幾乎沒有變化
• 有了語言的語法、語意和型別系統之後，我們需要支撐語言的執行。因此，在環境部分，需要考慮如何為執行中的程式提供執行時環境——如何設計編譯器，在執行時需要怎樣的支援（如記憶體的分配管理）等等。語言承載環境處於一個緩慢提升的階段，主要集中在硬體裝置以及高效能程式設計優化方面
• 變化最大的是程式分析，因為隨著IT、雲端計算、軟體SaaS的快速發展，軟體的規模變得更大、結構更復雜、數量更多。如何確保系統的可靠性、安全性和其他承諾，如何自動合成一個程度，成為了一個日趨熱門的研究和工程化領域

二、Static Analysis定義

Static analysis analyzes a program P to reason about its behaviors and determines whether it satisfies some properties before running P. 

• Does P contain any private information leaks?
• Does P dereference any null pointers?
• Are all the cast operations in P safe?
• Can v1 and v2 in P point to the same memory location?
• Will certain assert statements in P fail?
• Is this piece of code in P dead (so that it could be eliminated)?
• …

上圖中的兩種答案在靜態分析語意中都是對的，他們分別代表了兩種求解方式：

• 分支窮舉：耗時，但是精確
• 符號執行：快速，但是不那麼精確

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

Two Words to Conclude Static Analysis：

Static Analysis = Abstraction + Over-approximation

舉一個具體的例子：通過靜態分析，判斷一段PHP程式碼是否能存在外部任意引數執行風險，即是否是Webshell。要完成這個靜態分析過程，需要進行如下處理：

• Abstraction
• Over-approximation
  • Transfer functions
  • Control flows

原始程式碼如下：

<?php
    v1 = 1;
    v2 = 2;
    v3 = $_POST[1];
    v4 = $_POST[2];
    v5 = v3 == 1 ? v3 : 5;
    $$_POST[3] = $_POST[4];  // $_POST[4] = v6

    if(v3 == 1){
        eval(v5);
    }
    echo "hello world";
?>

我們先來看Abstraction抽象，

按照萊斯定律，「完美靜態分析」有兩個核心特徵：

• Sound（完全覆蓋）
• Complete（精確推斷）

如果一段程式是「non-trivial」的，則不存在一個完美的靜態分析程式，可以同時滿足Sound和Complete特徵。換到工業界的術語就是，誤報和漏報無法同時達到100%。

在實際使用中，我們並不是追求「完美靜態分析」，而是追求「有用的靜態分析」，即滿足如下兩個核心特徵：

• Compromise soundness (false negatives，折中地漏報控制)
• Compromise completeness (false positives，折中地誤報控制)

在實際工業場景中，Soundness往往是優先追求的目標，我們以Webshell靜態程式碼分析為例說明。

如果追求Sound的目標，在進行靜態程式碼分析的時候，完整性/覆蓋度/高檢出往往是優先追求的目標。在另一方面，相對的誤報就不可避免了。

五、靜態程式分析與類似技術的對比

靜態程式分析

• 優點：
  • 在選定的精度下能夠保證沒有bug
• 缺點：
  • 學術門檻相對高。目前已知國內高校公開的課程資料只有北京大學，南京大學，國防科大，吉林大學的，且通俗易懂的教材稀少。作為一門計算機專業的高年級選修課，入門和提高都較困難。

動態軟體測試

• 優點：
  • 在工程中被廣泛應用，並且有效。實現簡單，便於自動化。
• 缺點：
  • 無法保證沒有bug。 這是無法遍歷所有可能的程式輸入的必然結果。
  • 在當今的由多核與網路應用帶來的並行環境下作用有限。 某個bug可能只在特定情況下發生，因而難以穩定地復現。

形式化語意驗證

• 優點：
  • 由於用數學的方法對程式做了抽象，能夠保證沒有bug。
• 缺點：
  • 學術門檻較高，學習者必須有良好的數學基礎才能入門。
  • 驗證代價較高，一般來說非常重要的專案會使用這一方式保證程式質量。甚至在作業系統這樣重要的軟體中，也並不一定會使用。