引言

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

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

1 形式化方法與模型檢測

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

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

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

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

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

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

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

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

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

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

3 安全性質(zhì)檢測

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

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

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

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

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

    3．2 虛擬機遷移

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

    該安全性質(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 單點故障與容災(zāi)

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

    3．4 檢測方法

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

4 實例分析

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

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

    場景二進行虛擬機遷移試驗，指定一臺虛擬機為待遷移虛擬機，另一主機為遷移目標，驗證能否進行成功遷移。

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

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

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

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

5 結(jié)語

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

核心關(guān)注：拓步ERP系統(tǒng)平臺是覆蓋了眾多的業(yè)務(wù)領(lǐng)域、行業(yè)應(yīng)用，蘊涵了豐富的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/

本文標題：云計算虛擬環(huán)境的形式化安全驗證

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