Formal Modeling And Analysis Of Ultra-risky Vulnerability Exploitation Based On Petri Nets

In contemporary communities,computer networks have already been an integral role in our ordinary living.However,as the rapid development of Internet technology,the security vulnerabilities of the online system are gradually brought to the surface,and the attackers use the system vulnerabilities to launch malicious attacks and raise serious challenges to the privacy protection of individuals and national security protection.The super critical vulnerabilities not only have a wide range of impact,but also seriously affect the normal security operation of the network,which is a pressing issue of cyber security to be dealt with.In this paper,a formal modeling and analysis method based on Petri nets is proposed for the typical super critical vulnerabilities disclosed publicly.The method is based on the key code in the exploitation process of super critical vulnerabilities,analyzes the internal operation logic of the program,and constructs a vulnerability exploitation model based on Petri nets.Then the Petri net model of super-risk vulnerabilities is simulated and analyzed by tools,and finally the patch model of vulnerabilities is constructed.The major research efforts of this document consist of the following aspects :(1)The Petri net model for the hyper-risk vulnerabilities CVE-2014-6271 and CVE-2021-3711 is proposed.The model starts from the underlying principle of the system,and analyzes the relationship between the exploitation process of the hyper-risk vulnerability and the place and transition in Petri net and completes the mapping by exploring the key function calls in the process of vulnerability exploitation,and constructs a Petri net-based hyper-risk vulnerability exploitation model,which provides a formal description of the process of hyper-risk vulnerability exploitation.(2)A model validation method based on the Tina tool is investigated.The Petri net model of the super critical vulnerability CVE-2014-6271 and CVE-2021-3711 is simulated,and the correctness of the structure of the model is verified by observing the flow of model token.For the problem of path time spent for the first arrival of token to the secure and insecure states in the model,ten sets of times are counted and averaged for processing respectively.According to the experimental results,the time of model simulation is less than the time to complete the actual vulnerability attack,and the model achieves ultra real-time simulation.(3)A patching model for super critical vulnerabilities is proposed.By studying the key code for patching super critical vulnerabilities and adding the library place with variation so that the token cannot reach the system insecure state,the patching models for CVE-2014-6271 and CVE-2021-3711 are proposed respectively.In turn,according to the model to observe the library place where token should not reach,certain restrictions can be added to the path,which provides a theoretical reference method for vulnerability patching.