1. 引言

程序靜態(tài)分析（Program Static Analysis）是指在不運行代碼的方式下，通過詞法分析、語法分析、控制流、數(shù)據流分析等技術對程序代碼進行掃描，驗證代碼是否滿足規(guī)范性、安全性、可靠性、可維護性等指標的一種代碼分析技術[8]。 程序靜態(tài)分析的歷史幾乎與程序的歷史一樣長, 自從有了程序就有了程序分析。特別是隨著編譯技術的發(fā)展，大大帶動了程序的自動分析技術。目前靜態(tài)分析技術向模擬執(zhí)行的技術發(fā)展以能夠發(fā)現(xiàn)更多傳統(tǒng)意義上動態(tài)測試才能發(fā)現(xiàn)的缺陷，例如符號執(zhí)行、抽象解釋、值依賴分析等等并采用數(shù)學約束求解工具進行路徑約減或者可達性分析以發(fā)現(xiàn)更多的問題、減少誤報、提高效率。

隨著程序的規(guī)模和復雜度越來越高，現(xiàn)代的程序分析的具體應用中，對一個問題的檢查往往不是單一個使用一種技術，而是會同時使用多種分析技術，采用多次迭代，反復求精的過程。 這就要求我們在設計的時候能統(tǒng)一規(guī)劃，策略對待不同的問題。就好比一個大廚，做每道菜，用什么材料，先放什么，后放什么，用什么火候，放多少都要把控的恰到好處。

這里我打算把這個技術介紹做成一個系列，探討靜態(tài)分析中的各種技術，希望通過這些介紹，能夠讓更多的程序員能夠投入到程序分析的行列來，一起進行更深層次的軟件自動化方面的探討和研究。

2. 關于符號執(zhí)行的一個故事

大家都喜歡聽故事，這里先講一個和符號執(zhí)行相關的故事作為一個引子。

話說一年一度的網絡安全行業(yè)盛會RSA大會，每年入選的創(chuàng)新沙盒十強，都會成為業(yè)界投資者的追捧，同時從這些項目中，我們也可以推斷出網絡安全技術創(chuàng)新的熱點方向。

今年的十強中有一個叫做Mayhem的產品，對于Mayhem這個名字，搞符號執(zhí)行的人恐怕并不陌生。

首先這個名字Mayhem讓人影響深刻，中文翻譯過來就是“混亂”，本來世界就夠亂的了，還把工具叫成“混亂”，真是"Complete mayhem"（全亂了）。

把和Mayhem有關的信息，按時間順序編排一下，就可以看到故事的主線：

• ForAllSecure成立于2012年，其技術源于卡耐基梅隆大學（CMU）研究獲得的專利技術；
•  從2012年到2017年，美國國防部(DoD)在幾乎所有正在開發(fā)的關鍵武器系統(tǒng)中發(fā)現(xiàn)了漏洞。
• 《M國國防法》要求就加強關鍵系統(tǒng)的軟件安全性提出報告，建議在國防高級研究計劃局的“網絡大挑戰(zhàn)”下開發(fā)二進制分析和符號執(zhí)行工具;
• 2016年美國高等研究計劃署(DAPRA)主辦了自動網絡攻防賽(CyberGrandChallenge)，旨在建立實時自動化的網絡防御系統(tǒng)，并且能夠快速地應對大量新的攻擊手法，以應對頻發(fā)的網絡攻擊。符號執(zhí)行在參賽隊的自動攻防系統(tǒng)中起到了舉足輕重的作用，被廣泛應用在程序脆弱性的分析上。卡內基梅隆大學ForAllSecure團隊的Mayhem獲得了CGC的冠軍；
• 2018年，GAO-19-128號報告稱，由于武器系統(tǒng)的計算機化，武器系統(tǒng)比以往任何時候都更依賴軟件，也更加網絡化，為了使武器系統(tǒng)防范日益復雜的網絡安全攻擊，美國國防部(DoD)正在開發(fā)更安全的武器系統(tǒng);

Mayhem是聯(lián)邦政府推薦的安全解決方案，用于連續(xù)，自動化，準確的測試;

美國國防部的多個實體都使用Mayhem，包括但不限于：空軍第96網絡空間測試小組，空軍第90網絡空間操作中隊，海軍海系統(tǒng)司令部（NAVSEA）和美國陸軍司令部，控制，通信，計算機，網絡，情報，監(jiān)視和偵察中心（C5ISR）。

Mayhem是ForAllSecure推出的輔助智能行為測試解決方案。它采用符號執(zhí)行自動生成測試用例，然后通過模糊測試（fuzz）發(fā)現(xiàn)軟件缺陷。Mayhem將這兩種測試技術融合，集成在了DevOps中，持續(xù)的發(fā)現(xiàn)安全漏洞。

注: 從ForAllSecure的網站(https://forallsecure.com/government-and-defense)，可以得到上面的信息。

另：Mayhem[4]使用的是二進制的符號執(zhí)行框架，屬于動態(tài)分析的范疇，這里只是作為我們的一個引子，不必要糾結。

接下來，我們提綱絜領的介紹下符號執(zhí)行，讓大家明白這個技術的主要作用和面臨的挑戰(zhàn)，領大家入坑，更多的細節(jié)可以從后面的參考文獻中獲得。

3. 經典的符號執(zhí)行技術

符號執(zhí)行[1]是一種靜態(tài)分析技術，它可以通過分析技術得到讓特定區(qū)域執(zhí)行的輸入。最初在1976年由King JC在ACM上提出。即通過使用抽象的符號代替具體值來模擬程序的執(zhí)行，當遇到分支語句時，它會探索每一個分支, 將分支條件加入到相應的路徑約束中，若約束可解，則說明該路徑是可達的。符號執(zhí)行的目的是在給定的時間內，盡可能的探索更多的路徑。根據運行的目的來分，主要有兩個：

• 從測試的角度來看，它可以模擬出各個路徑的輸入值，從而創(chuàng)建高覆蓋率的測試套件。這里是靜態(tài)的分析程序得到測試需要的輸入，與動態(tài)執(zhí)行程序的測試不同，動態(tài)執(zhí)行程序的測試更多的是依賴完備的測試用例來提升測試的覆蓋率，達到發(fā)現(xiàn)問題的目的。比如曾經使用過的IBM的Purify 來檢測代碼的內存泄露問題。就需要人工的看代碼，編制大量的測試用例，然后通過讓程序執(zhí)行分別執(zhí)行這些輸入，來提高代碼的覆蓋率，從而盡可能的發(fā)現(xiàn)內存泄漏的問題。
• 從缺陷查找的角度來看，它為開發(fā)人員提供了觸發(fā)的缺陷的具體輸入，利用該輸入，程序可用于缺陷的確認或調試。符號執(zhí)行不僅限于查找諸如緩沖區(qū)溢出之類的問題，而且可以通過根據缺陷發(fā)現(xiàn)的條件，生成復雜的斷言，來判斷缺陷發(fā)生的可能性。

這里舉一個經典的例子[2]，來說明符號執(zhí)行的具體過程。

int twice(int v){
       return 2*v;
   }

   void testme(int x, int y){
       z = twice(y);
       if (z == x){
           if (x > y+10)
               ERROR;
       }
   }

   int main(){
      x = sym_input();
      y = sym_input();
      testme(x, y);
      return 0;
   }

這段代碼中的函數(shù)testme()有三條執(zhí)行路徑。符號執(zhí)行的目的，就是在給定的時間預算內，生成一組輸入，并通過這些輸入盡可能多的探索執(zhí)行路徑。

執(zhí)行路徑(execution path)：一個true和false的序列seq ={p0, p1, …, pn}。其中，如果是一個條件語句，那么pi=ture則表示條件語句的取值為：true，否則取false；

執(zhí)行樹(execution tree)：一個程序的所有執(zhí)行路徑則可表征成一棵執(zhí)行樹。

下圖是樣例代碼的執(zhí)行樹：

符號執(zhí)行通過維護符號狀態(tài)和路徑約束，以便在運行過程中傳遞信息。

符號狀態(tài)(symbolic state)：符號執(zhí)行維護一個符號狀態(tài)σ，將變量映射到符號表達式。

符號路徑約束(symbolic path constraint)：符號路徑約束PC，它是符號表達式上無量詞的一階公式。

在執(zhí)行開始時，將σ初始化為一個空映射，將PC初始化為true；

在符號執(zhí)行過程中，σ和PC都會更新。

在沿著程序執(zhí)行路徑的符號執(zhí)行結束時，使用約束求解器對PC進行求解，以生成具體的輸入值。 如果程序在這些具體的輸入值上執(zhí)行，它將采用與符號執(zhí)行完全相同的路徑，并以相同的方式終止。

對于樣例代碼，具體的過程如下

初始化：初始化符號狀態(tài)σ為空，符號路徑約束PC為true；

在每個賦值v = e處，符號執(zhí)行都通過將 v 映射到σ(e)來更新σ，該映射是通過對當前符號狀態(tài)求值, 而獲得的符號表達式。

例如：main（）函數(shù)的前兩行（第16-17行）的符號執(zhí)行導致σ= {x ->x0，y -> y0}，其中x0，y0是兩個初始不受約束的符號值；在執(zhí)行第6行之后，σ = {x ->x0，y ->y0，z -> 2y0}。對于每個條件語句：if（e） then S1 else S2。在第7行之后，分別創(chuàng)建了兩個符號執(zhí)行實例，分別具有路徑約束x0 = 2y0和x ≠ 2y0;在第8行之后，分別創(chuàng)建兩個具有路徑約束的符號執(zhí)行實例（x0 = 2y0）∧（x0 > y0 + 10）和（x0 = 2y0）∧（x0 ≤ y0 + 10）?！皌hen”分支： PC被更新為PC ∧ σ(e)；“else”分支：生成一個新的PC', PC'被初始化為：PC∧¬ σ(e)；如果分支的狀態(tài)σ的PC可滿足，則符號執(zhí)行沿著分支繼續(xù)，否則路徑終止。
例如:如果一個符號執(zhí)行實例碰到了exit或error時，當前符號執(zhí)行實例就會被終止，并利用一個現(xiàn)成的約束求解器來生成一個可滿足當前路徑約束的賦值。三條路徑按照約束求解后，分別得到我們期望的三組輸入：{x=0, y=1}，{x=2, y=1}和{x=30,y=15}。若代碼中包含循環(huán)或遞歸結構，且它們的終止條件是符號化的，則可能導致有無窮多條路徑。在實踐過程中，需要對路徑搜索設置一個限制，例如timeout，限制路徑數(shù)量，循環(huán)迭代次數(shù)或探測深度。

經典的符號執(zhí)行有一個關鍵的缺點，若符合執(zhí)行路徑的符號路徑約束無法使用約束求解器進行有效的求解，則無法生成輸入。

4. 現(xiàn)代符號執(zhí)行技術

經典的符號執(zhí)行，過度的依賴了符號執(zhí)行的約束求解能力，這就限制了傳統(tǒng)符號執(zhí)行的能力發(fā)揮。很快大家發(fā)現(xiàn)在分析過程中，如果能加入具體值進行分析，將大大簡化分析過程，降低分析的難度和提升效率；但分析過程中，仍不可避免的還是需要將各種條件表達式，進行符號化抽象后變成約束條件參與執(zhí)行。將程序語句轉換為符號約束的精度，對符號執(zhí)行所達到的覆蓋率以及約束求解的可伸縮性會產生重大影響。所以如何做好混合具體(Concrete)執(zhí)行和符號(Symbolic)執(zhí)行的能力的平衡，就成為現(xiàn)代符號執(zhí)行的關鍵點。

混合執(zhí)行測試（Concolic testing)[5][6]和執(zhí)行生成測試（Execution-Generated Testing (EGT)）[7]這兩種現(xiàn)代符號執(zhí)行的代表都是基于這個思想發(fā)展而來的。下面以混合執(zhí)行測試（Concolic testing)為例說明下現(xiàn)代符號執(zhí)行的主要過程。

與經典的符號執(zhí)行不同，由于混合執(zhí)行在整個執(zhí)行過程中，需要維護程序的具體狀態(tài)，因此其輸入需要初始具體值。 混合執(zhí)行測試從一個給定的輸入或隨機輸入開始執(zhí)行程序，沿著執(zhí)行的條件語句在輸入上收集符號約束，然后使用約束求解推斷先前輸入的變化，以便引導程序接下來的執(zhí)行該走向哪一個執(zhí)行路徑。重復此過程，直到探索了所有執(zhí)行路徑，或者滿足用戶定義的覆蓋標準、時間設置到期為止。

混合執(zhí)行測試會同時維護兩個狀態(tài)：

• 具體狀態(tài)：映射所有有具體值的變量；
• 符號狀態(tài)：僅映射沒有具體值的變量。

對于樣例代碼，執(zhí)行過程如下：

• 混合執(zhí)行會生成一些隨機的輸入值，比如{x=22, y=7}，然后符號化和具體化地一起來執(zhí)行程序。
• 依據{x=22, y=7}，程序在第7行，這個具體的執(zhí)行會走向else分支；符號執(zhí)行沿著執(zhí)行路徑會生成x ≠ 2y0的路徑約束；
• 混合測試將路徑約束中的連接（x ≠ 2y0）取反，生成一個新的約束x0=2y0，并求解得到測試輸入{x=2, y=1}。這個新的輸入會強制讓程序執(zhí)行then路徑。
• 依據{x=2, y=1}，程序在第8行執(zhí)行else分支?；旌蠝y試會沿著具體執(zhí)行來進行符號執(zhí)行，并生成路徑約束（x0 = 2y0）∧（x0 > y0 + 10）；
• 混合測試將路徑約束中的連接（（x0 > y0 + 10））取反，會生成一個新約束（x0 = 2y0）∧（x0 ≤ y0 + 10）的測試，求解得到測試輸入{x=30, y=15}。在這個輸入下程序走到ERROR語句。
• 混合測試報告所有被探索的執(zhí)行路徑，并終止測試輸入的生成。

比較混合執(zhí)行測試和傳統(tǒng)的符號執(zhí)行，不難發(fā)現(xiàn)由于具體值的引入，簡化了約束求解的難度。

5. 主要挑戰(zhàn)和解決方案

符號執(zhí)行技術已經有了40多年的發(fā)展，在2017年8月Google學術中，標題中帶有“符號執(zhí)行”的文章有742篇[3]，到2020.11月，文章數(shù)上升到1490, 可見符號執(zhí)行有了飛速的發(fā)展。但程序的復雜性和規(guī)模也在飛速的發(fā)展，符號執(zhí)行仍然存在路徑爆炸（代碼規(guī)模、復雜度）、約束求解（計算算法）、內存模型（工具設計）等挑戰(zhàn)。

5.1. 路徑爆炸(Path Explosion)

符號執(zhí)行在過程處理中默認已經過濾了以下兩種路徑：

不依賴于符號輸入的路徑；

對于當前的路徑約束，不可解的路徑。 但是，盡管符號執(zhí)行已經做了這些過濾，路徑爆炸依舊是符號執(zhí)行的最大挑戰(zhàn)。路徑爆炸不是符號執(zhí)行特有的挑戰(zhàn)，是整個程序分析都需要考慮的最大的問題。

解決路徑爆炸的方案，可以從以下兩個角度來考慮：

減少路徑總數(shù)（優(yōu)先的考慮最有希望的路徑， 路徑合并，剪枝）；

相似的路徑不再分析（函數(shù)摘要，緩存）；

依據這個思路業(yè)界提出了兩種解決方案。

啟發(fā)式（Heuristic)： 大多數(shù)啟發(fā)式方法側重于實現(xiàn)較高的語句和分支覆蓋率。

1. 特別有效的方法是使用靜態(tài)控制流圖（CFG）來指導探索，向最接近的路徑或優(yōu)先選擇先前執(zhí)行次數(shù)最少的語句；

2. 在每個可行的符號分支，隨機選擇要探索的一側； 或者將符號檢驗與隨機檢驗進行交錯進行；

3. 采用先驗知識，探索以往容易出錯的函數(shù)；目前也有研究通過AI的方式得到這些推薦的分析路徑；

利用完善的程序分析技術(Sound program analysis techniques): 這種方法主要是使用程序分析和軟件驗證中的各種思想，以合理的方式降低路徑探索的復雜性。

1. 靜態(tài)地合并路徑，然后再求解；

2. 通過函數(shù)摘要，緩存或重用已經計算過的信息用于后續(xù)的計算中；

3. 通過剪枝，去除無關的變量對路徑的求解的影響；

5.2. 約束求解(Constraint Solving)

盡管在過去的幾年中，約束解決方案技術取得了長足的進步，但約束求解是符號執(zhí)行的技術瓶頸。

減少不相關的約束(Irrelevant constraint elimination) 符號執(zhí)行中的絕大多數(shù)查詢是為了確定某個分支的可行性，一種有效的優(yōu)化方法是從路徑條件中刪除與當前分支的結果無關的那些約束。

增量求解(incremental solving) 符號執(zhí)行期間生成的約束集的一個重要特征是，它們根據來自程序源代碼的一組固定的靜態(tài)分支來表示。因此，許多路徑具有相似的約束集，因此可以采用相似的解決方案。

1. 通過重用先前類似查詢的結果，來提高約束求解的速度；

2. 通過約束集的超集，減少無解的情況出現(xiàn)； 我們目前常用的符號執(zhí)行的工具KLEE，在設計中都采用了著兩種方式。

5.3. 內存建模(Memory Modeling)

在符號執(zhí)行中我們將變量映射到了一個內存模型，來表示這個變量的類型、值或者值域。這個對變量的抽象模式對程序語句轉化成符號約束的精度和對符號執(zhí)行的覆蓋率有著很大的影響。太過精確，往往容易陷入復雜的計算，而不能得到具體的解；太過籠統(tǒng)，又會造成漏報。所以精度和可擴展性之間是需要權衡的。

目前這個權衡的主要參考依據是：

1. 具體分析問題的性質；

2. 采用的約束求解器的限制；

6. 符號執(zhí)行工具

下面列舉了我們常用的符號執(zhí)行工具作為大家的參考。

7. 結束語

目前符號執(zhí)行，在實際的應用中還主要用于與fuzz結合使用，用于縮小fuzz的取值范圍。由于符號執(zhí)行的主要瓶頸--約束求解的性能和局限性，并未在靜態(tài)分析的商業(yè)工具中，大規(guī)模的使用。但我們有理由相信，在不久的將來隨著并行技術、計算性能的提升、以及求解器的優(yōu)化，符號執(zhí)行能夠在靜態(tài)分析中發(fā)揮越來越大的作用。

以上就是詳解靜態(tài)分析技術符號執(zhí)行的詳細內容，更多關于靜態(tài)分析技術符號執(zhí)行的資料請關注腳本之家其它相關文章！

最新評論