標題: 記憶空間釋放再利用之安全漏洞自動探索與發掘
Automatic Path Inference and Input Reasoning for Use-After-Free Vulnerability Discovery
作者: 陳祐任
謝續平
Chen, Yu-Jen
Shieh, Shiuh-Pyng
資訊科學與工程研究所
關鍵字: 程式分析;釋放後使用漏洞;符號執行;動態符號執行;自動化;漏洞偵測;軟體漏洞;Program Analysis;Use-After-Free Vulnerability;Symbolic Execution;Concolic Execution;Automatic;Vulnerability Detection;Software Vulnerability
公開日期: 2016
摘要: 釋放後使用漏洞(Use-After-Free vulnerability)時常發生在程式當中的堆積記憶體(Heap memory),其漏洞對於現今日常生活所使用的軟體(例如瀏覽器、作業系統核心、媒體播放器......等等)均造成嚴重的程式安全問題。造成此漏洞的原因主要來自於動態記憶體管理函式庫的不當使用,以及程式當中因為一些程式邏輯上的錯誤導致了懸空指標(Dangling pointer)的產生。程式當中如果存在釋放後使用漏洞,將容易導致其產生不可預期的行為,例如記憶體被破壞(Memory corruption)、人工代碼執行(Arbitrary code execution)......等等。 我們提出了一套系統,藉由靜態分析以及動態符號執行技術(Concolic execution)來自動化偵測一支二進制檔案的釋放後使用漏洞。此系統透過我們提出的一套釋放後使用漏洞的特徵模型,將一支二進制檔案當中的執行路徑進行過濾與純化,進而萃取出含有釋放後使用漏洞的執行路徑。此外,我們還提出了一種以執行路徑目標為導向的動態符號執行技術(Target-oriented Concolic Execution),能夠將萃取出來的執行路徑進行可到達性(Reachability)以及釋放後使用漏洞存在性的驗證,並且產生出一組對應此執行路徑、能夠觸發此漏洞的輸入,做為程式存在釋放後使用漏洞的證明。我們的研究也對提出來的系統做驗證,而結果顯示我們擁有極高的漏洞偵測正確率以及極高的無關路徑排除率,意即我們排除掉了相當多的與釋放後使用漏洞無關的執行路徑。
Use-After-Free (UAF) vulnerabilities in the heap memory space have been causing lots of security issues nowadays. Our daily use software like browsers, OS kernel, media players, etc. all suffer from the UAF vulnerabilities. The vulnerabilities are mainly caused by the misuse of the dynamic memory management libraries and the creation of dangling pointers. With an adversary crafted input, the UAF vulnerabilities may lead a program into unpredictable behaviors, such as memory corruption and arbitrary code execution. In this paper, we present HVA (Heap Vulnerability Analyzer), which leverages static analysis and concolic execution to automatically detect UAF vulnerabilities in a binary program. We propose a UAF specification model that help HVA eliminate and purify the execution paths with UAF vulnerabilities during the static analysis. We also proposed target-oriented concolic execution, a concolic execution technique to recover the input sequence lead to certain path. With the help of target-oriented concolic execution, HVA can precisely verify the vulnerabilities and generate the input as the proof of the UAF vulnerabilities. HVA is evaluated against 366 binaries from the NIST's Juliet Test Suite, and the result shows that HVA is effective in eliminating non-UAF related execution paths, and achieves high accuracy of detecting UAF vulnerabilities without the false positive.
URI: http://etd.lib.nctu.edu.tw/cdrfb3/record/nctu/#GT070356036
http://hdl.handle.net/11536/139294
Appears in Collections:Thesis