前言

符號執(zhí)行 (Symbolic Execution)是一種程序分析技術(shù)，它可以通過分析程序來得到讓特定代碼區(qū)域執(zhí)行的輸入。顧名思義，使用符號執(zhí)行分析一個程序時，該程序會使用符號值作為輸入，而非一般執(zhí)行程序時使用的具體值。在達到目標(biāo)代碼時，分析器可以得到相應(yīng)的路徑約束，然后通過約束求解器來得到可以觸發(fā)目標(biāo)代碼的具體值。

符號執(zhí)行理解

以下面的源代碼為例子：

int m=M, n=N, q=Q;

int x1=0,x2=0,x3=0;

if(m!=0)

{

x1=-2;

}

if(n<12)

{

if(!m && q)

{

x2=1;

}

x3=2;

}

assert(x1+x2+x3!=3)

上述代碼是一個簡單的c語言分支結(jié)構(gòu)代碼，它的輸入是M,N,Q三個變量；輸出是x1,x2,x3的三個變量的和。我們這里設(shè)置的條件是想看看什么樣的輸入向量的情況下，得到的三個輸出變量的和等于3.

符號執(zhí)行

如果把結(jié)果條件更改為漏洞條件，理論上也是能夠進行漏洞挖掘了。對于如何根據(jù)最終得到的結(jié)果求解輸入向量，已經(jīng)有很多現(xiàn)成的數(shù)學(xué)工具可以使用。上述問題其實可以規(guī)約成約束規(guī)劃的求解問題(更詳細(xì)的介紹看這里：Constraint_programming )。比較著名的工具比如SMT(Satisfiability Modulo Theory，可滿足性模理論)和SAT。

靜態(tài)符號執(zhí)行具體流程

符號執(zhí)行分為過程內(nèi)分析和過程間分析(又稱全局分析)。過程內(nèi)分析是指只對單個過程的代碼進行分析，全局分析指對整個軟件代碼進行上下文敏感的分析。所謂上下文敏感分析是指在當(dāng)前函數(shù)入口點要考慮當(dāng)前的函數(shù)間調(diào)用信息和環(huán)境信息等。程序的全局分析是在過程內(nèi)分析的基礎(chǔ)上進行的，如果過程內(nèi)分析中包含了函數(shù)調(diào)用，就引入了過程間分析，因此兩者之間是相對獨立又相互依賴的關(guān)系

過程內(nèi)分析流程

程序全局分析流程

動態(tài)符號執(zhí)行(concolic)(混合符號執(zhí)行)

符號執(zhí)行在發(fā)展過程中出現(xiàn)了一種叫做動態(tài)符號執(zhí)行的方法(concrete and symbolic， concolic)。動態(tài)符號執(zhí)行是以具體數(shù)值作為輸入來模擬執(zhí)行程序代碼，與傳統(tǒng)靜態(tài)符號執(zhí)行相比，其輸入值的表示形式不同。動態(tài)符號執(zhí)行使用具體值作為輸入，同時啟動代碼模擬執(zhí)行器，并從當(dāng)前路徑的分支語句的謂詞中搜集所有符號約束。然后修改該符號約束內(nèi)容構(gòu)造出一條新的可行的路徑約束，并用約束求解器求解出一個可行的新的具體輸入，接著符號執(zhí)行引擎對新輸入值進行一輪新的分析。通過使用這種輸入迭代產(chǎn)生變種輸入的方法，理論上所有可行的路徑都可以被計算并分析一遍。

動態(tài)符號執(zhí)行相對于靜態(tài)符號執(zhí)行的優(yōu)點是每次都是具體輸入的執(zhí)行，在模擬執(zhí)行這個過程中，符號化的模擬執(zhí)行比具體化的模擬執(zhí)行的開銷大很多；并且模擬執(zhí)行過程中所有的變量都為具體值，而不必使用復(fù)雜的數(shù)據(jù)結(jié)構(gòu)來表達符號值，使得模擬執(zhí)行的花銷進一步減少。但是動態(tài)符號執(zhí)行的結(jié)果是對程序的所有路徑的一個下逼近，即其最后產(chǎn)生路徑的集合應(yīng)該比所有路徑集合小，其實concolic執(zhí)行使用了深度優(yōu)先的搜索策略。

參考：

https://www.k0rz3n.com/2019/02/28/%E7%AE%80%E5%8D%95%E7%90%86%E8%A7%A3%E7%AC%A6%E5%8F%B7%E6%89%A7%E8%A1%8C%E6%8A%80%E6%9C%AF/

https://zhuanlan.zhihu.com/p/26927127

總結(jié)

以上是生活随笔為你收集整理的漏洞挖掘 符号执行_简述符号执行的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

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