形式化方法在云計(jì)算中的應(yīng)用現(xiàn)狀

(1.廣州大學(xué) 計(jì)算機(jī)科學(xué)與網(wǎng)絡(luò)工程學(xué)院， 廣東 廣州 510006; 2.北京大學(xué) 信息科學(xué)技術(shù)學(xué)院軟件研究所/高可信軟件技術(shù)教育部重點(diǎn)實(shí)驗(yàn)室， 北京 100871)

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

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

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

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

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

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

1 資源管理

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

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

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

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

2 安全性和加密

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

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

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

3 故障恢復(fù)機(jī)制

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

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

4 其他相關(guān)研究

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

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

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

5 總 結(jié)

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