【作者】 张伟；

【导师】 张留美；

【作者基本信息】 西安石油大学 ， 计算机科学与技术， 2024， 硕士

【摘要】 现代社会中,计算机网络已经深深地渗透到人们的学习、工作和生活中,成为不可或缺的一部分。但伴随着技术的快速发展,网络系统中存在的安全漏洞数量和种类也在不断增长。攻击者利用系统和程序漏洞发起的恶意攻击,不仅对计算机系统和个人用户造成威胁,还对国家的安全防护发起严峻的挑战。尽管现有的漏洞利用研究已经可以发现大量的程序漏洞且漏洞利用的方式描述逐渐细化,但目前的研究缺少漏洞利用场景下细粒度的建模分析,对攻击场景下的细节描述也不够完备。本文以最普遍的栈溢出漏洞为研究对象,提出了一种基于Petri网的形式化建模与检测方法。该方法以栈溢漏洞利用过程中的攻击负载信息为基础,分析函数栈内的布局和控制流的转移,从而构建了基于Petri网的漏洞利用执行过程模型,接着在源码的基础下,使用带有彩色令牌的Petri网建立了栈溢出漏洞检测网。以下是本文的主要内容概述。(1)提出了面向栈溢出漏洞利用的Petri网模型。模型从系统的底层原理入手,分析了多种栈溢出漏洞利用方法,探究栈内构造恶意负载后的函数调用过程,通过分析漏洞利用过程的关键状态与行为,建立了其与Petri网中库所、变迁的映射关系,对栈溢出漏洞利用的执行过程进行了形式化表征,并在对关键路径进行分析选择后,构建了基于Petri网的栈溢出自动漏洞利用模型。(2)提出了针对栈溢出漏洞的检测网模型。为了有效地检测和定位栈溢出漏洞,本研究以C程序源代码为分析对象,通过将数据依赖图(Data Dependence Graph,DDG)和控制流图(Control Flow Graph,CFG)集成至Petri网框架中,并采用了彩色令牌Petri网(Colored Petri Net)的表示方法,以及定义了可以识别和追踪潜在的数据污染传播路径的网模型执行规则,构建了面向栈溢出漏洞的检测网模型,不仅为栈溢出漏洞提供了有效的可利用状态搜索方案,同时为软件安全分析提供了一种新的视角和方法。(3)研究了基于Tina工具与符号执行技术的模型验证方法。首先使用Tina工具对Petri网模型进行模拟仿真实验,通过观察模型中令牌的流动情况,对模型结构的可达性和正确性进行分析验证。其次使用Angr符号执行框架和Radare2动态分析工具对具有堆栈缓冲区溢出漏洞的CTF(Capture The Flag)和CVE(Common Vulnerabilities and Exposures)程序进行漏洞利用实验,并将其与Zeratool漏洞利用工具进行对比分析,结果表明,文中模型能够对漏洞点进行有效检测并实现四种不同的栈溢出漏洞利用方法,从而验证了模型的可行性。更多还原

【Abstract】 In modern society,computer networks have deeply penetrated into people’s learning,work and life,becoming an indispensable part.However,along with the rapid development of technology,the number and types of security vulnerabilities existing in network systems are also growing.Malicious attacks launched by attackers using system and program vulnerabilities not only pose a threat to computer systems and individual users,but also pose a serious challenge to national security protection.Although the existing vulnerability exploitation research has been able to find a large number of program vulnerabilities and the description of vulnerability exploitation gradually refined,but the current research lacks of vulnerability exploitation scenarios under the fine-grained modeling analysis,the details of the attack scenarios under the description is not complete.This paper takes the most common stack overflow vulnerability as the research object,and proposes a formal modeling and detection method based on Petri nets.The method is based on the attack load information in the process of stack overflow vulnerability exploitation,and analyzes the layout and control flow transfer within the function stack,so as to construct a Petri net-based model of the execution process of vulnerability exploitation,and then establishes a stack overflow vulnerability detection net using Petri nets with colored tokens on the basis of the source code.The following is a summary of the main contents of this paper.The research work of this paper mainly includes the following aspects:(1)A Petri net model for stack overflow vulnerability exploitation is proposed.The model starts from the underlying principle of the system,analyzes a variety of stack overflow vulnerability exploitation methods,explores the function call process after constructing malicious loads in the stack,establishes the mapping relationship between the key states and behaviors of the vulnerability exploitation process and the libraries and variations in the Petri nets by analyzing the key states and behaviors of the vulnerability exploitation process,and formally characterizes the execution process of the stack overflow vulnerability exploitation,and constructs the key paths after analyzing the critical paths and selecting the key paths.automatic stack overflow vulnerability exploitation model based on Petri net.(2)A detection net model for stack overflow vulnerabilities is proposed.In order to effectively detect and locate stack overflow vulnerabilities,this study takes the C program source code as the object of analysis,by integrating Data Dependence Graph(DDG)and Control Flow Graph(CFG)into the Petri net framework,and adopts the Colored Token Petri net(Colored Petri Net)representation,as well as the definition of net model execution rules that can identify and track potential data contamination propagation paths,constructed a stack overflow vulnerability-oriented detection net model,which not only provides an effective exploitable state search scheme for stack overflow vulnerabilities,but also provides a new perspective and method for software security analysis.(3)The model verification method based on Tina tool and symbolic execution technique is studied.Firstly,the Tina tool is used to simulate the Petri net model to analyze and verify the accessibility and correctness of the model structure by observing the flow of tokens in the model.Secondly,we use angr symbolic execution framework and radare2 dynamic analysis tool to conduct vulnerability exploitation experiments on CTF(Capture The Flag)and CVE(Common Vulnerabilities and Exposures)programs with stack buffer overflow vulnerabilities,and conduct comparative analyses with Zeratool vulnerability exploitation tool.Comparison analysis,the results show that the model in the paper can effectively detect the vulnerability points and realize four different stack overflow vulnerability exploitation methods,thus verifying the feasibility of the model.更多还原