XSM语义模型及安全需求形式化验证

XSM SEMANTIC MODEL AND FORMAL VERIFICATION OF SECURITY REQUIREMENTS

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

As a popular open-source virtualization tools, Xen is used more and more frequently. Xsm （Xen Security Module） , as the security framework of the Xen, has also been widespread concern. There are a lot of research to verify the system operations correctness by formal method. The existing formalization research is mainly concerned with the code correctness of the system implementation. Thus, the system is modeled formally which subject behavior is taken as operating system semantic model in the perspective of system function, and the security requirements of XMS is analyzed by adopting the CLT sequential logic. As the connection of the rationality of system design and formal verification, the semantic model is responsible for the formal verification of the XSM, and the Isabelle/HOL is utilized to verify the consistency between functions and security requirements so as to demonstrate whether the XSM meets the security re-quirements.