[[394624]]

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

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

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

KLEE

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

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

使用KLEE測試網(wǎng)絡(luò)協(xié)議

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

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

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

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

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

開放的挑戰(zhàn)和機遇

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

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

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