[[394624]]

動態符號執行的想法是在任何輸入上執行一個軟件，同時探索所有可能的執行路徑，而無需指定具體值。具體示例如下，其中輸入x未知，即符號：

符號執行在所有三個執行路徑(x < 0, x > 100, 0 < = x < =100)并生成三個具體的測試用例：x=-1, x=101和x=23在擊中斷言之后。

你不再需要手動編寫測試用例，你會沿執行路徑捕獲斷言失敗和內存安全漏洞。以上說的可不是理論層面上的事情，哪這種方法可以在實踐中用于實際程序嗎?

KLEE

KLEE是一個符號執行引擎，可對任何輸入執行未修改的真實程序。你將程序編譯為LLVM位碼，將某些輸入標記為符號，然后啟動KLEE。 KLEE使用約束解決方案探索可能的執行路徑，并為每個路徑生成具體的測試用例。如果發生漏洞，你可以使用觸發它的輸入來重播程序。

2019年11月，關于KLEE的OSDI 2008開創性論文被選入ACM SIGOPS名人堂。在過去的十年里，KLEE的研究和應用產生了超過150篇科學出版物、數十篇博士論文、研究資助、工具和安全初創公司。

使用KLEE測試網絡協議

在2007年，我一直努力尋找自己的研究論文，直到遇到Cristian Cadar的論文“EXE: Automatically Generating Inputs of Death“EXE: Automatically Generating Inputs of Death”。受到符號執行思想的啟發，在將傳入的網絡數據包傳遞到網絡堆棧之前，可以標記它的協議報頭嗎?如果是這樣，我可以用這種技術找到協議規范和實現漏洞嗎?

于是研究人員寫了一封電子郵件給Cristian Cadar，并迅速收到了答復。而且，Cristian和Daniel Dunbar慷慨地向它發送了KLEE的源代碼，這是他們正在使用的新工具，目前還尚未對外公布。

接下來我擴展了KLEE以執行相互通信的多個協議棧。我將此技術用于測試傳感器網絡，并在我的IPSN 2010論文中描述的Contiki OS中發現了兩個有趣的漏洞。其中一個導致了TCP/IP堆棧內的傳感器節點的死鎖，需要重新設置硬件，這是在傳感器網絡部署中觀察到的真正漏洞。死鎖是指兩個或兩個以上的進程在執行過程中，由于競爭資源或者由于彼此通信而造成的一種阻塞的現象，若無外力作用，它們都將無法推進下去。此時稱系統處于死鎖狀態或系統產生了死鎖，這些永遠在互相等待的進程稱為死鎖進程。

自2015年以來，我一直沒有過多使用過KLEE，并且想再次嘗試一下。同時，Contiki OS已拷貝到Contiki-NG。我復制了存儲庫，并將稱為20-packet-parsing的測試用例編譯為LLVM位碼。在測試用例中，我使用KLEE的klee_make_symbolic函數標記了測試數據包緩沖區(〜1KB)的符號。Contiki-NG是一套用于下一代IoT(物聯網)設備的開源跨平臺操作系統，可適用于獨立高防服務器。

在我的舊Mac上運行了幾分鐘后，KLEE在解析某些協議的標頭時發現了兩個內存漏洞(指針超出范圍)。我將這些發現與具體的測試案例一起報告給Contiki-NG的安全團隊，以進行進一步的分析。對我來說，這個小測試是KLEE仍然是有用的研究和測試案例生成工具的又一個證據。

開放的挑戰和機遇

將符號執行應用于任意真實程序很難，你通常必須對執行環境建模，并找到有效的方法來應對不確定性和路徑爆炸。 而且，許多路徑約束很難解決，但是對于當今的求解器而言難以及時解決。

盡管如此，研究和應用符號執行(使用KLEE)仍會帶來許多機會。你將了解程序結構，編譯器，SAT / SMT求解器，以及如何編寫其他類型的測試工具。基于這些知識，我編寫了模糊Android應用程序的工具，超級優化LLVM IR，以及最近在工作中使用拼寫編寫的模糊衛星控制程序的工具。

本文翻譯自：https://sasnauskas.eu/finding-software-bugs-using-symbolic-execution/