操作系统安全验证形式化分析框架

摘要

结合当前形式化验证方法的特点和操作系统安全模型情况,本文提出了这些方法在操作系统安全分析中的应用.结合传统定理证明方法的优势,将模型检验方法纳入形式化安全分析体系当中,并分别提出了在安全分析中的应用情况.将用定理证明用于从模型到规则的分析,模型检验从实现中抽取模型,用于从实现到规则的分析.