Design, Implementation And Verification Of Interrupt System In VTOS

In many situation, it is required that the computer system should have a high degree of security and reliability. The security of a computer system depends on the operating system which it runs on largely, and the security of an operating system mostly depends on its kernel. Therefore, it is an urgent problem to ensure the security and reliability of the kernel.It is common sense that the bugs of software increase with the amount of its im-plementing code. So the micro-kernel technology which streamlines the kernel is a good method to enhance the security of kernel.Using strict formal techniques for software verification is currently recognized a good method to ensure the security and reliability of software. Many projects, such as Verisoft and SeL4, use formal methods to verify the operating system and they have achieved great results. But almost all the current verification projects only concentrate on the upper software verification, few works verified the interrupt system. Because the interrupt system is at the bottom of a system, and the interrupts occurs uncertainly which leads to the execution flow’s uncertainly. All these reasons make the verifica-tion of interrupt a difficult work.But it is very necessary to ensure the correctness of interrupt system. Because the correctness of interrupt system ensures the correctness of saving and restoring of process context when interrupt occurs, which is one of the basic premises of the correctness of multi-tasking system.After we have done detailed analyses of the Minix3 kernel and the current verifi-cation projects, we firstly design and implement the interrupt and schedule system of our operating system VTOS,which based on the micro-kernel architecture, and then we modeled the interrupt and schedule system of VTOS in the auxiliary theorem prover Isabelle/HOL. We set the pre-conditions,the post-conditions and the theorems of all the functions which may be executed during the interrupt process. Though the theo-rems being proved correctly in Isabelle/HOL, we prove that the process context will not be changed during the interrupt process and the integrity of interrupt system in VTOS, thus we prove the correctness of the interrupt system in VTOS.