本文選題：缺陷檢測 + 程序靜態(tài)分析�。� 參考：《北京郵電大學(xué)》2016年碩士論文

【摘要】：隨著計(jì)算機(jī)軟件在數(shù)量和規(guī)模上不斷地增加,傳統(tǒng)的用于發(fā)掘軟件缺陷的人工測試的方式效率低下、成本較高的缺點(diǎn)逐漸暴露出來,一些新的、自動化的方法被用來完成程序缺陷分析這部分工作。程序分析技術(shù)作為一種自動化對程序缺陷分析的技術(shù),無論在學(xué)術(shù)界還是在工業(yè)界都有深入的研究和使用,目前這些技術(shù)已經(jīng)逐步替代傳統(tǒng)的方式。程序分析技術(shù)根據(jù)程序是否會被運(yùn)行分為程序動態(tài)分析技術(shù)和程序靜態(tài)分析技術(shù),程序動態(tài)分析技術(shù)根據(jù)通過對程序進(jìn)行反匯編,得到匯編代碼,或者進(jìn)行指令插樁,或者采用虛擬機(jī)模擬運(yùn)行,通過這樣種方式對程序進(jìn)行分析。程序靜態(tài)分析技術(shù)則不會運(yùn)行程序,通過對程序源代碼或者經(jīng)過源代碼編譯生成的中間代碼進(jìn)行分析,一般采用的技術(shù)包括,控制流分析、數(shù)據(jù)流分析、模型檢測、污點(diǎn)分析和符號執(zhí)行等,它們各自都有優(yōu)缺點(diǎn)。本文使用靜態(tài)程序方法作為主要的方式對程序缺陷進(jìn)行分析,采用符號執(zhí)行技術(shù)+SMT求解,實(shí)現(xiàn)了一個(gè)靜態(tài)分析工具——MLSA。MLS A使用LLVMIR(LLVM編譯器框架的中間語言)作為分析對象,采用符號執(zhí)行技術(shù),記錄程序變量的符號值,對于檢測指令和分支指令使用SMT求解判定程序是否存在缺陷和路徑的可達(dá)性問題。MLSA作為一個(gè)靜態(tài)分析工具,能夠完成過程內(nèi)和過程間分析,目前主要針對C++語言的除零、指針越界訪問和死代碼三類缺陷進(jìn)行分析,并支持分析Fortran語言的除零、數(shù)組越界程序缺陷。經(jīng)過實(shí)驗(yàn)表明MLSA具有實(shí)用工具缺陷分析能力。
[Abstract]:As the number and scale of computer software continue to increase, the traditional manual testing methods used to discover software defects are inefficient, and the disadvantages of higher cost are gradually exposed. Automated methods are used to complete this part of the program defect analysis. As a kind of automatic defect analysis technology, program analysis technology has been deeply studied and used in both academia and industry. At present, these technologies have gradually replaced the traditional methods. Program analysis technology is divided into program dynamic analysis technology and program static analysis technology according to whether the program will be run. According to the program dynamic analysis technology, according to the disassembly of the program, the assembly code is obtained, or the instruction pile is inserted. Or use virtual machine simulation to run, through this way to analyze the program. The program static analysis technology will not run the program, by analyzing the program source code or the intermediate code generated by the source code compilation, the commonly used techniques include, control flow analysis, data flow analysis, model checking, Stain analysis and symbol execution have their own advantages and disadvantages. In this paper, the static program method is used as the main way to analyze the program defects, and the symbolic execution technique SMT is used to solve the problem. A static analysis tool, MLSA.MLSA, using the intermediate language of the LLVMIR(LLVM compiler framework, is implemented as the analysis object. The symbolic execution technique is used to record the symbolic values of program variables. For detecting instructions and branch instructions, SMT is used to solve the reachability problem of whether the program has defects and paths. MLSA is used as a static analysis tool. At present, it mainly analyzes three kinds of defects of C language, such as removing zero, pointer overstepping access and dead code, and supports the analysis of Fortran language's zero removing and array crossing program defect. The experimental results show that MLSA has the ability to analyze the defects of practical tools.
【學(xué)位授予單位】：北京郵電大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2016
【分類號】：TP311.53

【參考文獻(xiàn)】

相關(guān)期刊論文 前1條

1 金繼偉;馬菲菲;張健;;SMT求解技術(shù)簡述[J];計(jì)算機(jī)科學(xué)與探索;2015年07期

，

本文編號：1886660