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