BLP改进模型的形式化描述及自动化验证

• 作者: 徐亮 谭煌
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: BLP模型 安全策略 形式化方法 自动化验证 定理证明 安全操作系统
• 年，卷（期）: 2013,（12）
• 所属期刊栏目: 安全技术
• 页码范围: 130-135
• 页数: 6页
• 分类号: TP301.2
• 字数: 5555字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2013.12.028

摘要

在《雷息安全技术操作系统安全技术要求》中，提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况，对经典的数据机密性BLP模型进行陒应改进，为系统中的主客体引入多级安全标签以及安全迁移规则，使其满足实际系统开发的需求。运用完全形式化的方法对改进模型的状态、不变量、迁移规则等进行描述，使用Isabelle定理证明器证明了迁移规则对模型的不变量保持性，从而实现对模型正确性的自动形式化验证，并保证了模型的可靠性。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	谭煌	湖南师范大学数学与计算机科学学院	7	24	2.0	4.0
3	徐亮	湖南师范大学数学与计算机科学学院	9	50	3.0	7.0