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

Automated Formal Verification of Practical BLP Model

作　　者：徐亮[1,2] 刘宏[1,2] 

机构地区：[1]湖南师范大学数学与计算机科学学院,湖南长沙410081 [2]高性能计算与随机信息处理省部共建教育部重点实验室,湖南长沙410081

出　　处：《湖南大学学报（自然科学版）》2013年第9期91-97,共7页Journal of Hunan University:Natural Sciences

基　　金：国家自然科学基金资助项目(60903168);湖南省科技计划资助项目(2012FJ6012);湖南省教育厅科学研究项目(13C527);湖南省重点学科建设资助项目(湘教发[2011]76号)

摘　　要：通过给传统的Biba模型增加相应的敏感级函数,完善其主客体完整性标签,并对其安全操作规则进行相应的改进,使其适应实际的应用需求.采用完全形式化的方法对改进后模型中的各元素、模型必须满足的不变式以及模型迁移规则进行描述,并在此基础上利用定理证明器Isabelle完成对该模型的自动化形式验证,从而实现高等级安全操作系统研发过程中对安全策略模型的形式化需求.In order to adapt the actual application requirements, sensitive-level functions, perfect integ- rity labels of subjects and objects were added in the traditional Biba model. Also its safety operation rules were improved. The elements, the invariants and the transition rules of the improved model were described in completely formal methods. By doing this, the model was automatically formal verified by using theo- rem-prover Isabelle. The formal description and formal verification satisfied the formal methods require- ment in the development of high-level secure operating systems.

关 键 词：BIBA模型 形式化方法 定理证明 自动化形式验证 安全策略 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]