摘要
结合当前形式化验证方法的特点和操作系统安全模型情况,本文提出了这些方法在操作系统安全分析中的应用。结合传统定理证明方法的优势,将模型检验方法纳入形式化安全分析体系当中,并分别提出了在安全分析中的应用情况。将用定理证明用于从模型到规则的分析,模型检验从实现中抽取模型,用于从实现到规则的分析。
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 specifications.
出处
《计算机工程与科学》
CSCD
北大核心
2009年第3期24-26,121,共4页
Computer Engineering & Science
