Automated Verification Framework for Mixed Code in Embedded Real Time Operating System Kernel

How to construct a trustworthy software system has become an important research area in academia and industry. As a basic component of the software system, the operating system kernel is an important component of constructing a trustworthy software system. In order to ensure the safety and reliability of an operating system kernel, this study introduces formal method into OS kernel verification, and proposes an automatically verifying framework. The verification framework includes following factors. (1) Separate C language programs and mixed language programs (for example, mixed language programs written by C and assembly language) for verification. (2) In the mixed language program verification, establish an abstract model for the assemble program, and then glue the C language program and the abstract model to form a verification model received by a C language verification tool. (3) Extract properties from the OS specification, and automatically verify properties based on a verification tool. (4) Do not limit to a specific hardware architecture. This study successfully applies the verification framework to verify a commercial real-time operating system kernel μC/OS-II of two different hardware platforms. The results show that when kernels on two different hardware platforms are verified, the reusability of the verification framework is very high, up to 83.8%. Of course, the abstract model needs to be reconstructed according to different hardware. During verification of operating system kernels based on two kinds of hardware, 10~12 defaults are found respectively. Among them, two hardware-related defaults on the ARM platform are discovered. This method has certain versatility for analysis and verification of the same operating system on different hardware architectures. © Copyright 2020, Institute of Software, the Chinese Academy of Sciences. All rights reserved.