操作系统形式化设计与安全需求的一致性验证研究  

Research on Consistency Verification of Formal Design and Security Requirements for Operating System

作　　者：钱振江[1,2,3] 黄皓[1] 宋方敏[1] 

机构地区：[1]南京大学计算机科学与技术系,南京210046 [2]常熟理工学院计算机科学与工程学院,江苏常熟215500 [3]伦敦大学国王学院

出　　处：《计算机学报》2014年第5期1082-1099,共18页Chinese Journal of Computers

基　　金：国家自然科学基金创新研究群体基金(60721002);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001);CSLG科研项目(QT1312)资助~~

摘　　要：采用数学形式化方法对操作系统进行设计和验证可以保证系统的高度安全性.目前已有的操作系统形式化研究工作主要是验证系统的实现在代码级的程序正确性.提出一种操作系统形式化设计和验证的方法,采用操作系统对象语义模型(OSOSM)对系统的设计进行形式化建模,使用带有时序逻辑的高阶逻辑对操作系统的安全需求进行分析和定义.对象语义模型作为系统设计和形式化验证的联系.以实现和验证过的可信微内核操作系统VTOS为实例,阐述形式化设计和安全需求分析,并使用定理证明器Isabelle/HOL①对系统的设计和安全需求的一致性进行验证,表明VTOS达到预期的安全性.The mathematical formal methods for operating system design and verification achievehigh assurance of system security.The existing formalization research works in the scope ofoperating system mainly focus on showing that an implementation complies with the program correctness in the code-level verification.In this paper,we propose a method for formal designand verification.We adopt the operating system object semantics model （OSOSM）for formal modeling of the system design,and analyze and define the security requirements using higher-order logic （HOL）with temporal logic （TL）.We view OSOS Mas the link between systemdesign and formal verification,and take the self-implemented and verified trusted operating system （VTOS）as an example to illustrate formal design and analysis of security requirements.Meanwhile,we use the theorem prover Isabelle/HOL to verify the consistency between system design and security requirements,and show that VTOS achieves the desired security.

关 键 词：操作系统 形式化设计 安全需求 一致性验证 定理证明 信息安全 网络安全 

分 类 号：TP316[自动化与计算机技术—计算机软件与理论]