Formal Verification Of SPARCv8 Assembly Code

System software is the core part of the computer system.Its safety and reliability are important to build high confidence system.Formal verification is based on rigorous mathematical theories and methods,and can provide a strong guarantee for the correct-ness of system software.In system software,inline assembly code is usually used to interact with low-level hardware platform.So,safety and correctness of the assembly code is crucial to guarantee the safety of the whole system.In our current formal verifi-cation project of an aerospace embedded operating system,the operating system's^inline assembly codes are implemented by SPARCv8·However,the verification framework used previously cannot verify the correctness of this part of assembly code.In order to improve this part of work,this paper proposes a method for formal verificaiton of SPARCv8 assembly code.It is based on the existing technology about formal verifi-cation,and makes the following contributions:First,we design a Hoare-style program logic for SPARCv8,and give direct-style semantic interperation for the logic judgement.Our logic supports modular verification of function call,and three main features of SPARCv8:delayed control transfer,delayed write and register windows.Second,we use our logic to verify the main body of context switch routine in a realistics embedded OS kemal for aerospace crafts,which consists of around 250 lines of SPARCv8 code.The definition of our logic,soundness proof and verification work for context switch routine are all mechanized in Coq.Finally,we propose a simulation relation between the SPARCv8 program and its corresponding abstract assembly primitive.We prove that if the SPARCv8 program and an assembly primitive satisfy this simulation relation,then they satisfy the con-textual refinement,which means the programs call this SPARCv8 program will not produce more behaviors than the program call this assembly primitive.We use this method to verify that a context switch routine implemented by SPARCv8 satisfies this simulation relation with the swit ch primitive.