Research And Implementation Of Automatic Verification Technology For Mixed Code Of C And Assembly Language

With the continuous development of software engineering technology,the functions of software have become more and more abundant,which brings great convenience to people's lives.However,the complexity and diversity of software also make software security vulnerabilities increase day by day.The software testing method shows that the software has some security vulnerabilities,but it cannot guarantee that the software does not have certain security vulnerabilities.In contrast,the formal verification method can do this.As the basic system software,the security of the operating system is very important.Using the formal verification method to verify the implementation code of the operating system kernel is an effective way to ensure its security and correctness.The kernel implementation code of the operating system is mostly mixed code of C and assembly,if the traditional formal verification method is used for verification,there are problems such as high manual participation,low verification efficiency and high verification complexity.Therefore,with the automatic formal verification of mixed code as the research background,this thesis focus on the automatic formal verification technology and implementation method of mixed code.The main work of this thesis is as follows:(1)Based on model checking technology,an automatic formal verification method for assembly code is proposed.In order to improve the verification efficiency and reduce the verification workload,an ARM assembly instruction model library is constructed.The model library provides a unified interface for the modeling and verification of ARM assembly code.The model library can be used to easily abstract the assembly code and verification.(2)Aiming at the problems of modeling difficulty and high verification complexity caused by nested calls of C code and assembly code in mixed code,a modeling and verification method of mixed code is proposed.Compiling and abstracting the C code in mixed code makes it possible to verify C language and assembly language code at a unified abstraction level,which greatly improves the verification efficiency.Verification support for interrupt handlers is also added to the mixed code verification method,and the resulting model state explosion problem is solved using an interrupt execution prediction algorithm.(3)In order to further improve the automation degree of mixed code verification,an automatic formal verification tool for mixed code is developed based on the automatic formal verification method of mixed code proposed in this thesis.The tool supporting functional correctness verification of C code,automatic analysis of mixed code to generate abstract model,and security attribute verification.The tool is used to verify the mixed code functions in ?C/OS-II operating system,showing the convenience of using the tool and the effectiveness of the verification method.