1. 引言

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3. 經(jīng)典的符號執(zhí)行技術(shù)

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

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

這里舉一個經(jīng)典的例子[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í)行的目的，就是在給定的時間預(yù)算內(nèi)，生成一組輸入，并通過這些輸入盡可能多的探索執(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í)行結(jié)束時，使用約束求解器對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）。“then”分支： 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)或遞歸結(jié)構(gòu)，且它們的終止條件是符號化的，則可能導致有無窮多條路徑。在實踐過程中，需要對路徑搜索設(shè)置一個限制，例如timeout，限制路徑數(shù)量，循環(huán)迭代次數(shù)或探測深度。

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

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

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

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

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

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

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

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

• 混合執(zhí)行會生成一些隨機的輸入值，比如{x=22, y=7}，然后符號化和具體化地一起來執(zhí)行程序。
• 依據(jù){x=22, y=7}，程序在第7行，這個具體的執(zhí)行會走向else分支；符號執(zhí)行沿著執(zhí)行路徑會生成x ≠ 2y0的路徑約束；
• 混合測試將路徑約束中的連接（x ≠ 2y0）取反，生成一個新的約束x0=2y0，并求解得到測試輸入{x=2, y=1}。這個新的輸入會強制讓程序執(zhí)行then路徑。
• 依據(jù){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í)行技術(shù)已經(jīng)有了40多年的發(fā)展，在2017年8月Google學術(shù)中，標題中帶有“符號執(zhí)行”的文章有742篇[3]，到2020.11月，文章數(shù)上升到1490, 可見符號執(zhí)行有了飛速的發(fā)展。但程序的復(fù)雜性和規(guī)模也在飛速的發(fā)展，符號執(zhí)行仍然存在路徑爆炸（代碼規(guī)模、復(fù)雜度）、約束求解（計算算法）、內(nèi)存模型（工具設(shè)計）等挑戰(zhàn)。

5.1. 路徑爆炸(Path Explosion)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

5.2. 約束求解(Constraint Solving)

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

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

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

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

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

5.3. 內(nèi)存建模(Memory Modeling)

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

目前這個權(quán)衡的主要參考依據(jù)是：

1. 具體分析問題的性質(zhì)；

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

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

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

7. 結(jié)束語

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

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

最新評論