高等级安全操作系统可信保证技术研究
高等级安全操作系统的可信性保证技术是极其重要且极具挑战性的问题.在“面向访问验证保护级安全操作系统”课题的研究中,对高安全可信操作系统进行预研,我们完成了如下工作:设计并实现了一个基于B语言的安全操作系统形式化原型-HAK;应用基于B语言的安全不变式模型检测技术,验证了中国墙策略(CW)和多级安全策略(MLS)在HAK实现级的安全性质;应用基于前置互模拟的对应性分析方法,分析了安全策略模型与形式化顶层规约(FTLS)之间的对应性;提出了基于符号执行的断言分析技术,验证了HAK核心系统调用对安全策略不变式的保持性.本课题解决方案支持系统的快速原型开发方法,研究成果将有助于提高国产操作系统的可信性.
计算机软件 安全操作系统 可信保证技术
李斌 马越 刘剑
中国科学院软件研究所,北京100190
国内会议
上海
中文
400-413
2012-12-06（万方平台首次上网日期，不代表论文的发表时间）