| 操作系统安全验证形式化分析框架 |
| |
| 引用本文： | 尹中旭,吴灏. 操作系统安全验证形式化分析框架[J]. 计算机工程与科学, 2009, 31(3) |
| |
| 作者姓名： | 尹中旭 吴灏 |
| |
| 作者单位： | 解放军信息工程大学信息工程学院,河南,郑州,450002;解放军信息工程大学信息工程学院,河南,郑州,450002 |
| |
| 摘 要： | 结合当前形式化验证方法的特点和操作系统安全模型情况,本文提出了这些方法在操作系统安全分析中的应用。结合传统定理证明方法的优势,将模型检验方法纳入形式化安全分析体系当中,并分别提出了在安全分析中的应用情况。将用定理证明用于从模型到规则的分析,模型检验从实现中抽取模型,用于从实现到规则的分析。
|
| 关 键 词： | 模型检测 定理证明 可信计算基 访问控制模型 |
A Formal Analysis Framework for Operating System Security Verification |
| |
| YIN Zhong-xu,WU Hao. A Formal Analysis Framework for Operating System Security Verification[J]. Computer Engineering & Science, 2009, 31(3) |
| |
| Authors: | YIN Zhong-xu WU Hao |
| |
| Affiliation: | School of Information Engineering;PLA Information Engineering University;Zhengzhou 450002;China |
| |
| Abstract: | By studying the characteristics of the formal verification methods and the security model of operating systems,various conditions for the application of these methods to OS security analysis are introduced.We introduce a model checking method to OS security evaluation with the benefit of the traditional theorem proving methods.In the new method,we apply theorem proving to the analysis from the security model to specifications,and the model checking method to the analysis from implementation to specification... |
| |
| Keywords: | model checking therem proving TCB access control model |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
