2014SyScan360——程序分析及約束求解器
責編：admin ｜2014-07-17 19:07:202014年7月16日，由SyScan主辦，360公司承辦的SyScan360國際前瞻信息安全會議隆重召開。本次會議上匯集了來自美、意、西、葡等9個地區的18名頂級安全專家，向與會者分享安全領域最新的科研成果，議題涵蓋Window、ios、Android系統安全，汽車攻擊、云服務攻擊等諸多領域。
來自COSEINC的資深安全研究員的Edgar Barbosa為大家帶了關于《程序分析及約束求解器》的主題演講。Edgar Barbosa曾參與開發了虛機rootkit“Blue Pill”，并發表過幾篇論文。他擅長于內核開發、rootkit研究、逆向工程、硬件虛擬化及程序分析。
Edgar表示，程序分析更多的是要專注于特定的目標，即是要找到漏洞和Bug，逆向工程主要的工作就是要做漏洞的挖掘，結合逆向工程可以提取協議和格式的信息，其包括協議和文件解析器。
在演講中，Edgar首先針對漏洞挖掘時采用模糊測試用的Fuzzing 進行了基礎性的講解。他提到，Fuzzing有六個類別，一個是找到目標，二是生成數據，將謀劃的數據輸入執行程序，然后監視它的異常，是不是能夠被跟蹤，再驗證它的可用性。比如我們想要創造一個FTP服務器的Fuzzing需要產生一些隨機的數據，我們要了解FTP協議，而且它也需要一些其他的應用。
然而，Edgar表示，雖然模糊測試仍然是漏洞挖掘的有效手段，它能產生很多崩潰，這些崩潰作為分析問題的起點，用來確定漏洞的可利用性。但是對于某些具體的產品來說，Fuzzing并不是很有用。所以實現漏洞挖掘的自動化成為必要，自動化的實現可以讓用戶不必學習內部的知識，不必了解數據結構，不必了解新的格式和協議。對此，Edgar認為，實現漏洞挖掘自動化需要做到：
理解輸入數據時如何影響軟件的執行；
審計程序函數不需要包括協議和文件格式的任何先驗知識；
報告錯誤并立即分析出錯根源；
不產生誤報；
自動增加和程序路徑的覆蓋。
那么，如何才能做到以上幾個方面？Edgar認為，這需要把程序分析的問題能夠把它轉換成為約束求解器的問題來解決，然后讓約束求解器幫助解決問題。什么是約束求解器？約束求解器和約束編程的概念是一樣的，約束編程實際上是一個最接近的一種計算機科學的方法，它可以接近于編程方面的圣杯，它可以解決用戶面臨的問題。
Edgar說自己最喜歡的強大的SMT求解器是微軟的Z3，它能夠管理核心機管理的核心代碼的求解性，而且Z3在微軟的產品當中發現了好幾個漏洞。它是一個自動化的、可滿足性校驗的工具，對于所有的東西不需要理解，除非你想自己創建一個SMT的求解器，否則你不需要知道，而且在Linux、MAc、Windows上都可以用。
最后，Edgar展示了如何將x86匯編碼翻譯成中間語言和SMT公式，并就在程序分析時使用求解器的利與弊，求解器與污點數據分析的關系進行了討論。