操作利用非典型之擬真執行

Exploiting Atypical Symbolic Executions

邱世欣(Shih-Hsin Chiu)

指導教授 ： 黃世昆

國立交通大學/資訊學院/資訊科學與工程研究所/碩士(2011年)

https://doi.org/10.6842/NCTU.2011.00313

摘要

軟體安全日漸成為重要的研究主題，起因於越來越多的軟體攻擊行為發生，這些狀況有一部份是源自於程式語言本身的缺陷，而另一方面也是程式設計師本身的粗心所導致。因此，我們將藉由軟體偵測技術以減少這些問題。在論文中探討目前被廣泛運用的的程式漏洞-緩衝區溢位(Buffer overflow)，例如西元2003年八月造成重大損失的疾風(Blaster)病毒即利用此種漏洞進行破壞。為了防止此類型的漏洞，本論文使用KLEE的符號執行模組(symbolic execution model)並引入新的記憶體對映機制(memory map)來探測緩衝區溢位。相較於傳統的檢測工具，本論文所提出的工具可確實產生、可利用的測資來觸發漏洞的行為，進而證實漏洞的存在。這些測資事實上就是一組攻擊字串，有別於駭客手動方式產生，我們將提出自動產生的方法。

關鍵字

擬真執行 ； 緩衝區溢位

並列摘要

Software security is getting more important recently. There are more and more attacks than before. It is partially due to some design flaws of the programming language and the lack of secure programming practices by programmers. The most serious vulnerability this thesis concerns with is buffer overflow, present in many C/C++ programs, such as the Blaster worm. For preventing from such vulnerabilities, we use symbolic execution with a new memory model supported by KLEE to detect buffer overflow vulnerabilities. This thesis actually generates an exploitable input to trigger buffer overflow and verify the presence of the vulnerability. The input suites we generate are realistic attacks. Unlike the usual hacking methods with manual techniques to reason on the tainting paths, we propose methods to generate exploitable input automatically.

並列關鍵字

symbolic execution ； buffer overflow

參考文獻

[21] R. Majumdar and K. Sen. Latest: Lazy dynamic test input generation. Technical Report UCB/EECS-2007-36, EECS Department, University of California, Berkeley, 2007.

[26] You-Siang Lin. CAST: Automatic and Dynamic Software Verification Tool, NCTU , Master thesis, 2009

[27] Richard W M Jones and Paul H J Kelly. Backwards-compatible bounds checking for arrays and pointers in C programs. Department of Computing Imperial College if Science, Technology and Medicine 180 Queen’s Gate, London.

[1] C. Lattner and V. Adve. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In CGO , 2004.

[4] E. Haugh and M. Bishop. Testing C programs for buffer overflow vulnerabilities. In Proceedings of the Network and Distributed System Security Symposium, February 2003.