Research on Microkernel Integrity Semantics Model and Formal Verification  

作　　者：QIAN Zhenjiang LIU Wei HUANG Hao 

机构地区：[1]State Key Laboratory for Novel Software Technology, Nanjing University [2]Department of Computer Science and Technology, Nanjing University

出　　处：《Chinese Journal of Electronics》2014年第1期43-48,共6页电子学报（英文版）

基　　金：supported by the National High Technology Research and Development Program of China(863 Program)(No.2011AA01A202);the National Natural Science Foundation of China(No.61021062);the"Six Talents Peak"High-Level Personnel Project of Jiangsu Province(No.2011-DZXX-035);University Natural Science Research Program of Jiangsu Province(No.12KJB520001)

摘　　要：Microkernel integrity is an important aspect of security for the whole microkernel system. Many of the research works on microkernel integrity focus on analysis and safeguards against the existing kernel attacks, and security enhancements for the vulnerabilities of system design and implementation aspects. The formal methods for operating system design and verification ensure the system's high level of security. The existing formalization work and research for operating system mainly focus on the code-level verification of program correctness. In this paper, we propose a formal abstraction model of microkernel in order to accurately describe the semantics of every kernel behavior, and achieve the description of the whole kernel. Based on the model we illustrate the microkernel integrity criterions and elaborate on the integrity mechanism. Meanwhile, we formally verify the completeness and consistency between the mechanism and the definition of the microkernel integrity. We use the self-implemented operating system VTOS(Verified trusted operating system) as an example to illustrate the design method for the microkernel integrity.Microkernel integrity is an important as- pect of security for the whole microkernel system. Many of the research works on microkernel integrity focus on anal- ysis and safeguards against the existing kernel attacks, and security enhancements for the vulnerabilities of system de- sign and implementation aspects. The formal methods for operating system design and verification ensure the sys- tem＇s high level of security. The existing formalization work and research for operating system mainly focus on the code-level verification of program correctness. In this paper, we propose a formal abstraction model of microker- nel in order to accurately describe the semantics of every kernel behavior, and achieve the description of the whole kernel. Based on the model we illustrate the microkernel integrity criterions and elaborate on the integrity mech- anism. Meanwhile, we formally verify the completeness and consistency between the mechanism and the definition of the microkernel integrity. We use the self-implemented operating system VTOS （Verified trusted operating sys- tem） as an example to illustrate the design method for the microkernel integrity.

关 键 词：Microkernel integrity Integrity mecha-nism Integrity semantics model Formal verification. 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]