Correctness Analysis Of An Algorithm For Memory Safety Dynamic Detection Based On Theorem Proving

Computer software systems have been used on a large scale in key security areas such as defense,finance,communications,and medical care.Many software in these fields are developed in C language.While enjoying the efficient operation efficiency of C language,they also need to bear the memory security risks brought by C language pointer operations.In order to build a highly reliable software system.Many memory security detection tools for C language are widely used.These tools use code instrumentation to achieve runtime detection of memory security errors.However,none of these memory security detection tools and their algorithms have been rigorously proven to be correct,which brings two problems.First,the inserted program may change the behavior and semantics of the original program,leading to changes in the execution results of the original program.Second,we cannot ensure that the detection algorithm can detect all memory security errors it targets.Therefore,how to prove the reliability and effectiveness of the memory security detection tool and its algorithm itself has become a crucial issue.Aiming at the above two problems,this paper proposes a correctness proof method of the memory security dynamic detection algorithm based on theorem proof,and uses this method to complete the correctness proof of the algorithm of the C language memory security dynamic detection tool Movec,Specifically,the work of this article mainly includes the following three parts:First,we formally define the syntax and semantics of the core subset of the C language and the instrumentation semantics of the Movec memory security detection algorithm.We have realized the formal representation of C language types,operation syntax and semantics through the functional programming language built in Coq.Based on these formal definitions,we can prove two correctness attributes of the detection algorithm: behavior invariance and memory security.Second,we prove the invariance of the behavior of Movec algorithm,that is,all the instrumentation behavior will not change the behavior and semantics of the original program,mainly by deriving the original function of C language through the formal specification of the Movec packaging function Method to prove the invariance of the behavior of Movec algorithm.Third,we proved the memory security of Movec algorithm,that is,the algorithm can detect typical time and space memory security errors at runtime.First,we define a well-structured environment that satisfies the memory security specifications,and then combine the nature of Movec instrumentation operations and related axioms to prove the memory security maintained by memory operations.Finally,we use the famous Coq interactive theorem prover to implement all the above formal definitions,and automatically prove the above two correctness attributes,verifying the effectiveness of the method in this paper.