| BLP改进模型的形式化描述及自动化验证 |
| |
| 引用本文： | 徐亮,谭煌.BLP改进模型的形式化描述及自动化验证[J].计算机工程,2013(12):130-135. |
| |
| 作者姓名： | 徐亮 谭煌 |
| |
| 作者单位： | [1]湖南师范大学数学与计算机科学学院,长沙410081 [2]高性能计算与随机信息处理省部共建教育部重点实验室,长沙410081 |
| |
| 基金项目： | 国家自然科学基金资助项目（60903168）;湖南省科技计划基金资助项目（2012FJ6012）;湖南省重点学科建设基金资助项目（湘教发[2011]76号）;湖南省教育厅科学研究基金资助项目（13C527）;长沙市科技计划基金资助项目（KI109020-11） |
| |
| 摘 要： | 在《信息安全技术操作系统安全技术要求》中，提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况，对经典的数据机密性BLP模型进行相应改进，为系统中的主客体引入多级安全标签以及安全迁移规则，使其满足实际系统开发的需求。运用完全形式化的方法对改进模型的状态、不变量、迁移规则等进行描述，使用Isabelle定理证明器证明了迁移规则对模型的不变量保持性，从而实现对模型正确性的自动形式化验证，并保证了模型的可靠性。
|
| 关 键 词： | BLP模型 安全策略 形式化方法 自动化验证 定理证明 安全操作系统 |
| 本文献已被 维普 等数据库收录！ |
