微内核完整性保障研究与应用

Integrity Assurance of Micro-kernel Operating System and its Application

为了避免安全操作系统中访问控制机制被篡改、绕过,提出利用微内核多服务器结构为安全核完整性提供保障。微内核提供的进程隔离和消息传递机制使得各个服务进程独立运行,通过受控的消息机制进行交互,有效保证了各个模块的完整性。微内核结构的简单性和模块化为形式化验证奠定了基础。原型系统Nutos利用Flask安全体系结构为用户提供灵活多策略的强制访问控制,由微内核多服务器结构为Flask中的安全服务器和引用监控器提供完整性保障,确保安全策略的正确实施。

To avoid the security mechanism applied in operating systems being bypassed or tampered, this paper proposed the use of micro-kernel, multiserver architecture to assure the integrity of security kernel. Process isolation and message passing provided by the micro-kernel make the processes above isolated and protect the integrity of them effectively. Simplicity and modularity, the most obvious advantages of micro-kernel, laid an excellent base for the future formal verification. The prototype operating system, Nutos, was presented as an example on how to use these mechanisms to enforce security. It combined the multiserver architecture and the Flask security infrastructure to provide for flexibility in security policies and integrity assurance for security sever and reference monitor.