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

作     者：钱振江 黄皓 宋方敏 QIAN Zhen-Jiang;HUANG Hao;SONG Fang-Min

作者机构：南京大学计算机科学与技术系南京210046 常熟理工学院计算机科学与工程学院江苏常熟215500 伦敦大学国王学院 

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

出 版 物：《计算机学报》 (Chinese Journal of Computers)

年 卷 期：2014年第37卷第5期

页      码：1082-1099页

摘      要：采用数学形式化方法对操作系统进行设计和验证可以保证系统的高度安全性.目前已有的操作系统形式化研究工作主要是验证系统的实现在代码级的程序正确性.提出一种操作系统形式化设计和验证的方法,采用操作系统对象语义模型(OSOSM)对系统的设计进行形式化建模,使用带有时序逻辑的高阶逻辑对操作系统的安全需求进行分析和定义.对象语义模型作为系统设计和形式化验证的联系.以实现和验证过的可信微内核操作系统VTOS为实例,阐述形式化设计和安全需求分析,并使用定理证明器Isabelle/HOL①对系统的设计和安全需求的一致性进行验证,表明VTOS达到预期的安全性.

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

学科分类：0810[工学-土木类] 0808[工学-自动化类] 0839[0839] 08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.3724/SP.J.1016.2014.01082

馆 藏 号：203109472...