Assembly Instruction Simulation System Based On Isabelle And A Suitable Tool For Instruction Translation And Assisted Verification

With the popularity of computers in the medicine, aerospace, finance and other fields, to protect the safety of our computer’s operating system becomes increasingly important. Currently academia and industry has a lot of research on operating system security, but so far, still no operating system can ensure the realization of the intended requirement, without any errors.Currently, the most accepted method is using formal method in the design and implementation of the operating system for verification. Formal method is the use of a variety of techniques based on mathematical logic and verification to guide the software and hardware design, development and validation. The use of formal method to guide the design and verification of operating systems, including the use of rigorous mathematical formalism to describe the behavior of the operating system and semantics, semantic model to build the operating system, and verify its code to achieve the functional requirements of the design. This method is called formal verification.Based on the VTOS verification model, we improve to achieve the assembly instruction simulation system based on Isabelle which can be used for process simulation, status view and functional verification, while achieving an assisted instruction translation and verification tools which is adapted to the simulation system. Specific content:1. Construct the register group, instruction set, RAM, ALU with flags and instructions’fetch, interpretation and implementation corresponding to the von Neumann architecture machines. These elements constitute an assembly instruction simulation system, that can be used to simulate program’s execution. Use the Hoare Logic to express the relationship between state after each instruction execution and the initial state. Use formal language to describe the program requirement for functional verification.2. Use C language to implement a tool adapted to the assembly instruction simulation system for instruction translation and assisted verification to reduce manual workload.3. Use a simple program to show program’s simulation and its functional verification.