近年来，虚拟化技术飞速发展，各种基于虚拟机技术的应用也越来越多。云计算等基于虚拟化这一新兴技术的安全性也越来越受到人们的关注。Xen作为一种新兴的虚拟化技术，拥有可扩展性好，隔离性强，适应性好等优点，在虚拟化技术中扮演着重要的角色，发展前景非常看好。目前，基于虚拟机Xen上的安全系统的研究越来越多。XSM(XenSecurityModule)是虚拟机Xen的安全模型框架，对系统的安全性具有决定性的作用。因此，对XSM框架的正确性验证具有重要的研究意义和价值。　　 静态分析是在不执行程序的情况下对其进行分析的技术，能够覆盖程序执行的所有路径，在程序部署之前及时发现和修正错误，是一种有效的软件漏洞检测技术。使用静态分析的方法来检查安全框架的正确性是一种常用的技术。　　 目前，对类似的强制访问框架的正确性验证研究主要集中于对钩子函数放置的验证。现有检测方法通常路径覆盖不够完整，或者有较高的误报率。本文对XSM框架的正确性验证问题进行了分析，提出了一种过程间流敏感，过程内路径敏感的，适用于XSM框架的静态分析方法。该方法通过扩展静态分析工具Saturn，实现了对XSM框架的钩子函数设置的正确性和完备性的验证。经实验验证，该方法具有完全的路径覆盖性，并且具有较高的精确度。