Coq Verification Of Multiple Semantic Relations In C Language Expressions

Since the beginning of the 21st century,the degree of informatization of the entire society has become higher and higher,network information has exploded,and more and more information technology has entered everyone's life.The Internet of Things technology is becoming more and more diverse.And the accompanying computer system software and hardware security and reliability challenges are greater than in the past.Therefore,the realization of information security in the information age has become one of the current mainstream research directions,and the construction of high credibility system has become an important subject worldwide.In order to ensure the safety of software development and eliminate potential program hazards,we usually use logical reasoning systems to complete formal verification and achieve information security.An important direction is to achieve formal verification in the software development process.Using interactive mathematical proofs of theorems,modular proof writing methods have always been a major concern of researchers.In fields such as national defense,finance,and transportation that require extremely high security,formal verification has been widely used in research and application.This article first introduces the hidden dangers of C language in the process of program development and the latest developments in program verification at home and abroad,and then introduces and analyzes the basic tools of formal verification Coq,Comp Cert,VST,Hall logic and separation logic.On this basis,the C standard stipulates whether signed integer operations are out of bounds as an example for in-depth research.Based on Coq and VST tools,when performing formal verification on a section of C program,it is assumed that this section of program needs to be verified according to different compilation requirements.,According to different compilation requirements,set different verification specifications.This article uses the verification of plastic overflow as an undefined behavior as reference,studies and determines three different verification standards,and at the same time abstractly defines it in the way of functional programming in Coq language.As far as the interactive program verification tool VST is concerned,for different verification specifications,the basic architecture Verifiable C program logic is modified,and the various proof theorems involved are decomposed and re-proved to ensure the reliability of the entire VST tool program logic.Finally,it is demonstrated in detail in the VST,based on the Verifiable C program logic,through the interactive theorem prover Coq,to verify whether a section of C program s meets the reliability of Ps Q,where P is the pre-condition and Q is the post-condition,and the definition in VST is deeply deconstructed A formal framework for the semantics of C expressions.By comparing the advantages and disadvantages of the two formal writing methods,the high-level logic method and the module/module type method,the benefits of using the module/module type method to transform VST are analyzed in this article.The main improvement to the VST structure in this paper is the use of Module/Module Type class methods,focusing on formal verification of the semantics of C expression evaluation,decoupling the existing large-scale interactive theorem proofs,and implementing it through the modular transformation of VST Formal definition and formal proof based on separation logic;through the abstract definition of some key functions,it can perform different instantiations of the semantic verification specification for C expression evaluation according to the required scene,realize dynamic attribute configuration and some verification Parameterized setting of options;to ensure that the compiled C program does not run errors when VST verifies a series of high-level properties represented by functional correctness.The experimental results show that this project takes plastic overflow as an example to modularize the reconstruction and transformation of the VST verification logic framework.When different verification standards need to be implemented,only the Coq proofs related to the logic of each Verifiable C variant need to be called different AC module class instances.,It can ensure the end-to-end reliability of the C program under different compilation standards when verifying the C program related to the plastic overflow problem.At the same time,the VST modular transformation method in this article is also easy to extend the transformation scheme to other parts of the VST reliability certification,to realize the dynamic configuration of the VST verification specification,so that the reliability verification can be instantiated according to different needs.Thereby ensuring the integrity and reliability of the entire VST program logic.