引言
云計算是近年來IT產業的熱門詞匯，在谷歌的定義中，云計算是以公開的標準和服務為基礎，以互聯網為中心提供安全、快速、便捷的數據存儲和網絡計算服務模式。虛擬化?是對資源(CPU、存儲器、網絡、應用棧和數據庫)的抽象，不同的用戶根據需要提出訪問請求并獲取資源，而無需關心資源的具體位置。虛擬化將傳統的數據中心轉化為適合云計算的運行節點，為云環境提供統一、易用的資源組織和使用方式 。
然而， 由于云計算的信息系統本質， 云計算具有自身的安全問題，虛擬化即是其中一個重要方面。云計算供應商對虛擬環境的安全構建及驗證進行了大量的研究，在驗證技術方面，主要的趨勢還是使用傳統手段如硬件可靠性測試、功能覆蓋率測試等，其得到的結果傾向于工程化，未實現理論層面的完全驗證能力。形式化方法作為系統建模和指標驗證的重要手段，其應用逐漸由硬件領域向信息系統拓展，在用于虛擬機性質驗證的方面已取得了一定成果 ，但尚缺乏針對云計算背景下虛擬環境安全需求的驗證方法研究。
1 形式化方法與模型檢測
形式化方法的基本含義是借助數學的方法來研究計算機與數學科學問題，在系統構建、實現的全過程中，凡是采用嚴格的數學語言，具有精確的數學語義的方法，都可以稱之為形式化方法。經過40多年的發展，形式化方法已經從理論研究逐漸走向成熟和實用化，在航空航天系統、通訊系統和集成電路等領域得到了較為廣泛的應用。
由于潛在的系統錯誤數量總是和組件的數量成正比，云計算這一新興計算方式包含的組件眾多，實現技術如虛擬化等特點極大地增加了復雜性。基于形式化方法中的模型檢測在探查設計潛在缺陷方面的能力，使用模型檢測對云計算虛擬化環境進行安全性質驗證具備可操作性。
2 虛擬化環境建模
虛擬化技術的目的是為應用提供更強的計算能力和更大的靈活性，這項優勢較好地契合了云計算的需求和主要理念。但虛擬化技術提升云基礎設施使用效率的同時也使傳統的安全防護手段失效 ，在實施虛擬化的同時需要對云計算環境整體可靠性進行評估驗證。虛擬環境構成模型如圖1所示。
圖1 虛擬環境構成模型
形式化驗證過程一般需要經過配置采集、需求分析、模型輸出3個階段：
1)配置采集。定義虛擬化環境中虛擬應用程序的集合為Apps，虛擬機的集合為Vms，物理主機的集合為Hosts，網絡的集合為Networks，令集合Unit為虛擬環境中的元素集合，可以使用一階邏輯定義以下謂詞，如表1所示。虛擬環境的配置采集過程即為集合、謂詞的實例化過程，從而確定所有虛擬應用程序及虛擬機的位置關系、網絡的連通情況、環境內主機的數量規模等。表1虛擬驗證環境謂詞定義
表1 虛擬驗證環境謂詞定義
2)需求分析。需求分析階段的目標是得到形式化語言刻畫的安全性質語句，一般也用邏輯命題的形式表述，是需要判定的，即系統的安全目標。這類謂詞中包含的是虛擬化環境中人們某一方面感興趣的安全性質，包括功能正確性、可達性、安全性、活性等。
3)模型輸出。模型輸出將綜合配置采集和需求分析兩個階段的結果，按照模型檢測器的輸入要求進行優化、規范化，以提高后續模型檢測工作執行的效率。
3 安全性質檢測
安全性質模型檢測是虛擬化環境形式化安全驗證的核心步驟，其中虛擬應用安全隔離、虛擬機遷移和單點故障容災是云計算領域關注的焦點問題，云服務運營商通過功能、性能驗證對虛擬化環境的元素進行調整以達到最佳的安全性能，降低故障概率，提高用戶滿意度。
3．1虛擬應用安全隔離
在云計算環境中往往部署著多種虛擬應用程序，為了性能、安全起見，應根據應用程序的種類和QoS等級進行劃分，如運行數據庫服務的虛擬機最好與郵件系統分隔開來，避免相互訪問產生安全隱患等。
定義謂詞reach(a，b)為兩應用程序能夠互相訪問，則希望驗證的性質可表達為：對于Apps的子集AppA、AppB，不希望兩集合中的程序能夠相互訪問， 即命題reach(appa，appb對于任何appa∈Appa、appb∈Appb均不成立。其完整性質如下：
secureIsolation(Appa，Appb):┐∨reach(appa，appb)
3．2 虛擬機遷移
虛擬機遷移是實現虛擬化環境高可用性的關鍵能力之一，在因物理、負載、系統原因導致的虛擬機功能失效情況下，需要立即將原虛擬機遷移至另一臺物理機上運行，保證業務的連續性。在本場景中，考慮到虛擬機與主機的安全等級必須匹配，安全等級為高的虛擬機只能運行在安全等級為高(isHigh)的主機上，而安全等級低(isNonnal)的虛擬機可以運行在兩種主機上。
該安全性質可以表述為：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 單點故障與容災
云計算環境中的節點都存在失效的可能，在這種情況下系統和資源容災是必須要考慮的因素。對于用戶而言，在災難發生時，系統的任何一個部分都可能產生故障，Failure(unit)謂詞的參數是整個Units集合，為保證系統避免單點失效，希望用戶在災難發生前后都能保證getService(app)成立， 即：disasterRecovery(app)：getService(app):getService(app)/failure(u))。其中，條件因子failu(u))表示去除模型中所有與u相關的事實，如果該性質滿足，說明云計算虛擬環境具有容災能力，在災難發生后不需要人工干預就能夠自動保證服務連續性。
3．4 檢測方法
在虛擬化環境模型和待驗證的安全性質確定后，檢測器將算法選項參數初始化，并輸入待檢測的語句作為未知命題進行演算，窮舉模型空間里的謂詞和給定事實，尋找能夠匹配的規則，將命題進一步分解，直到能夠成功求值并返回演算結果，整個計算過程在遍歷了整棵演算樹后結束，根據獲得的中間結果組合成最終返回值，給出“是”、“否” 、“系統異常”的驗證結果。
4 實例分析
這里用一個實例分析對虛擬環境進行驗證的有效性，使用一個包含29臺物理機(劃分為6個網段)、共計75個虛擬機和237個虛擬應用程序的環境，設計了3個試驗場景，定義如下：
場景一進行虛擬應用程序的安全隔離試驗，驗證應用程序間的訪問連通性。
場景二進行虛擬機遷移試驗，指定一臺虛擬機為待遷移虛擬機，另一主機為遷移目標，驗證能否進行成功遷移。
場景三先后將指定的虛擬機、主機、網絡設為失效模式，驗證業務連續性的保證情況。
表2 驗證場景測試結果
所有試驗在一臺配置為i5 CPU，內存為4 096 MB的計算機上運行，使用的模型檢測器為Visual Prolog，其測試結果如表2所示。表2驗證場景測試結果
試驗結果表明，形式化方法對于云計算虛擬環境的安全驗證是有效的。
5 結語
云計算作為新興的計算、存儲資源使用模式，在提供更高性能、更易于使用的服務的同時，其衍生出來的安全問題，特別是虛擬環境的安全問題制約著云計算的發展和進一步應用。形式化方法作為信息系統的可靠性驗證方法，在虛擬化環境驗證領域同樣能夠發揮效能，為云計算虛擬環境提供安全需求的嚴格驗證能力，實現云可靠性、安全性的提升。
核心關注：拓步ERP系統平臺是覆蓋了眾多的業務領域、行業應用，蘊涵了豐富的ERP管理思想，集成了ERP軟件業務管理理念，功能涉及供應鏈、成本、制造、CRM、HR等眾多業務領域的管理，全面涵蓋了企業關注ERP管理系統的核心領域，是眾多中小企業信息化建設首選的ERP管理軟件信賴品牌。
轉載請注明出處：拓步ERP資訊網http://www.guhuozai8.cn/
本文標題：云計算虛擬環境的形式化安全驗證
相關文章
