引言

    云計(jì)算是近年來IT產(chǎn)業(yè)的熱門詞匯，在谷歌的定義中，云計(jì)算是以公開的標(biāo)準(zhǔn)和服務(wù)為基礎(chǔ)，以互聯(lián)網(wǎng)為中心提供安全、快速、便捷的數(shù)據(jù)存儲(chǔ)和網(wǎng)絡(luò)計(jì)算服務(wù)模式。虛擬化?是對資源(CPU、存儲(chǔ)器、網(wǎng)絡(luò)、應(yīng)用棧和數(shù)據(jù)庫)的抽象，不同的用戶根據(jù)需要提出訪問請求并獲取資源，而無需關(guān)心資源的具體位置。虛擬化將傳統(tǒng)的數(shù)據(jù)中心轉(zhuǎn)化為適合云計(jì)算的運(yùn)行節(jié)點(diǎn)，為云環(huán)境提供統(tǒng)一、易用的資源組織和使用方式 。

    然而， 由于云計(jì)算的信息系統(tǒng)本質(zhì)， 云計(jì)算具有自身的安全問題，虛擬化即是其中一個(gè)重要方面。云計(jì)算供應(yīng)商對虛擬環(huán)境的安全構(gòu)建及驗(yàn)證進(jìn)行了大量的研究，在驗(yàn)證技術(shù)方面，主要的趨勢還是使用傳統(tǒng)手段如硬件可靠性測試、功能覆蓋率測試等，其得到的結(jié)果傾向于工程化，未實(shí)現(xiàn)理論層面的完全驗(yàn)證能力。形式化方法作為系統(tǒng)建模和指標(biāo)驗(yàn)證的重要手段，其應(yīng)用逐漸由硬件領(lǐng)域向信息系統(tǒng)拓展，在用于虛擬機(jī)性質(zhì)驗(yàn)證的方面已取得了一定成果 ，但尚缺乏針對云計(jì)算背景下虛擬環(huán)境安全需求的驗(yàn)證方法研究。

1 形式化方法與模型檢測

    形式化方法的基本含義是借助數(shù)學(xué)的方法來研究計(jì)算機(jī)與數(shù)學(xué)科學(xué)問題，在系統(tǒng)構(gòu)建、實(shí)現(xiàn)的全過程中，凡是采用嚴(yán)格的數(shù)學(xué)語言，具有精確的數(shù)學(xué)語義的方法，都可以稱之為形式化方法。經(jīng)過40多年的發(fā)展，形式化方法已經(jīng)從理論研究逐漸走向成熟和實(shí)用化，在航空航天系統(tǒng)、通訊系統(tǒng)和集成電路等領(lǐng)域得到了較為廣泛的應(yīng)用。

    由于潛在的系統(tǒng)錯(cuò)誤數(shù)量總是和組件的數(shù)量成正比，云計(jì)算這一新興計(jì)算方式包含的組件眾多，實(shí)現(xiàn)技術(shù)如虛擬化等特點(diǎn)極大地增加了復(fù)雜性�；�于形式化方法中的模型檢測在探查設(shè)計(jì)潛在缺陷方面的能力，使用模型檢測對云計(jì)算虛擬化環(huán)境進(jìn)行安全性質(zhì)驗(yàn)證具備可操作性。

2 虛擬化環(huán)境建模

    虛擬化技術(shù)的目的是為應(yīng)用提供更強(qiáng)的計(jì)算能力和更大的靈活性，這項(xiàng)優(yōu)勢較好地契合了云計(jì)算的需求和主要理念。但虛擬化技術(shù)提升云基礎(chǔ)設(shè)施使用效率的同時(shí)也使傳統(tǒng)的安全防護(hù)手段失效 ，在實(shí)施虛擬化的同時(shí)需要對云計(jì)算環(huán)境整體可靠性進(jìn)行評估驗(yàn)證。虛擬環(huán)境構(gòu)成模型如圖1所示。

    圖1 虛擬環(huán)境構(gòu)成模型

    形式化驗(yàn)證過程一般需要經(jīng)過配置采集、需求分析、模型輸出3個(gè)階段：

    1)配置采集。定義虛擬化環(huán)境中虛擬應(yīng)用程序的集合為Apps，虛擬機(jī)的集合為Vms，物理主機(jī)的集合為Hosts，網(wǎng)絡(luò)的集合為Networks，令集合Unit為虛擬環(huán)境中的元素集合，可以使用一階邏輯定義以下謂詞，如表1所示。虛擬環(huán)境的配置采集過程即為集合、謂詞的實(shí)例化過程，從而確定所有虛擬應(yīng)用程序及虛擬機(jī)的位置關(guān)系、網(wǎng)絡(luò)的連通情況、環(huán)境內(nèi)主機(jī)的數(shù)量規(guī)模等。表1虛擬驗(yàn)證環(huán)境謂詞定義

表1 虛擬驗(yàn)證環(huán)境謂詞定義

    2)需求分析。需求分析階段的目標(biāo)是得到形式化語言刻畫的安全性質(zhì)語句，一般也用邏輯命題的形式表述，是需要判定的，即系統(tǒng)的安全目標(biāo)。這類謂詞中包含的是虛擬化環(huán)境中人們某一方面感興趣的安全性質(zhì)，包括功能正確性、可達(dá)性、安全性、活性等。

    3)模型輸出。模型輸出將綜合配置采集和需求分析兩個(gè)階段的結(jié)果，按照模型檢測器的輸入要求進(jìn)行優(yōu)化、規(guī)范化，以提高后續(xù)模型檢測工作執(zhí)行的效率。

3 安全性質(zhì)檢測

    安全性質(zhì)模型檢測是虛擬化環(huán)境形式化安全驗(yàn)證的核心步驟，其中虛擬應(yīng)用安全隔離、虛擬機(jī)遷移和單點(diǎn)故障容災(zāi)是云計(jì)算領(lǐng)域關(guān)注的焦點(diǎn)問題，云服務(wù)運(yùn)營商通過功能、性能驗(yàn)證對虛擬化環(huán)境的元素進(jìn)行調(diào)整以達(dá)到最佳的安全性能，降低故障概率，提高用戶滿意度。

    3．1虛擬應(yīng)用安全隔離

    在云計(jì)算環(huán)境中往往部署著多種虛擬應(yīng)用程序，為了性能、安全起見，應(yīng)根據(jù)應(yīng)用程序的種類和QoS等級進(jìn)行劃分，如運(yùn)行數(shù)據(jù)庫服務(wù)的虛擬機(jī)最好與郵件系統(tǒng)分隔開來，避免相互訪問產(chǎn)生安全隱患等。

    定義謂詞reach(a，b)為兩應(yīng)用程序能夠互相訪問，則希望驗(yàn)證的性質(zhì)可表達(dá)為：對于Apps的子集AppA、AppB，不希望兩集合中的程序能夠相互訪問， 即命題reach(appa，appb對于任何appa∈Appa、appb∈Appb均不成立。其完整性質(zhì)如下：

    secureIsolation(Appa，Appb):┐∨reach(appa，appb)

    3．2 虛擬機(jī)遷移

    虛擬機(jī)遷移是實(shí)現(xiàn)虛擬化環(huán)境高可用性的關(guān)鍵能力之一，在因物理、負(fù)載、系統(tǒng)原因?qū)е碌奶摂M機(jī)功能失效情況下，需要立即將原虛擬機(jī)遷移至另一臺(tái)物理機(jī)上運(yùn)行，保證業(yè)務(wù)的連續(xù)性。在本場景中，考慮到虛擬機(jī)與主機(jī)的安全等級必須匹配，安全等級為高的虛擬機(jī)只能運(yùn)行在安全等級為高(isHigh)的主機(jī)上，而安全等級低(isNonnal)的虛擬機(jī)可以運(yùn)行在兩種主機(jī)上。

    該安全性質(zhì)可以表述為：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 單點(diǎn)故障與容災(zāi)

     云計(jì)算環(huán)境中的節(jié)點(diǎn)都存在失效的可能，在這種情況下系統(tǒng)和資源容災(zāi)是必須要考慮的因素。對于用戶而言，在災(zāi)難發(fā)生時(shí)，系統(tǒng)的任何一個(gè)部分都可能產(chǎn)生故障，F(xiàn)ailure(unit)謂詞的參數(shù)是整個(gè)Units集合，為保證系統(tǒng)避免單點(diǎn)失效，希望用戶在災(zāi)難發(fā)生前后都能保證getService(app)成立， 即：disasterRecovery(app)：getService(app):getService(app)/failure(u))。其中，條件因子failu(u))表示去除模型中所有與u相關(guān)的事實(shí)，如果該性質(zhì)滿足，說明云計(jì)算虛擬環(huán)境具有容災(zāi)能力，在災(zāi)難發(fā)生后不需要人工干預(yù)就能夠自動(dòng)保證服務(wù)連續(xù)性。

    3．4 檢測方法

    在虛擬化環(huán)境模型和待驗(yàn)證的安全性質(zhì)確定后，檢測器將算法選項(xiàng)參數(shù)初始化，并輸入待檢測的語句作為未知命題進(jìn)行演算，窮舉模型空間里的謂詞和給定事實(shí)，尋找能夠匹配的規(guī)則，將命題進(jìn)一步分解，直到能夠成功求值并返回演算結(jié)果，整個(gè)計(jì)算過程在遍歷了整棵演算樹后結(jié)束，根據(jù)獲得的中間結(jié)果組合成最終返回值，給出“是”、“否” 、“系統(tǒng)異�！钡尿�(yàn)證結(jié)果。

4 實(shí)例分析

    這里用一個(gè)實(shí)例分析對虛擬環(huán)境進(jìn)行驗(yàn)證的有效性，使用一個(gè)包含29臺(tái)物理機(jī)(劃分為6個(gè)網(wǎng)段)、共計(jì)75個(gè)虛擬機(jī)和237個(gè)虛擬應(yīng)用程序的環(huán)境，設(shè)計(jì)了3個(gè)試驗(yàn)場景，定義如下：

    場景一進(jìn)行虛擬應(yīng)用程序的安全隔離試驗(yàn)，驗(yàn)證應(yīng)用程序間的訪問連通性。

    場景二進(jìn)行虛擬機(jī)遷移試驗(yàn)，指定一臺(tái)虛擬機(jī)為待遷移虛擬機(jī)，另一主機(jī)為遷移目標(biāo)，驗(yàn)證能否進(jìn)行成功遷移。

    場景三先后將指定的虛擬機(jī)、主機(jī)、網(wǎng)絡(luò)設(shè)為失效模式，驗(yàn)證業(yè)務(wù)連續(xù)性的保證情況。

表2 驗(yàn)證場景測試結(jié)果

    所有試驗(yàn)在一臺(tái)配置為i5 CPU，內(nèi)存為4 096 MB的計(jì)算機(jī)上運(yùn)行，使用的模型檢測器為Visual Prolog，其測試結(jié)果如表2所示。表2驗(yàn)證場景測試結(jié)果

    試驗(yàn)結(jié)果表明，形式化方法對于云計(jì)算虛擬環(huán)境的安全驗(yàn)證是有效的。

5 結(jié)語

    云計(jì)算作為新興的計(jì)算、存儲(chǔ)資源使用模式，在提供更高性能、更易于使用的服務(wù)的同時(shí)，其衍生出來的安全問題，特別是虛擬環(huán)境的安全問題制約著云計(jì)算的發(fā)展和進(jìn)一步應(yīng)用。形式化方法作為信息系統(tǒng)的可靠性驗(yàn)證方法，在虛擬化環(huán)境驗(yàn)證領(lǐng)域同樣能夠發(fā)揮效能，為云計(jì)算虛擬環(huán)境提供安全需求的嚴(yán)格驗(yàn)證能力，實(shí)現(xiàn)云可靠性、安全性的提升。

核心關(guān)注：拓步ERP系統(tǒng)平臺(tái)是覆蓋了眾多的業(yè)務(wù)領(lǐng)域、行業(yè)應(yīng)用，蘊(yùn)涵了豐富的ERP管理思想，集成了ERP軟件業(yè)務(wù)管理理念，功能涉及供應(yīng)鏈、成本、制造、CRM、HR等眾多業(yè)務(wù)領(lǐng)域的管理，全面涵蓋了企業(yè)關(guān)注ERP管理系統(tǒng)的核心領(lǐng)域，是眾多中小企業(yè)信息化建設(shè)首選的ERP管理軟件信賴品牌。

轉(zhuǎn)載請注明出處：拓步ERP資訊網(wǎng)http://www.ezxoed.cn/

本文標(biāo)題：云計(jì)算虛擬環(huán)境的形式化安全驗(yàn)證

本文網(wǎng)址：http://www.ezxoed.cn/html/consultation/1083972411.html