引言
云计算是近年来IT产业的热门词汇，在谷歌的定义中，云计算是以公开的标准和服务为基础，以互联网为中心提供安全、快速、便捷的数据存储和网络计算服务模式。虚拟化?是对资源(CPU、存储器、网络、应用栈和数据库)的抽象，不同的用户根据需要提出访问请求并获取资源，而无需关心资源的具体位置。虚拟化将传统的数据中心转化为适合云计算的运行节点，为云环境提供统一、易用的资源组织和使用方式 。
然而， 由于云计算的信息系统本质， 云计算具有自身的安全问题，虚拟化即是其中一个重要方面。云计算供应商对虚拟环境的安全构建及验证进行了大量的研究，在验证技术方面，主要的趋势还是使用传统手段如硬件可靠性测试、功能覆盖率测试等，其得到的结果倾向于工程化，未实现理论层面的完全验证能力。形式化方法作为系统建模和指标验证的重要手段，其应用逐渐由硬件领域向信息系统拓展，在用于虚拟机性质验证的方面已取得了一定成果 ，但尚缺乏针对云计算背景下虚拟环境安全需求的验证方法研究。
1 形式化方法与模型检测
形式化方法的基本含义是借助数学的方法来研究计算机与数学科学问题，在系统构建、实现的全过程中，凡是采用严格的数学语言，具有精确的数学语义的方法，都可以称之为形式化方法。经过40多年的发展，形式化方法已经从理论研究逐渐走向成熟和实用化，在航空航天系统、通讯系统和集成电路等领域得到了较为广泛的应用。
由于潜在的系统错误数量总是和组件的数量成正比，云计算这一新兴计算方式包含的组件众多，实现技术如虚拟化等特点极大地增加了复杂性。基于形式化方法中的模型检测在探查设计潜在缺陷方面的能力，使用模型检测对云计算虚拟化环境进行安全性质验证具备可操作性。
2 虚拟化环境建模
虚拟化技术的目的是为应用提供更强的计算能力和更大的灵活性，这项优势较好地契合了云计算的需求和主要理念。但虚拟化技术提升云基础设施使用效率的同时也使传统的安全防护手段失效 ，在实施虚拟化的同时需要对云计算环境整体可靠性进行评估验证。
形式化验证过程一般需要经过配置采集、需求分析、模型输出3个阶段：
1)配置采集。定义虚拟化环境中虚拟应用程序的集合为Apps，虚拟机的集合为Vms，物理主机的集合为Hosts，网络的集合为Networks，令集合Unit为虚拟环境中的元素集合，可以使用一阶逻辑定义以下谓词，如表1所示。虚拟环境的配置采集过程即为集合、谓词的实例化过程，从而确定所有虚拟应用程序及虚拟机的位置关系、网络的连通情况、环境内主机的数量规模等。
2)需求分析。需求分析阶段的目标是得到形式化语言刻画的安全性质语句，一般也用逻辑命题的形式表述，是需要判定的，即系统的安全目标。这类谓词中包含的是虚拟化环境中人们某一方面感兴趣的安全性质，包括功能正确性、可达性、安全性、活性等。
3)模型输出。模型输出将综合配置采集和需求分析两个阶段的结果，按照模型检测器的输入要求进行优化、规范化，以提高后续模型检测工作执行的效率。
3 安全性质检测
安全性质模型检测是虚拟化环境形式化安全验证的核心步骤，其中虚拟应用安全隔离、虚拟机迁移和单点故障容灾是云计算领域关注的焦点问题，云服务运营商通过功能、性能验证对虚拟化环境的元素进行调整以达到最佳的安全性能，降低故障概率，提高用户满意度。
3．1虚拟应用安全隔离
在云计算环境中往往部署着多种虚拟应用程序，为了性能、安全起见，应根据应用程序的种类和QoS等级进行划分，如运行数据库服务的虚拟机最好与邮件系统分隔开来，避免相互访问产生安全隐患等。
定义谓词reach(a，b)为两应用程序能够互相访问，则希望验证的性质可表达为：对于Apps的子集AppA、AppB，不希望两集合中的程序能够相互访问， 即命题reach(appa，appb对于任何appa∈Appa、appb∈Appb均不成立。其完整性质如下：
secureIsolation(Appa，Appb):┐∨reach(appa，appb)
3．2 虚拟机迁移
虚拟机迁移是实现虚拟化环境高可用性的关键能力之一，在因物理、负载、系统原因导致的虚拟机功能失效情况下，需要立即将原虚拟机迁移至另一台物理机上运行，保证业务的连续性。在本场景中，考虑到虚拟机与主机的安全等级必须匹配，安全等级为高的虚拟机只能运行在安全等级为高(isHigh)的主机上，而安全等级低(isNonnal)的虚拟机可以运行在两种主机上。
该安全性质可以表述为：successMigrate(vrca，vmb)：reside(vma，host)∧reside(vmb，hostb)∧belong(vma，networka)∧belong(vmb，networkb)∧connect(networka，networkb)∧(isHigh(vma)∧isHigh(vmb))∨isNormal(vma))。
3．3 单点故障与容灾
云计算环境中的节点都存在失效的可能，在这种情况下系统和资源容灾是必须要考虑的因素。对于用户而言，在灾难发生时，系统的任何一个部分都可能产生故障，Failure(unit)谓词的参数是整个Units集合，为保证系统避免单点失效，希望用户在灾难发生前后都能保证getService(app)成立， 即：disasterRecovery(app)：getService(app):getService(app)/failure(u))。其中，条件因子failu(u))表示去除模型中所有与u相关的事实，如果该性质满足，说明云计算虚拟环境具有容灾能力，在灾难发生后不需要人工干预就能够自动保证服务连续性。
3．4 检测方法
在虚拟化环境模型和待验证的安全性质确定后，检测器将算法选项参数初始化，并输入待检测的语句作为未知命题进行演算，穷举模型空间里的谓词和给定事实，寻找能够匹配的规则，将命题进一步分解，直到能够成功求值并返回演算结果，整个计算过程在遍历了整棵演算树后结束，根据获得的中间结果组合成最终返回值，给出“是”、“否” 、“系统异常”的验证结果。
4 实例分析
这里用一个实例分析对虚拟环境进行验证的有效性，使用一个包含29台物理机(划分为6个网段)、共计75个虚拟机和237个虚拟应用程序的环境，设计了3个试验场景，定义如下：
场景一进行虚拟应用程序的安全隔离试验，验证应用程序间的访问连通性。
场景二进行虚拟机迁移试验，指定一台虚拟机为待迁移虚拟机，另一主机为迁移目标，验证能否进行成功迁移。
场景三先后将指定的虚拟机、主机、网络设为失效模式，验证业务连续性的保证情况。
所有试验在一台配置为i5 CPU，内存为4 096 MB的计算机上运行，使用的模型检测器为Visual Prolog，其测试结果如表2所示。表2验证场景测试结果
试验结果表明，形式化方法对于云计算虚拟环境的安全验证是有效的。
5 结语
云计算作为新兴的计算、存储资源使用模式，在提供更高性能、更易于使用的服务的同时，其衍生出来的安全问题，特别是虚拟环境的安全问题制约着云计算的发展和进一步应用。形式化方法作为信息系统的可靠性验证方法，在虚拟化环境验证领域同样能够发挥效能，为云计算虚拟环境提供安全需求的严格验证能力，实现云可靠性、安全性的提升。
