| Biba实用模型的自动化形式验证 |
| |
| 引用本文： | 徐 亮,刘 宏.Biba实用模型的自动化形式验证[J].湖南大学学报(自然科学版),2013,40(9):91-97. |
| |
| 作者姓名： | 徐 亮 刘 宏 |
| |
| 作者单位： | 湖南师范大学数学与计算机科学学院;高性能计算与随机信息处理省部共建教育部重点实验室 |
| |
| 基金项目： | 国家自然科学基金资助项目(60903168);湖南省科技计划资助项目(2012FJ6012);湖南省教育厅科学研究项目(13C527);湖南省重点学科建设资助项目(湘教发[2011]76号) |
| |
| 摘 要： | 通过给传统的Biba模型增加相应的敏感级函数,完善其主客体完整性标签,并对其安全操作规则进行相应的改进,使其适应实际的应用需求.采用完全形式化的方法对改进后模型中的各元素、模型必须满足的不变式以及模型迁移规则进行描述,并在此基础上利用定理证明器Isabelle完成对该模型的自动化形式验证,从而实现高等级安全操作系统研发过程中对安全策略模型的形式化需求.
|
| 关 键 词： | Biba模型 形式化方法 定理证明 自动化形式验证 安全策略 |
Automated Formal Verification of Practical Biba Model |
| |
| XU Liang,LIU Hong.Automated Formal Verification of Practical Biba Model[J].Journal of Hunan University(Naturnal Science),2013,40(9):91-97. |
| |
| Authors: | XU Liang LIU Hong |
| |
| Institution: | XU Liang;LIU Hong;College of Mathematics and Computer Science,Hunan Normal Univ;Key Laboratory of High Performance Computing and Stochastic Information Processing (Ministry of Education of China); |
| |
| Abstract: | |
| |
| Keywords: | Biba model formal method theorem proving automated formal verification security policy |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《湖南大学学报(自然科学版)》浏览原始摘要信息 |
| 点击此处可从《湖南大学学报(自然科学版)》下载免费的PDF全文 |
