Research On Methodology Of Formal Verification In Assembly Language And Its Application In VTOS Message Module Verification

With the development of the times,computer software plays an important role in the development of the financial,telecommunications,and other areas of business.As the core of computer software,operating system's reliability and security is essential for all computer software.The operating system's design and implementation is the basis of the correctness of their security,so finding a way to prove that the operating system has achieved the design goal is very important.The method of software testing can not give enough test cases to cover all the operating system state,so in this paper we use the formal method,currently recognized as the most reasonable and reliable way,to verify the correctness of the operating system functions.The formal method is based on rigorous mathematical logic system and uses a variety of reasoning verification techniques.If formal method's proof result is correct,we can say the operating system has achieved the design goal of the function.In this paper,we proof the assembly code and it is authenticated on the assembly level.Although we can describe the consistency better,but has made the verification more difficult.So in this paper,we studied the formal verification method,and got some conclusions.This paper makes the following study and contributions:1.Describe the operating system modules on the domain,and establish a formal model in Isabelle theorem prover.Use the domain as a bridge to indicate that the operating system model and the formal model is the same.2.Get the formal verification methods in Isabelle/HOL in assembly-level.Find an engineered-way to verify a sequential statement,including the oregular method for establishing front and post condition.On the basis of this method,according to the characteristics of the operating system,we proposed branch selection statement processing method,not only to reduce the verification time,but also reduces the difficulty of verification.3.VTOS(Verified Trusted Operating System)message module in Isabelle/HOL described and formal verification.We define the model's state-space and front-post-conditions,use the prove way of sequential statements to describe the the process of state change and use the prove way of loops and branching statements to describe correctness of message module.