如何學習符號執行(Symbolic Execution)?

01-06

竊以為符號執行更像是一種方法一種idea而非一項技術，概念出現很早(76年)很容易理解，而在實現它的過程中則需要解決許多現實中的問題，例如約束求解，路徑爆炸等問題，並且需要優化其性能，隨之發展出了concrete execution。現在的主要問題是在如何高效準確地去實現它，同時可以結合多種技術例如靜態分析，甚至機器學習等，去提高效率和準確性。對於入門，最好的方法無過於學習現有的系統源碼，可以先看klee，對於進一步了解conclic，可以看s2e。進入研究階段，就需要大開腦洞去想如何設計或改善一些演算法或設計去提高它，使其更具有實用性。個人見解，僅供參考。

ls的答主說得很好，我補充幾個項目DART(PLDI 05), EXE(CCS 06), Sketch(ASPLOS 06), SAGE(NDSS 08)。另外有個「微型」項目 GitHub - xiw/mini-mc（作者是誰就不用介紹了..）

兩點建議：

從特定應用需求（如果有的話）出發：testing, verification(比如invariant generation), synthesis, repair等等，symbolic execution的設計各有不同。.

從通用的技術問題出發，除了symbolic execution,其他技術也有這些問題。學習某項目時可以重點看它們是如何處理的：

Loops and recursion：是unroll/inline還是藉助invariant inference
Path explosion：各種path selection策略（加入啟發式方法？)..
Heap modeling: 藉助shape analysis/pointer analysis? lazy concretization? 用solver的array theory?
Environment modeling: library, os等環境。
Solver limitation：從生成到求解的各種優化策略..

https://github.com/saswatanand/symexbib 這裡有一個關於符號執行的文獻列表，此外CACM 2013-02 有一篇Symbolic Execution for Software Testing: Three Decades Later的文章可以作為入門。入手項目的話，感覺klee的文檔比較全。

符號執行的發展從傳統符號執行到動態符號執行到選擇性符號執行理論上已經很豐富，要學習可以先了解符號執行原理參考相關論文，比如KLEE，S2E，CREST等工具相關論文，如果想深刻理解符號執行的原理和過程最好學習一款符號執行工具的設計源碼，個人覺得CREST的代碼量相對小，如果不想涉足學習基於cil的插樁方法可以只看插樁結果和樁函數，結合小程序符號執行過程可以對動態符號執行有個基本的理解。希望這些對你有所幫助。

首先隨便找個開源Symbolic Execution工具，看自帶的教學，從自帶的例子（如果有）開始試著玩玩各種功能。可選的工具其他人已經說差不多了，再提一個最近才開源的angr:

angr, a binary analysis framework

DARPA CGC勝者組！融合了最近幾年的數種優化技術！有能用的Veritesting真令人羨慕;w;

如果想要深入理解，玩的同時可以看看這方面的論文。雖然市面上有多個開源的Symbolic Execution工具，但是基本原理都差不多，所以看個一兩篇就夠了。嫌整篇論文太長的話也可以找篇最近的Symbolic Execution論文看看Background的部分。

其他一些我所知道的開源Symbolic Execution工具:

KLEE

Overview - S2E: A Platform for In-Vivo Analysis of Software Systems

CREST by jburnim

FuzzBALL: Vine-based Binary Symbolic Execution