关键词：xsm 语义模型 形式化验证 安全性分析 

摘要：Xen作为一种开源流行的虚拟化工具,使用越来越频繁。作为Xen的安全框架XSM（Xen Security Module）也受到广泛的关注。许多研究者通过形式化的方式对现有的操作系统进行正确性的验证,目前已有的形式化研究主要是验证系统实现的代码正确性。从系统功能角度提出了一种以主体行为为操作系统语义模型对系统进行形式化建模,并采用CTL时序逻辑对XSM安全需求进行分析。语义模型作为系统设计合理性和形式化验证的联系,对XSM进行形式化验证,并使用Isabelle/HOL验证功能和安全需求的一致性,以说明XSM是否符合安全需求。

计算机应用与软件杂志要求:

{1}文章关键要素，需有英文摘要。

{2}文章主题明确，数据可靠，书写准确，图表清晰，文字简练，内容齐全完整。来稿应含以下部分：中英文题名、中英文摘要、中英文关键词、中图分类号（本编辑部亦可代查）、正文以及必要的图表、参考文献。

{3}文稿要一稿一投，严禁各类侵权行为。

{4}前言应充分说明研究工作的背景、意义、本文拟解决的问题、采用的方法和手段,引出重要文献,全面评述相关研究工作,突出本工作的重要性和创新性,不要忽视国内同行的工作。

{5}稿件注释一律采用 “脚注”。注释规则请参下附《注释规范》，请投稿者严格遵循。

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社