2014年7月16日，由SyScan主辦，360公司承辦的SyScan360國際前瞻信息安全會(huì)議隆重召開。本次會(huì)議上匯集了來自美、意、西、葡等9個(gè)地區(qū)的18名頂級(jí)安全專家，向與會(huì)者分享安全領(lǐng)域最新的科研成果，議題涵蓋Window、ios、Android系統(tǒng)安全，汽車攻擊、云服務(wù)攻擊等諸多領(lǐng)域。

來自COSEINC的資深安全研究員的Edgar Barbosa為大家?guī)Я岁P(guān)于《程序分析及約束求解器》的主題演講。Edgar Barbosa曾參與開發(fā)了虛機(jī)rootkit“Blue Pill”，并發(fā)表過幾篇論文。他擅長(zhǎng)于內(nèi)核開發(fā)、rootkit研究、逆向工程、硬件虛擬化及程序分析。

COSEINC資深安全研究員 Edgar Barbosa

Edgar表示，程序分析更多的是要專注于特定的目標(biāo)，即是要找到漏洞和Bug，逆向工程主要的工作就是要做漏洞的挖掘，結(jié)合逆向工程可以提取協(xié)議和格式的信息，其包括協(xié)議和文件解析器。

在演講中，Edgar首先針對(duì)漏洞挖掘時(shí)采用模糊測(cè)試用的Fuzzing 進(jìn)行了基礎(chǔ)性的講解。他提到，F(xiàn)uzzing有六個(gè)類別，一個(gè)是找到目標(biāo)，二是生成數(shù)據(jù)，將謀劃的數(shù)據(jù)輸入執(zhí)行程序，然后監(jiān)視它的異常，是不是能夠被跟蹤，再驗(yàn)證它的可用性。比如我們想要?jiǎng)?chuàng)造一個(gè)FTP服務(wù)器的Fuzzing需要產(chǎn)生一些隨機(jī)的數(shù)據(jù)，我們要了解FTP協(xié)議，而且它也需要一些其他的應(yīng)用。

然而，Edgar表示，雖然模糊測(cè)試仍然是漏洞挖掘的有效手段，它能產(chǎn)生很多崩潰，這些崩潰作為分析問題的起點(diǎn)，用來確定漏洞的可利用性。但是對(duì)于某些具體的產(chǎn)品來說，F(xiàn)uzzing并不是很有用。所以實(shí)現(xiàn)漏洞挖掘的自動(dòng)化成為必要，自動(dòng)化的實(shí)現(xiàn)可以讓用戶不必學(xué)習(xí)內(nèi)部的知識(shí)，不必了解數(shù)據(jù)結(jié)構(gòu)，不必了解新的格式和協(xié)議。對(duì)此，Edgar認(rèn)為，實(shí)現(xiàn)漏洞挖掘自動(dòng)化需要做到：

◆理解輸入數(shù)據(jù)時(shí)如何影響軟件的執(zhí)行;

◆審計(jì)程序函數(shù)不需要包括協(xié)議和文件格式的任何先驗(yàn)知識(shí);

◆報(bào)告錯(cuò)誤并立即分析出錯(cuò)根源;

◆不產(chǎn)生誤報(bào);

◆自動(dòng)增加和程序路徑的覆蓋。

那么，如何才能做到以上幾個(gè)方面?Edgar認(rèn)為，這需要把程序分析的問題能夠把它轉(zhuǎn)換成為約束求解器的問題來解決，然后讓約束求解器幫助解決問題。什么是約束求解器?約束求解器和約束編程的概念是一樣的，約束編程實(shí)際上是一個(gè)最接近的一種計(jì)算機(jī)科學(xué)的方法，它可以接近于編程方面的圣杯，它可以解決用戶面臨的問題。

Edgar現(xiàn)場(chǎng)舉例演示

Edgar說自己最喜歡的強(qiáng)大的SMT求解器是微軟的Z3，它能夠管理核心機(jī)管理的核心代碼的求解性，而且Z3在微軟的產(chǎn)品當(dāng)中發(fā)現(xiàn)了好幾個(gè)漏洞。它是一個(gè)自動(dòng)化的、可滿足性校驗(yàn)的工具，對(duì)于所有的東西不需要理解，除非你想自己創(chuàng)建一個(gè)SMT的求解器，否則你不需要知道，而且在Linux、MAc、Windows上都可以用。

最后，Edgar展示了如何將x86匯編碼翻譯成中間語言和SMT公式，并就在程序分析時(shí)使用求解器的利與弊，求解器與污點(diǎn)數(shù)據(jù)分析的關(guān)系進(jìn)行了討論。