KLEE到底是靜態分析工具還是動態分析工具？

01-28

KLEE以及S2E是目前比較成熟的符號執行工具，KLEE採用是動態符號執行進行分析，S2E採用選擇符號執行，哪款工具採用的是混合符號執行呢S2E么

符號執行(Symbolic Execution) 屬於靜態分析的一種，舉個例子，對於函數a = malloc(), 符號執行會賦值一個符號$a 來代表 a的值，說白了，就是符號執行不知道a具體是啥值，他也沒有真正去執行malloc()這個函數調用。所以不能算作動態分析，當然得算靜態分析了。

回樓上的，他說的混合執行，應該是concolic(concrete symbolic) execution 吧。

符號執行(symbolic execution)本身是靜態的，因為它只是把具體的輸入值(input value)用符號值(symbolic value)替換，然後根據符號值的的約束條件在約束求解器(constraint solver)允許的條件下求解出滿足條件的輸入值。約束條件傳播過程是靜態的，這個過程沒有辦法執行真正任何程序。通常的做法是分析到有定義的函數調用層次(需要考慮函數參數映射)。遇到標準庫函數或系統調用大部分情況下還是沒有辦法，例如KLEE要在把ulibc編譯成LLVM IR的時候才能解決部分C的標準庫函數。

得到(根據約束求解器生成的可能)滿足約束條件的輸入值(即測試用例)，符號執行引擎會按照正常的方式(具體值)去執行程序，這是動態的——但是這不屬於"自動生成測試用例"的過程，儘管現實的符號執行工具通常會包含這一步。

concolic testing通常是取一個具體的輸入值，先進行一次具體執行同時記錄對應的分支狀態，然後採用一定的啟發式手段來反轉分支條件，得到的約束條件交給約束求解器求解算出新的滿足條件的輸入值並執行；後續的分支條件即測試用例可能依賴於已有的分支條件以及具體的輸入值用例生成。

KLEE更接近於傳統的符號執行，即它開始的值是符號值(通過make symbolic)，給符號值分配了一段指定大小的內存空間，然後根據後續的條件(不一定限於分支條件)算出該內存空間的值所需要滿足的條件。如果約束求解器算不出(如浮點數條件)，或者由於遇到沒有事先處理的函數調用(如遇到printf而沒有告訴KLEE如何處理)，那麼KLEE的解釋器無法得到新的約束條件，從而停止繼續生成約束條件、而轉而根據當前的路徑條件求解出一個具體值帶入執行，同時這條路徑條件(path condition)上的分析到此結束。

S2E的"selective"好像體現在選擇在將二進位代碼"在qemu模擬器上(具體)解釋執行"還是"動態轉化成LLVM的IR並用符號執行器(KLEE)求解約束條件(並具體執行)"上。

另外有一篇survey性質的論文https://people.eecs.berkeley.edu/~ksen/papers/cacm13.pdf 可供參考(有點老，但是符號執行最近三年可能沒有實質性的突破)。

Cristian Cadar在符號執行30年論文中提到現代符號執行技術主要是將具體執行和符號執行結合起來，分為兩種：concolic testing和Execution-Generated Testing（EGT），KLEE屬於第二種。第一種是同時維護具體state和符號化state，在具體輸入引導下收集符號化約束，反轉後產生新輸入，下一次走其他路徑。KLEE所用的EGT將具體執行和符號執行是通過在每個操作前檢查操作涉及到的值是不是都是具體的，如果是則像在原始程序中一樣執行，否則符號化執行。

2017年10月10日更新

KLEE是動態符號執行工具，工具目前主要維護負責人Cadar在11年的文章中明確的把KLEE劃分為動態符號執行工具。論文標題為：Symbolic execution for software testing in practice - preliminary assessment。

以下是修改後的原答案：

KLEE是用LLVM解釋器在執行代碼的，然後在解釋器執行的過程中，如果遇到分支，就生成新的路徑，用解釋器執行這本身就是一個動態的探索過程過程，程序是真的通過解釋器在執行的。但是這和動態符號執行的想法又略微有些不一樣，動態符號執行是給定一個輸入跑到程序結束，跑出一條程序路徑，在分支節點取反，求出新的輸入再繼續跑。

所以，我認為KLEE是和靜態符號執行策略相似的，動態符號執行工具。

符號執行分為靜態符號執行，動態符號執行，選擇符號執行,微符號執行四種。1.靜態符號執行變數為純符號，搜索過程會有路徑爆炸問題。2.動態符號執行也稱為conclic符號執行，是具體值和符號值相結合，例如，具體值執行，跟蹤符號化的約束，在分支取反可以探索新的路徑，可以一部分避免路徑爆炸問題,如klee。3.選擇符號執行，在程序分析過程中部分具體執行，部分符號化執行，可以進行一定選擇切換，如s2e。4.微符號執行，是指對程序的代碼片段做符號執行，可以是一個函數或任意一段代碼，如uc-klee。

s2e是在klee的基礎上加上了qemu，s2e現在主要的優勢是選擇性符號執行，混合符號執行是啥？