(1.廣州大學 計算機科學與網(wǎng)絡工程學院， 廣東 廣州 510006; 2.北京大學 信息科學技術學院軟件研究所/高可信軟件技術教育部重點實驗室， 北京 100871)

隨著計算機和互聯(lián)網(wǎng)技術的進步，互聯(lián)網(wǎng)企業(yè)需要存儲和處理的數(shù)據(jù)量大大增加，互聯(lián)網(wǎng)用戶也需要便捷靈活的互聯(lián)網(wǎng)服務.在這樣的背景下，云計算技術應運而生[1]，并很快得到了飛速的發(fā)展和廣泛的應用.云計算是一種新的計算模型，它將虛擬化計算、分布式技術、并行處理和網(wǎng)格計算等進行了整合和擴充.美國國家標準與技術研究院在其對云計算的定義中給出了云計算的五個關鍵特征[2]，即按需服務、快速靈活、網(wǎng)絡連接、資源共享和可度量服務.

通常來說，云計算平臺主要包括兩個方面：硬件設施和軟件架構.前者主要包括網(wǎng)絡通訊設備、網(wǎng)絡連接、數(shù)據(jù)和存儲中心、服務器和計算資源.后者包括操作系統(tǒng)、數(shù)據(jù)庫、軟件開發(fā)平臺、軟件應用和中間件.一個運行在云計算平臺上的應用由多個運行在不同分布式虛擬機器上的軟件組建構成.因而，云計算平臺需要許多任務管理程序和專門的協(xié)議來調(diào)度和監(jiān)控這些分布式程序，以保證它們之間的一致性.

云計算系統(tǒng)應當向用戶保證程序的魯棒性、容錯率、自動執(zhí)行以及提供強有力的計算設備.這要求云計算系統(tǒng)必須能夠滿足一系列相關的性質(zhì).例如，云計算系統(tǒng)中數(shù)據(jù)存儲的一致性，即云計算系統(tǒng)中，一份數(shù)據(jù)及其多個副本同時存在，并且被存儲在不同的數(shù)據(jù)中心，該性質(zhì)是云計算系統(tǒng)所獨有的.同時，對于服務需求不準確的解讀，會導致云服務無法滿足用戶的需求.此外，隨著云計算技術誕生的大數(shù)據(jù)采集和分析也迫切需要新的驗證方法.因此，使用形式化方法和工具驗證云計算系統(tǒng)是非常必要的.

云計算系統(tǒng)為了在滿足更多需求的同時減少管理開銷，大量使用了虛擬化技術.這導致云計算系統(tǒng)非常復雜，以致難以管理和測試.這要求必須進行全面的測試和驗證.然而我們已經(jīng)發(fā)現(xiàn)在云計算框架如Hadoop中使用調(diào)度算法可能由于無法預知的云環(huán)境改變導致調(diào)度失敗[3]，傳統(tǒng)的模擬方法也無法保證對復雜系統(tǒng)的完整覆蓋.除了上述方法之外我們使用形式化方法來提升云計算系統(tǒng)的質(zhì)量，保證云計算系統(tǒng)的可靠性.

形式化方法是用嚴格的數(shù)學語言對計算機軟硬件進行描述、開發(fā)和驗證的技術.由于其驗證方法是嚴格的，驗證結果是可靠的，多被用于安全關鍵系統(tǒng)的驗證中.形式化方法主要包括：定理證明、模型檢查和等效性檢查.等效性檢查通常僅被應用于非常狹窄的研究領域，定理證明和模型檢查已經(jīng)被應用于云計算系統(tǒng)的形式化驗證中.所有的形式化方法都是基于形式化語法和語義的，有一些驗證方法提出形式化的語法，同時允許非形式化的語義，稱之為半形式化方法.

在本文中，主要調(diào)研了形式化方法在云計算中應用的現(xiàn)狀.依據(jù)使用形式化方法驗證云計算系統(tǒng)中的性質(zhì)不同，將相關的工作分為幾個類別.

1 資源管理

在傳統(tǒng)計算機系統(tǒng)架構中，計算機通過系統(tǒng)進行資源(內(nèi)存、CPU、I/O設備等)的分配.云計算系統(tǒng)通過引入虛擬技術改變了資源分配的方式.在云計算系統(tǒng)中，通過引入資源池的概念，將物理存儲、虛擬內(nèi)存、CPU等作為數(shù)據(jù)存儲、數(shù)據(jù)處理和帶寬服務提供給用戶，并能夠通過管理程序按照用戶的需求調(diào)整資源分配狀況.云計算系統(tǒng)應當保證資源管理的正確性，這密切關系到云計算系統(tǒng)提供給用戶的服務質(zhì)量.

文獻[4]使用Frama-C軟件驗證工具和Coq定理證明器[5]建模和驗證了云管理程序Anaxagoros的虛擬內(nèi)存系統(tǒng).該管理程序是為資源隔離和保護設計的.文獻[6-7]提供了資源視圖的形式化定義，以保證云資源分配的正確性和最優(yōu)性.作者基于Event-B提出了一種形式化體系來詳細說明商業(yè)程序模型中的云資源分配策略，它可以在設計系統(tǒng)時形式化地驗證云資源分配的一致性，并根據(jù)用戶需求和資源性質(zhì)分析和驗證程序模型的正確性.文獻[8]提出了保證時間感知的云資源分配一致性的方法.作者給出了云資源和商業(yè)進程執(zhí)行過程中的時間約束的形式化描述，并將這些規(guī)范用時間自動機建模，以驗證時間感知的云資源分配一致性和分析檢查云資源分配對于商業(yè)進程時間約束的正確性.文獻[9]以節(jié)能為目的，提出了云計算管理的架構原則以及考慮服務質(zhì)量的資源分配策略和調(diào)度算法.經(jīng)驗證該方法能夠有效地減少能源消耗.文獻[10]用λ演算分析和驗證了云計算環(huán)境下網(wǎng)絡服務應用的資源使用，并且用Labeled Transition System Analyser[11]驗證了若干資源保護策略的合理性.文獻[12]使用Petri網(wǎng)給出了基于代理的云計算系統(tǒng)的形式化模型，該模型能夠按照代理的需求提供更好的資源利用.文獻[13]用Event-B方法[14]為自由開源軟件提出了一種云資源分配模型.該模型可以用來在設計程序時驗證資源分配的一致性，并根據(jù)用戶需求和資源滿足的性質(zhì)分析和檢查程序的正確性.該模型的正確性和一致性使用ProB模型檢查工具來驗證.

除了資源分配以外，云計算系統(tǒng)中的任務調(diào)度問題也非常重要.好的任務調(diào)度算法能夠保證云計算系統(tǒng)運行的穩(wěn)定，同時還能滿足用戶需求甚至達到節(jié)能的目的.文獻[15]提出了一種改良的強大的遺傳算法來解決云系統(tǒng)中的任務調(diào)度問題，并使用模型檢查方法驗證了該算法的正確性.文中基于模型檢查技術提出了一種行為建模方法，并且把期望驗證的算法的有關性質(zhì)提取出來表示為線性時序邏輯的形式.為了獲得最好的驗證效果，文中使用了標號遷移系統(tǒng).作者使用NuSMV和PAT模型檢查工具驗證了算法的行為模型，并根據(jù)驗證結果分析了算法的可達性、公平性和無死鎖性.文獻[16]提出了一種新的任務調(diào)度策略，能夠兼顧服務質(zhì)量和能量消耗.作者首先從云任務調(diào)度的視角建模了虛擬機能量，然后提出了一種遺傳算法來兼顧不同的能源需求和表現(xiàn)需求，并設計了兩種適應度函數(shù)，以根據(jù)能源消耗和任務表現(xiàn)的不同來挑選后代.文獻[17]通過分析影響虛擬機的花銷和利用率的因素提出了一種基于博弈論的任務調(diào)度方案，同時提出了一種形式描述語言建模云應用中的不同組件.作者提出了一種逆向歸納博弈算法來保證云應用在提升虛擬機利用率的同時動態(tài)滿足用戶的需求.Petri網(wǎng)的操作語義和相關理論被用來驗證該方法的正確性.

此外，還有部分工作研究了云計算系統(tǒng)中操作和配置的正確性.文獻[18]用SPIN模型檢查工具[19]建模了云計算環(huán)境下的Event-Condition-Action規(guī)則，可以將云計算系統(tǒng)中的種種約束在該工具中建模.同時，系統(tǒng)正確性可以用這些約束的屬性在線性時序邏輯中描述出來.該工具通過擴展SPIN的PROMELA語言實現(xiàn).文獻[20]中用NuSMV模型檢查工具驗證了云計算系統(tǒng)中的一些操作缺陷性質(zhì).作者首先建立了云系統(tǒng)及其性質(zhì)的模型，然后將該模型翻譯為NuSMV語法，最后在一個三層使用Amazon EC2負載均衡的云系統(tǒng)中用模型檢查驗證了一系列性質(zhì).文獻[21]提出了兩種技術來減少云計算系統(tǒng)錯誤配置的風險，一種是把配置修改過程自動合成以減少錯誤修改，另一種是識別系統(tǒng)配置中的缺陷.作者用模型檢查工具實現(xiàn)了這些技術，并通過樣例分析評估了它們的可用性.

2 安全性和加密

在云計算大規(guī)模普及的互聯(lián)網(wǎng)背景下，用戶將大量數(shù)據(jù)存儲在公共網(wǎng)絡中，面臨的其中一個重大威脅就是安全問題.根據(jù)云安全聯(lián)盟公布的《The Treacherous 12——Cloud Computing Top Threats in 2016》[22]，數(shù)據(jù)泄露、憑證被盜等安全問題已經(jīng)成為云計算服務面臨的核心威脅.近年來，科研工作者們開展了許多與云計算安全有關的工作，主要包括驗證安全性協(xié)議和提出新的加密方式等等.

許多工作通過驗證安全規(guī)則來保證云計算系統(tǒng)的安全性.文獻[23]中定義了云演算(Cloud calculus)用來描述云計算系統(tǒng)的拓撲結構和防火墻安全規(guī)則.文獻[24]中提出了一套系統(tǒng)的過程來驗證虛擬機遷移后防火墻策略的安全合法性.云系統(tǒng)中的分布式防火墻配置使用云演算描述的網(wǎng)絡拓撲來定義；防火墻配置表達為命題約束，并基于約束滿足問題建立了一個驗證模型.此外，文章還提出了一個Amazon EC2中的例子說明該方法的適用性和有效性.文獻[25]中提出了一套基于云的安全的信息共享系統(tǒng)，用資源描述框架定義其各種性質(zhì)如可靠性、透明度、一致性、完全性等等.作者準備用ACL2[26]來生成系統(tǒng)滿足的性質(zhì)的機器可驗證的證明過程，但作者沒有提供這些性質(zhì)如何被建模和驗證的細節(jié).文獻[27]提出了一種云計算的安全存儲服務，它結合了不同的安全機制以加強現(xiàn)有方法對威脅的檢測.該方法中使用了審查和監(jiān)控機制來發(fā)現(xiàn)威脅和證明其對安全性質(zhì)的破壞性，并使用有色Petri網(wǎng)對效果進行了評估.

除了在云計算系統(tǒng)中引入安全規(guī)則外，還可以通過加密的方式來保證私有數(shù)據(jù)的安全性和隱私性.文獻[28]中用WebSpi網(wǎng)絡安全庫研究了一系列商業(yè)或?qū)W術的加密網(wǎng)絡應用，并用ProVerif模型檢查工具[29]驗證了加密存儲協(xié)議應對攻擊的安全性.文獻[30]形式化地分析了一種基于ABS(Attribute-based signature)和ABE(Attribute-based encryption)的加密協(xié)議，對該協(xié)議進行了建模，并使用ProVerif自動工具驗證了協(xié)議的安全性質(zhì).文獻[31]對RDIC(Remote data integrity checking)協(xié)議進行了改進，并證明了改進后的協(xié)議能夠滿足舊的協(xié)議不能確保的安全性質(zhì).文獻[32]對一種可能遭受攻擊的RDPC(Remote data possession checking)協(xié)議進行了改進，提供了改進后協(xié)議的安全性的形式化證明，并且通過實現(xiàn)該協(xié)議給出了其表現(xiàn)的報告.文獻[33]提出了一種名為KSF-OABE的加密方法，并證明了該方法在選擇明文攻擊下是安全的.文獻[34]提出了一種新的云存儲加密方法，該方法能夠保證用戶的隱私不會被泄露.

3 故障恢復機制

在云計算系統(tǒng)中，通常采用一些故障恢復機制來增加系統(tǒng)的容錯.這是由于在云計算系統(tǒng)這樣的分布式系統(tǒng)中往往包含成百上千個節(jié)點，節(jié)點故障時有發(fā)生.同時為了應對軟件故障和人為錯誤操作，也有必要采用故障恢復機制避免影響整個系統(tǒng)運轉(zhuǎn).文獻[35]中為云計算提出了一種基于Byzantine故障檢測技術的模型.文中使用了云計算故障網(wǎng)來建模云計算中的不同組件，如服務資源、云模塊等，并分析了模型的一些基本性質(zhì).在此模型的基礎上，作者提出了能夠動態(tài)檢測執(zhí)行時云應用中故障的故障檢測策略，并使用Petri網(wǎng)的操作語義和相關性質(zhì)證明了策略的有效性和正確性.文獻[36]中提出了一種云存儲系統(tǒng)可檢索性方案的動態(tài)證明，這種方案支持公共審核和數(shù)據(jù)損壞時有效恢復通信.

多副本機制是云計算系統(tǒng)故障恢復機制中非常重要的一個部分，它能夠有效地提高云計算系統(tǒng)的可伸縮性和可靠性，同時在一定程度上改善用戶訪問時間.文獻[37]中用基于Event-B的方法建模了多副本數(shù)據(jù)存儲，數(shù)據(jù)存儲中使用了大量復制和預寫日志的方法.作者在同步、半同步、異步架構下實現(xiàn)了該模型,并在可能出錯的場景下驗證了數(shù)據(jù)完整性.文獻[38]用Petri 網(wǎng)通過三種方法：多線程、分布式和基于云的方法建模同一個系統(tǒng)，比較了面對狀態(tài)空間爆炸問題時三者的表現(xiàn).文獻[39]中用CSP建模了Hadoop并行框架，并用PAT模型檢查工具[40]驗證了數(shù)據(jù)局部性及無死鎖等性質(zhì).

4 其他相關研究

虛擬化技術是云計算系統(tǒng)中所使用的關鍵技術，通過該技術，云計算系統(tǒng)能夠?qū)⒂布鎯Y源抽象為一個“資源池”，對資源進行統(tǒng)一管理，從整體上提高資源利用率，并節(jié)約管理成本.文獻[41]中提出了vTRUST建?？蚣苡脕硇问交孛枋鎏摂M系統(tǒng)，并通過自動化驗證現(xiàn)實世界中云計算實現(xiàn)識別缺陷，以說明該框架的效果.文獻[42]中用High-Level Petri Nets建模和分析了三種開源的基于虛擬機器的云管理平臺的結構的和操作的性質(zhì).作者用Satisfiability Modulo Theories Library[43]和Z3[44]建模了100個虛擬機器來驗證模型的正確性和可行性，同時驗證增加虛擬機器的數(shù)量并不影響模型的運轉(zhuǎn)，說明該模型還具有很強的可擴展性和靈活性.在文獻[45]中作者構造了虛擬數(shù)據(jù)中心并發(fā)動態(tài)遷移的性能模型，在該模型下同時進行多個動態(tài)遷移，收集表現(xiàn)數(shù)據(jù).然后用PRISM概率模型檢查工具[46]構造表現(xiàn)模型，驗證了若干云計算系統(tǒng)中的概率性質(zhì).

通常來說，云計算提供的服務分為三個層次，即IaaS、PaaS和SaaS.這三個層次所面對的用戶群體不同.SaaS是軟件的開發(fā)、管理、部署全部由第三方完成，用戶拿來即用，完全不需要關心技術問題.PaaS提供的是軟件部署平臺，抽象掉了硬件和底層細節(jié)，開發(fā)者只需要關注業(yè)務邏輯，不需要關心底層細節(jié).IaaS則提供最底層的服務，用戶需要自己控制底層，實現(xiàn)基礎設施的使用邏輯.文獻[47]為SaaS云傳送模型定義了服務層協(xié)議參數(shù)，并提出一種檢測框架對協(xié)議進行符合性檢查.文獻[48]提出了VaaS的概念，即把在云環(huán)境下進行驗證作為服務提供給用戶.文章給出了VaaS的體系結構和用VaaS驗證模型的方法，并以偶圖為例進行了說明.

除了上述研究工作之外，還有部分工作關注了云計算中工作流、檢索以及事務的相關性質(zhì).文獻[49]使用Z notation[50]形式化了聯(lián)合(federated)云工作流.文章對觀察到的感興趣的性質(zhì)進行了抽象描述，用Z/EVES定理證明器進行了符號化演算，同時使用數(shù)學規(guī)則約束安全性、開銷、依賴關系等來定義這些性質(zhì)，最后給出了一個Haskell實現(xiàn)，輸入用戶工作流和需要的性質(zhì)，生成滿足條件的工作流部署配置.文獻[51]中提出了用Rule Markup Language表達檢索和聚合規(guī)則的形式化方法.在Distributed Data Aggregation Service處理檢索請求時，該方法能夠?qū)z索規(guī)則映射到結構化數(shù)據(jù)的XML格式，以從BlobSeer數(shù)據(jù)存儲系統(tǒng)中獲取非結構化條目.在文獻[52]中，Read Atomic Multi-Partition事務作為一種高效輕量多分區(qū)的事務被提出，它能夠保證讀原子性.作者用rewriting logic給出了RAMP事務的形式化表達，并用Maude工具進行了關鍵形式的模型檢查驗證.在文獻[53]中又進而提出了rewriting logic和Maude工具作為配套的框架來詳細描述和分析云存儲系統(tǒng)的正確性和表現(xiàn).

5 總 結

在本文中，作者調(diào)研了在云計算系統(tǒng)中使用形式化方法驗證系統(tǒng)性質(zhì)的研究工作，并根據(jù)所驗證的性質(zhì)將它們分為資源管理、安全性和加密、故障恢復機制等幾類.雖然目前的工作在一定程度上能夠確保云計算系統(tǒng)在設計和部署時能夠滿足我們所要求的性質(zhì)，但是依然存在很多挑戰(zhàn)，如云計算系統(tǒng)底層的存儲架構的可靠性，與大數(shù)據(jù)有關的算法的性質(zhì)的分析和驗證，云計算系統(tǒng)中并發(fā)程序的驗證等等.