Model,Methods And Tools For Formal Verification Of Assembly Language

With the increasing of software complexity,it is much more difficult to guarantee the correctness of software.While it is possible to minimize the occurrence of errors through extensive testing,but it is difficult to ensure correctness.Formal verification of software is recognized as the most reliable method to guarantee the correctness of software.But most of the existing formal verification methods are for high-level languages such as C,which requires the assumption of the correctness of the compiler.In addition,most of these methods are highly complex and requires a lot of manpower and time.This paper presents a new method to construct simulation environment in Isabelle and to perform formal verification of the assembly language directly in it.Since the assembly code and machine code are highly consistent,so the verification or the assumption of the correctness of the compiler can be avoided.In addition,using automatic scripts as much as possible will aid in the verification process.Although the proof process cannot be fully automated,but at least we can improve the efficiency of formal verification.This article consists of the following sections:1.Build a simulation environment in Isabelle to analog ALU,controller,registers,memory,Intel IA32 instruction set and so on.Translate the assembly instruction into the model,execute the program at the weakest precondition and record the changes in the system state.Ultimately we can get the relationship between the terminate state and the initial state of the system,which can be used as the basis of the following proof.2.Present methods to prove three kinds of code structure:the order structure,the branch structure and the loop structure,and methods to deal with procedure call.Among them,the proof of the loop structure is relatively more important.It can deal with two kinds of common loops:one is the indefinite loop iteration on linkedlist,and two is the definite loop iteration of some general loops.Method to carry on the proof after exiting the loop has also been given.Through an application of the above methods,we come to meaningful conclusions eventually.3.Using Python to translate the assembly code to the model,which can improve the accuracy and efficiency of translation,and to automatically generate the framework of the proof so the prover can focus on logical reasoning,not writing prove scripts.