具目標認知符號執行模糊測試框架

Abstract

軟體設計不良所產生的漏洞，例如buffer overflows、integer overflows、uncontrolled format strings和command injections等，這些問題常被駭客操作使用、入侵使用者個人電腦或伺服器。Windows和Linux上的應用程式，或作業系統本身不時發布安全性更新就是為了修補這樣的問題。 為了減少軟體的漏洞，有許多測試方法被提出來，其中最常使用的是模糊測試（fuzz testing）。但傳統的模糊測試必須執行到程式出現例外情況（如失控）才能發現該問題，導致覆蓋率不足時無法發現受測程式的漏洞，忽略可能存在的安全威脅。 本篇論文提出使用S2E以symbolic execution為基礎的軟體測試架構，能在程式正常執行到某些自訂的敏感函式，例如malloc、strcpy和printf時，自動判斷此程式執行路徑在此位置是否可能造成安全性的威脅，若是，則進一步產生exploit的概念驗證（proof of concept），以及相對應的數學限制式。 我們運用此方法成功且有效地產生許多在CVE網站公開的漏洞，並能協助開發者迅速找到問題所在，提升維護軟體品質的效率。

Vulnerabilities caused by implementation bugs, such as buffer overflows, integer overflows, uncontrolled format strings, and command injections, are often exploited by hackers to intrude users’ personal computer or servers. In order to reduce software bugs, many testing techniques are proposed. The most frequently used technique is fuzz testing. However, traditional fuzzers can only find bugs when program exceptions, especially crashes, raised. That means some security threats may pass these tests due to the insufficient code coverage. In this thesis, we introduce a software testing framework based on symbolic execution using S2E, a whole system symbolic execution engine. When a program executes some pre-defined sensitive functions, such as malloc, strcpy or printf, our framework will initiate a triage process. It will determine whether any related security vulnerabilities would possibly occur in these functions automatically. If the answer is yes, a proof-of-concept exploit and its corresponding math constraints will be generated. We successfully and efficiently reproduce some CVE vulnerabilities, which means developers could locate bugs faster, and improve the efficiency of software quality maintenance.