建站
咨詢
售后
建站咨詢
新聞中心
動(dòng)態(tài)符號(hào)執(zhí)行的想法是在任何輸入上執(zhí)行一個(gè)軟件，同時(shí)探索所有可能的執(zhí)行路徑，而無(wú)需指定具體值。具體示例如下，其中輸入x未知，即符號(hào)：
符號(hào)執(zhí)行在所有三個(gè)執(zhí)行路徑(x < 0, x > 100, 0 < = x < =100)并生成三個(gè)具體的測(cè)試用例：x=-1, x=101和x=23在擊中斷言之后。
你不再需要手動(dòng)編寫測(cè)試用例，你會(huì)沿執(zhí)行路徑捕獲斷言失敗和內(nèi)存安全漏洞。以上說(shuō)的可不是理論層面上的事情，哪這種方法可以在實(shí)踐中用于實(shí)際程序嗎?
KLEE
KLEE是一個(gè)符號(hào)執(zhí)行引擎，可對(duì)任何輸入執(zhí)行未修改的真實(shí)程序。你將程序編譯為L(zhǎng)LVM位碼，將某些輸入標(biāo)記為符號(hào)，然后啟動(dòng)KLEE。 KLEE使用約束解決方案探索可能的執(zhí)行路徑，并為每個(gè)路徑生成具體的測(cè)試用例。如果發(fā)生漏洞，你可以使用觸發(fā)它的輸入來(lái)重播程序。
2019年11月，關(guān)于KLEE的OSDI 2008開創(chuàng)性論文被選入ACM SIGOPS名人堂。在過(guò)去的十年里，KLEE的研究和應(yīng)用產(chǎn)生了超過(guò)150篇科學(xué)出版物、數(shù)十篇博士論文、研究資助、工具和安全初創(chuàng)公司。
使用KLEE測(cè)試網(wǎng)絡(luò)協(xié)議
在2007年，我一直努力尋找自己的研究論文，直到遇到Cristian Cadar的論文“EXE: Automatically Generating Inputs of Death“EXE: Automatically Generating Inputs of Death”。受到符號(hào)執(zhí)行思想的啟發(fā)，在將傳入的網(wǎng)絡(luò)數(shù)據(jù)包傳遞到網(wǎng)絡(luò)堆棧之前，可以標(biāo)記它的協(xié)議報(bào)頭嗎?如果是這樣，我可以用這種技術(shù)找到協(xié)議規(guī)范和實(shí)現(xiàn)漏洞嗎?
于是研究人員寫了一封電子郵件給Cristian Cadar，并迅速收到了答復(fù)。而且，Cristian和Daniel Dunbar慷慨地向它發(fā)送了KLEE的源代碼，這是他們正在使用的新工具，目前還尚未對(duì)外公布。
接下來(lái)我擴(kuò)展了KLEE以執(zhí)行相互通信的多個(gè)協(xié)議棧。我將此技術(shù)用于測(cè)試傳感器網(wǎng)絡(luò)，并在我的IPSN 2010論文中描述的Contiki OS中發(fā)現(xiàn)了兩個(gè)有趣的漏洞。其中一個(gè)導(dǎo)致了TCP/IP堆棧內(nèi)的傳感器節(jié)點(diǎn)的死鎖，需要重新設(shè)置硬件，這是在傳感器網(wǎng)絡(luò)部署中觀察到的真正漏洞。死鎖是指兩個(gè)或兩個(gè)以上的進(jìn)程在執(zhí)行過(guò)程中，由于競(jìng)爭(zhēng)資源或者由于彼此通信而造成的一種阻塞的現(xiàn)象，若無(wú)外力作用，它們都將無(wú)法推進(jìn)下去。此時(shí)稱系統(tǒng)處于死鎖狀態(tài)或系統(tǒng)產(chǎn)生了死鎖，這些永遠(yuǎn)在互相等待的進(jìn)程稱為死鎖進(jìn)程。
自2015年以來(lái)，我一直沒(méi)有過(guò)多使用過(guò)KLEE，并且想再次嘗試一下。同時(shí)，Contiki OS已拷貝到Contiki-NG。我復(fù)制了存儲(chǔ)庫(kù)，并將稱為20-packet-parsing的測(cè)試用例編譯為L(zhǎng)LVM位碼。在測(cè)試用例中，我使用KLEE的klee_make_symbolic函數(shù)標(biāo)記了測(cè)試數(shù)據(jù)包緩沖區(qū)(?1KB)的符號(hào)。Contiki-NG是一套用于下一代IoT(物聯(lián)網(wǎng))設(shè)備的開源跨平臺(tái)操作系統(tǒng)，可適用于獨(dú)立高防服務(wù)器。
在我的舊Mac上運(yùn)行了幾分鐘后，KLEE在解析某些協(xié)議的標(biāo)頭時(shí)發(fā)現(xiàn)了兩個(gè)內(nèi)存漏洞(指針超出范圍)。我將這些發(fā)現(xiàn)與具體的測(cè)試案例一起報(bào)告給Contiki-NG的安全團(tuán)隊(duì)，以進(jìn)行進(jìn)一步的分析。對(duì)我來(lái)說(shuō)，這個(gè)小測(cè)試是KLEE仍然是有用的研究和測(cè)試案例生成工具的又一個(gè)證據(jù)。
開放的挑戰(zhàn)和機(jī)遇
將符號(hào)執(zhí)行應(yīng)用于任意真實(shí)程序很難，你通常必須對(duì)執(zhí)行環(huán)境建模，并找到有效的方法來(lái)應(yīng)對(duì)不確定性和路徑爆炸。 而且，許多路徑約束很難解決，但是對(duì)于當(dāng)今的求解器而言難以及時(shí)解決。
盡管如此，研究和應(yīng)用符號(hào)執(zhí)行(使用KLEE)仍會(huì)帶來(lái)許多機(jī)會(huì)。你將了解程序結(jié)構(gòu)，編譯器，SAT / SMT求解器，以及如何編寫其他類型的測(cè)試工具。基于這些知識(shí)，我編寫了模糊Android應(yīng)用程序的工具，超級(jí)優(yōu)化LLVM IR，以及最近在工作中使用拼寫編寫的模糊衛(wèi)星控制程序的工具。
本文翻譯自：https://sasnauskas.eu/finding-software-bugs-using-symbolic-execution/
網(wǎng)頁(yè)題目：利用 KLEE 符號(hào)執(zhí)行引擎挖掘軟件漏洞
當(dāng)前路徑：http://m.5511xx.com/article/codppoo.html
