实用模型的自动化形式验证

• 作者: 刘宏 徐亮
• 来源期刊: 湖南大学学报（自然科学版）
• 关键词: Biba模型 形式化方法 定理证明 自动化形式验证 安全策略
• 年，卷（期）: 2013,（9）
• 所属期刊栏目: 计算机科学与工程
• 页码范围: 91-97
• 页数: 7页
• 分类号: TP301.2
• 语种: 中文

摘要

通过给传统的Biba模型增加相应的敏感级函数,完善其主客体完整性标签,并对其安全操作规则进行相应的改进,使其适应实际的应用需求.采用完全形式化的方法对改进后模型中的各元素、模型必须满足的不变式以及模型迁移规则进行描述,并在此基础上利用定理证明器Isabelle完成对该模型的自动化形式验证,从而实现高等级安全操作系统研发过程中对安全策略模型的形式化需求.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘宏	湖南师范大学数学与计算机科学学院	61	193	8.0	10.0
3	徐亮	湖南师范大学数学与计算机科学学院	9	50	3.0	7.0