Research On Formal Automatic Modeling Of Security Protocol Source Code

With the continuous development of emerging technologies such as big data,artificial intelligence and 5G,threats to computer networks are increasing.According to the analysis of relevant data,the potential global economic losses caused by network attacks could be as high as $294 billion between 2015 and 2025.The escalation of network risks has made both academia and industry pay more attention to network security issues.In computer system,security protocols based on cryptography provides the basic guarantee for network security.However,the running environment of the security protocols is usually insecure.Once the design of the protocols is defective,it will cause irreversible consequences.In recent years,formal analysis techniques have been widely used in security protocol verification and have made outstanding achievements.The formal analysis technology can be roughly divided into modeling and verification.Automatic verification with tools has been realized,but the modeling process still relies on manual modeling by professionals,which is difficult and costly,limiting the further promotion of this technology.In order to improve the automation degree of formal analysis technology,automatic modeling technology is indispensable in addition to the further development of automatic verification technology.Among the existing formal tools for security protocol verification,Tamarin-prover has the most extensive verification ability.Therefore,based on the basic theory of Tamarin-prover,this thesis proposes the scheme for automatic formal modeling based on security protocol code from two perspectives.The main work and contributions of this thesis are as follows:(1)Automatic formal modeling based on taint analysisProposes a formal automatic modeling scheme based on taint analysis.The manual establishment of formal models is based on the specification of security protocols,which is long and descriptive,requiring experts to carefully study and then filtrate modeling information.In order to facilitate computer automatic extraction of modeling information,the security protocol code is selected as the research object in this thesis.First,the communication flow of the protocol is captured using taint analysis and the cryptographic primitive operations are recorded.Then,the protocol communication state machine is constructed according to the sequential relationship between communication processes.Finally,a formal model is generated according to the modeling syntax of Tamarin,a popular security protocol formal analysis tool.The experimental results show that this scheme can generate the key parts of the formal model,improving the degree of automation of the formal modeling and contributing to the popularization of the formal analysis technology.(2)Automatic formal modeling for Proof-of-correctness of program semanticsThe automatic modeling method for semantic correctness proof of program is further explored from a more formal perspective.First,a conversion function is designed according to the core semantics of C language,which converts the main statements and function calls in the protocol code into formal model rules conforming to Tamarinprover input specification.Then,the security attribute and the attacker capabilities are modeled,combined with the aforementioned formal model rules as a complete protocol model.Finally,based on the underlying principle of Tamarin-prover and K frame theory,the formal proof of this scheme is carried out to prove the correctness of it.