形式化方法在云计算中的应用现状

2019-03-18 09:48

广州大学学报（自然科学版） 2019年4期

(1.广州大学计算机科学与网络工程学院，广东广州 510006; 2.北京大学信息科学技术学院软件研究所/高可信软件技术教育部重点实验室，北京 100871)

随着计算机和互联网技术的进步，互联网企业需要存储和处理的数据量大大增加，互联网用户也需要便捷灵活的互联网服务.在这样的背景下，云计算技术应运而生[1]，并很快得到了飞速的发展和广泛的应用.云计算是一种新的计算模型，它将虚拟化计算、分布式技术、并行处理和网格计算等进行了整合和扩充.美国国家标准与技术研究院在其对云计算的定义中给出了云计算的五个关键特征[2]，即按需服务、快速灵活、网络连接、资源共享和可度量服务.

通常来说，云计算平台主要包括两个方面：硬件设施和软件架构.前者主要包括网络通讯设备、网络连接、数据和存储中心、服务器和计算资源.后者包括操作系统、数据库、软件开发平台、软件应用和中间件.一个运行在云计算平台上的应用由多个运行在不同分布式虚拟机器上的软件组建构成.因而，云计算平台需要许多任务管理程序和专门的协议来调度和监控这些分布式程序，以保证它们之间的一致性.

云计算系统应当向用户保证程序的鲁棒性、容错率、自动执行以及提供强有力的计算设备.这要求云计算系统必须能够满足一系列相关的性质.例如，云计算系统中数据存储的一致性，即云计算系统中，一份数据及其多个副本同时存在，并且被存储在不同的数据中心，该性质是云计算系统所独有的.同时，对于服务需求不准确的解读，会导致云服务无法满足用户的需求.此外，随着云计算技术诞生的大数据采集和分析也迫切需要新的验证方法.因此，使用形式化方法和工具验证云计算系统是非常必要的.

云计算系统为了在满足更多需求的同时减少管理开销，大量使用了虚拟化技术.这导致云计算系统非常复杂，以致难以管理和测试.这要求必须进行全面的测试和验证.然而我们已经发现在云计算框架如Hadoop中使用调度算法可能由于无法预知的云环境改变导致调度失败[3]，传统的模拟方法也无法保证对复杂系统的完整覆盖.除了上述方法之外我们使用形式化方法来提升云计算系统的质量，保证云计算系统的可靠性.

形式化方法是用严格的数学语言对计算机软硬件进行描述、开发和验证的技术.由于其验证方法是严格的，验证结果是可靠的，多被用于安全关键系统的验证中.形式化方法主要包括：定理证明、模型检查和等效性检查.等效性检查通常仅被应用于非常狭窄的研究领域，定理证明和模型检查已经被应用于云计算系统的形式化验证中.所有的形式化方法都是基于形式化语法和语义的，有一些验证方法提出形式化的语法，同时允许非形式化的语义，称之为半形式化方法.

在本文中，主要调研了形式化方法在云计算中应用的现状.依据使用形式化方法验证云计算系统中的性质不同，将相关的工作分为几个类别.

1 资源管理

在传统计算机系统架构中，计算机通过系统进行资源(内存、CPU、I/O设备等)的分配.云计算系统通过引入虚拟技术改变了资源分配的方式.在云计算系统中，通过引入资源池的概念，将物理存储、虚拟内存、CPU等作为数据存储、数据处理和带宽服务提供给用户，并能够通过管理程序按照用户的需求调整资源分配状况.云计算系统应当保证资源管理的正确性，这密切关系到云计算系统提供给用户的服务质量.

文献[4]使用Frama-C软件验证工具和Coq定理证明器[5]建模和验证了云管理程序Anaxagoros的虚拟内存系统.该管理程序是为资源隔离和保护设计的.文献[6-7]提供了资源视图的形式化定义，以保证云资源分配的正确性和最优性.作者基于Event-B提出了一种形式化体系来详细说明商业程序模型中的云资源分配策略，它可以在设计系统时形式化地验证云资源分配的一致性，并根据用户需求和资源性质分析和验证程序模型的正确性.文献[8]提出了保证时间感知的云资源分配一致性的方法.作者给出了云资源和商业进程执行过程中的时间约束的形式化描述，并将这些规范用时间自动机建模，以验证时间感知的云资源分配一致性和分析检查云资源分配对于商业进程时间约束的正确性.文献[9]以节能为目的，提出了云计算管理的架构原则以及考虑服务质量的资源分配策略和调度算法.经验证该方法能够有效地减少能源消耗.文献[10]用λ演算分析和验证了云计算环境下网络服务应用的资源使用，并且用Labeled Transition System Analyser[11]验证了若干资源保护策略的合理性.文献[12]使用Petri网给出了基于代理的云计算系统的形式化模型，该模型能够按照代理的需求提供更好的资源利用.文献[13]用Event-B方法[14]为自由开源软件提出了一种云资源分配模型.该模型可以用来在设计程序时验证资源分配的一致性，并根据用户需求和资源满足的性质分析和检查程序的正确性.该模型的正确性和一致性使用ProB模型检查工具来验证.

除了资源分配以外，云计算系统中的任务调度问题也非常重要.好的任务调度算法能够保证云计算系统运行的稳定，同时还能满足用户需求甚至达到节能的目的.文献[15]提出了一种改良的强大的遗传算法来解决云系统中的任务调度问题，并使用模型检查方法验证了该算法的正确性.文中基于模型检查技术提出了一种行为建模方法，并且把期望验证的算法的有关性质提取出来表示为线性时序逻辑的形式.为了获得最好的验证效果，文中使用了标号迁移系统.作者使用NuSMV和PAT模型检查工具验证了算法的行为模型，并根据验证结果分析了算法的可达性、公平性和无死锁性.文献[16]提出了一种新的任务调度策略，能够兼顾服务质量和能量消耗.作者首先从云任务调度的视角建模了虚拟机能量，然后提出了一种遗传算法来兼顾不同的能源需求和表现需求，并设计了两种适应度函数，以根据能源消耗和任务表现的不同来挑选后代.文献[17]通过分析影响虚拟机的花销和利用率的因素提出了一种基于博弈论的任务调度方案，同时提出了一种形式描述语言建模云应用中的不同组件.作者提出了一种逆向归纳博弈算法来保证云应用在提升虚拟机利用率的同时动态满足用户的需求.Petri网的操作语义和相关理论被用来验证该方法的正确性.

此外，还有部分工作研究了云计算系统中操作和配置的正确性.文献[18]用SPIN模型检查工具[19]建模了云计算环境下的Event-Condition-Action规则，可以将云计算系统中的种种约束在该工具中建模.同时，系统正确性可以用这些约束的属性在线性时序逻辑中描述出来.该工具通过扩展SPIN的PROMELA语言实现.文献[20]中用NuSMV模型检查工具验证了云计算系统中的一些操作缺陷性质.作者首先建立了云系统及其性质的模型，然后将该模型翻译为NuSMV语法，最后在一个三层使用Amazon EC2负载均衡的云系统中用模型检查验证了一系列性质.文献[21]提出了两种技术来减少云计算系统错误配置的风险，一种是把配置修改过程自动合成以减少错误修改，另一种是识别系统配置中的缺陷.作者用模型检查工具实现了这些技术，并通过样例分析评估了它们的可用性.

2 安全性和加密

在云计算大规模普及的互联网背景下，用户将大量数据存储在公共网络中，面临的其中一个重大威胁就是安全问题.根据云安全联盟公布的《The Treacherous 12——Cloud Computing Top Threats in 2016》[22]，数据泄露、凭证被盗等安全问题已经成为云计算服务面临的核心威胁.近年来，科研工作者们开展了许多与云计算安全有关的工作，主要包括验证安全性协议和提出新的加密方式等等.

许多工作通过验证安全规则来保证云计算系统的安全性.文献[23]中定义了云演算(Cloud calculus)用来描述云计算系统的拓扑结构和防火墙安全规则.文献[24]中提出了一套系统的过程来验证虚拟机迁移后防火墙策略的安全合法性.云系统中的分布式防火墙配置使用云演算描述的网络拓扑来定义；防火墙配置表达为命题约束，并基于约束满足问题建立了一个验证模型.此外，文章还提出了一个Amazon EC2中的例子说明该方法的适用性和有效性.文献[25]中提出了一套基于云的安全的信息共享系统，用资源描述框架定义其各种性质如可靠性、透明度、一致性、完全性等等.作者准备用ACL2[26]来生成系统满足的性质的机器可验证的证明过程，但作者没有提供这些性质如何被建模和验证的细节.文献[27]提出了一种云计算的安全存储服务，它结合了不同的安全机制以加强现有方法对威胁的检测.该方法中使用了审查和监控机制来发现威胁和证明其对安全性质的破坏性，并使用有色Petri网对效果进行了评估.

除了在云计算系统中引入安全规则外，还可以通过加密的方式来保证私有数据的安全性和隐私性.文献[28]中用WebSpi网络安全库研究了一系列商业或学术的加密网络应用，并用ProVerif模型检查工具[29]验证了加密存储协议应对攻击的安全性.文献[30]形式化地分析了一种基于ABS(Attribute-based signature)和ABE(Attribute-based encryption)的加密协议，对该协议进行了建模，并使用ProVerif自动工具验证了协议的安全性质.文献[31]对RDIC(Remote data integrity checking)协议进行了改进，并证明了改进后的协议能够满足旧的协议不能确保的安全性质.文献[32]对一种可能遭受攻击的RDPC(Remote data possession checking)协议进行了改进，提供了改进后协议的安全性的形式化证明，并且通过实现该协议给出了其表现的报告.文献[33]提出了一种名为KSF-OABE的加密方法，并证明了该方法在选择明文攻击下是安全的.文献[34]提出了一种新的云存储加密方法，该方法能够保证用户的隐私不会被泄露.

3 故障恢复机制

在云计算系统中，通常采用一些故障恢复机制来增加系统的容错.这是由于在云计算系统这样的分布式系统中往往包含成百上千个节点，节点故障时有发生.同时为了应对软件故障和人为错误操作，也有必要采用故障恢复机制避免影响整个系统运转.文献[35]中为云计算提出了一种基于Byzantine故障检测技术的模型.文中使用了云计算故障网来建模云计算中的不同组件，如服务资源、云模块等，并分析了模型的一些基本性质.在此模型的基础上，作者提出了能够动态检测执行时云应用中故障的故障检测策略，并使用Petri网的操作语义和相关性质证明了策略的有效性和正确性.文献[36]中提出了一种云存储系统可检索性方案的动态证明，这种方案支持公共审核和数据损坏时有效恢复通信.

多副本机制是云计算系统故障恢复机制中非常重要的一个部分，它能够有效地提高云计算系统的可伸缩性和可靠性，同时在一定程度上改善用户访问时间.文献[37]中用基于Event-B的方法建模了多副本数据存储，数据存储中使用了大量复制和预写日志的方法.作者在同步、半同步、异步架构下实现了该模型,并在可能出错的场景下验证了数据完整性.文献[38]用Petri 网通过三种方法：多线程、分布式和基于云的方法建模同一个系统，比较了面对状态空间爆炸问题时三者的表现.文献[39]中用CSP建模了Hadoop并行框架，并用PAT模型检查工具[40]验证了数据局部性及无死锁等性质.

4 其他相关研究

虚拟化技术是云计算系统中所使用的关键技术，通过该技术，云计算系统能够将硬件存储资源抽象为一个“资源池”，对资源进行统一管理，从整体上提高资源利用率，并节约管理成本.文献[41]中提出了vTRUST建模框架用来形式化地描述虚拟系统，并通过自动化验证现实世界中云计算实现识别缺陷，以说明该框架的效果.文献[42]中用High-Level Petri Nets建模和分析了三种开源的基于虚拟机器的云管理平台的结构的和操作的性质.作者用Satisfiability Modulo Theories Library[43]和Z3[44]建模了100个虚拟机器来验证模型的正确性和可行性，同时验证增加虚拟机器的数量并不影响模型的运转，说明该模型还具有很强的可扩展性和灵活性.在文献[45]中作者构造了虚拟数据中心并发动态迁移的性能模型，在该模型下同时进行多个动态迁移，收集表现数据.然后用PRISM概率模型检查工具[46]构造表现模型，验证了若干云计算系统中的概率性质.

通常来说，云计算提供的服务分为三个层次，即IaaS、PaaS和SaaS.这三个层次所面对的用户群体不同.SaaS是软件的开发、管理、部署全部由第三方完成，用户拿来即用，完全不需要关心技术问题.PaaS提供的是软件部署平台，抽象掉了硬件和底层细节，开发者只需要关注业务逻辑，不需要关心底层细节.IaaS则提供最底层的服务，用户需要自己控制底层，实现基础设施的使用逻辑.文献[47]为SaaS云传送模型定义了服务层协议参数，并提出一种检测框架对协议进行符合性检查.文献[48]提出了VaaS的概念，即把在云环境下进行验证作为服务提供给用户.文章给出了VaaS的体系结构和用VaaS验证模型的方法，并以偶图为例进行了说明.

除了上述研究工作之外，还有部分工作关注了云计算中工作流、检索以及事务的相关性质.文献[49]使用Z notation[50]形式化了联合(federated)云工作流.文章对观察到的感兴趣的性质进行了抽象描述，用Z/EVES定理证明器进行了符号化演算，同时使用数学规则约束安全性、开销、依赖关系等来定义这些性质，最后给出了一个Haskell实现，输入用户工作流和需要的性质，生成满足条件的工作流部署配置.文献[51]中提出了用Rule Markup Language表达检索和聚合规则的形式化方法.在Distributed Data Aggregation Service处理检索请求时，该方法能够将检索规则映射到结构化数据的XML格式，以从BlobSeer数据存储系统中获取非结构化条目.在文献[52]中，Read Atomic Multi-Partition事务作为一种高效轻量多分区的事务被提出，它能够保证读原子性.作者用rewriting logic给出了RAMP事务的形式化表达，并用Maude工具进行了关键形式的模型检查验证.在文献[53]中又进而提出了rewriting logic和Maude工具作为配套的框架来详细描述和分析云存储系统的正确性和表现.

5 总结