引言
基 礎 設 施 即 服 務 \\(IaaS,infrastructure as aservice\\)作為云服務的最底層,利用虛擬化技術將基礎軟硬件進行封裝,為租戶提供彈性和透明的計算存儲服務.目前包括亞馬遜在內的許多IT廠商已經向租戶提供IaaS服務.
隨著IaaS的發展,其安全問題也越發突出:共享的基礎軟硬件資源訪問不受控制、服務提供商的權限不受控制、設計缺陷導致的安全漏洞等,這些問題導致租戶資源的安全完整性無法得到保障;同時,IaaS對外隱藏內部操作,資源狀態對外不可見,更加深了租戶對自身資源數據的安全性憂慮.
針對上述問題,國內外學者進行了一系列研究.Santos針對租戶對資源數據和執行環境的完整性要求,提出TCCP可信云計算框架,該框架對節點的行為進行約束,保證VM只在信任的節點上運行.Khan基于Eucalyptus平臺設計了3個協議,實現VM安全注冊和啟動,并在遷移之前實現對目的節點的驗證.文獻[6,7]從服務提供商的角度出發,通過加密的手段保證租戶資源在啟動之初的靜態完整性.但是這些方案在資源運行過程中缺乏對資源的動態度量和驗證,云服務商無法向租戶提供其資源的完整性證明.
Azad針對IaaS底層物理虛擬機平臺的安全度量問題,提出HyperSentry動態度量框架,實現對VM的動態度量和驗證,但是該方案缺乏有效的完整性度量驗證協議.Bertholon沿用文獻[5,7]中的思想,著重從用戶的角度設計可信云保證IaaS資源的完整性.但是該方案中服務提供商的權限過大,導致云服務特權管理員存在操縱驗證結果的可能;同時,文章也缺乏對協議的安全性證明.
安全協議設計本身就存在困難,同時由于運行環境的復雜性和并發性以及攻擊者能力的不確定性,導致上述協議可能存在潛在的安全問題.形式化驗證方法以其嚴密的邏輯分析能力能夠發現協議存在的缺陷和安全問題.SVO邏輯\\(Syverson P F,Van Oorschot P C\\)作為模態邏輯中的佼佼者,目前已經廣泛應用于安全通信協議、電子商務協議的形式化分析.
本文針對IaaS環境缺乏動態度量和驗證的現狀,借鑒HyperSentry和文獻[14]底層動態度量方案,設計了交互協議使租戶主動發起對自身資源的度量和驗證,增強IaaS資源安全完整狀態的可見性,利用SVO邏輯對所設計的協議進行分析和證明.
1 完整性度量協議設計
1.1 協議交互實體
本協議基于Eucalyptus框架進行設計,Eu-calyptus是一種流行的開源IaaS系統管理平臺,如圖1所示,其具備模塊化的思想構建.主要組件包括:云控制器CLC、集群控制器CC、執行節點Node等.本文提出的度量協議包含3類Eucalyptus節點:CLC、CC、Node,加上租戶和可信第三方TC,一共5個協議交互實體.下面將詳細介紹CLC、CC、Node和TC這4個實體.
CLC是租戶和管理員進入云的主要入口,CC負責管理整個虛擬局域網絡,本文忽略CLC與CC的交互,將CLC和CC統稱CLC,協議中,CLC負責接受租戶的度量驗證請求,并將請求分發到對應的Node節點.
Node作為VM運行的物理節點,通過虛擬機監控器和管理域控制租戶VM的啟動、遷移、中斷、停止等全部生命活動;Node節點安全可信的前提是Node上運行一個可信軟件模塊TVMM,TVMM與底層可信平臺模塊TPM安全交互,完成對Node節點和租戶VM的完整性度量和度量值提交,詳見.Node采用“遲啟動”的方式,在節點啟動前保 證 可 信 軟 件 模 塊TVMM的 可 信 啟 動.該TVMM在節點的全程生命周期內必須正常運行.如果TVMM不能完成可信啟動或者是受到攻擊篡改,則TC通過協議認證部分能夠檢測到TVMM的可信狀態從而判定Node節點是否安全可信.
TC作為可信的第三方實體,不與協議中的任何實體“合謀”,被協議中其他實體\\(租戶、云服務商等\\)所信任.TC在協議中作為第三方可信實體對度量值進行可信驗證和結果反饋,1\\)TC與目的Node節點上的TVMM進行安全交互,通過分析TVMM是否安全運行從而判定Node節點是否可信,2\\)TC對Node節點提交的度量值進行分析和驗證,并將驗證結果生成可信報告反饋給協議發起方\\(即租戶\\).通過引入TC,將協議的度量和驗證分開,增加驗證的可信性,使得云服務商和云管理員無法操縱驗證結果,提高協議過程的安全性.
本文要求所有交互實體必需配置可信密碼硬件TPM\\(除了對租戶沒有要求\\),TPM實現度量值的安全存儲,提供綁定的加密密鑰BK和身份證明密鑰AIK,并在完整性度量協議里對平臺證明信息進行簽名.
完整性度量協議所使用的密鑰均是TPM直接或間接產生的,節點Node、CLC以及可信第三方TC在協議中均使用兩種非對稱密鑰:AIK和BK.本協議嚴格遵循TCG的密鑰規范,使用AIK作為TPM身份證明密鑰對TPM內部數據進行簽名;BK作為實體綁定密鑰,實現會話通道的加密和部分TPM外部數據的簽名.租戶雖然沒有AIK和BK,但是具有CA簽名的一對公私鑰,我們也將該密鑰稱之為BK.AIK和BK的公鑰以證書形式可以被其他節點或者實體訪問,兩類證書經過CA簽名頒發,被認為是可信的.
1.2 協議過程
本文提出的協議允許租戶主動發起對運行環境安全性和資源數據完整性的度量和驗證\\(見圖2\\).因此,協議必須完成以下目標:
目標1 能夠驗證資源數據執行環境的可信性\\(即證明Node節點是否運行安全的TVMM\\);
目標2 能夠度量租戶資源的完整性并將可信的驗證結果反饋給租戶.
該協議由租戶發起,經過一系列的操作交互之后,由TC反饋給租戶資源數據的完整性報告,其詳細過程如下:
M1:User→ CLC:{{{N1,UserID,MLis-tRequest\\(m1,m2,…\\)}BK-1User}BKpubTC,Node}BKCLC
外部租戶發起對VM執行環境和資源完整性的度量:外部租戶產生一個隨機數、租戶ID、度量的組件列表MListRequest\\(m1,m2,…\\),將這些數據用BK私鑰簽名后,利用TC的公鑰加密,保證只有TC能夠看到這些請求.將加密的度量請求與Node節點名稱通過CLC的公鑰加密后傳給CLC.
M2:CLC → Node:{{{N1,UserID,MLis-tRequest\\(m1,m2,…\\)}BK-1User}BKTC,TC}BKNode
CLC將接收到的度量請求數據并解密后,得知目的節點的名字為Node,需要將度量請求分發路由到節點Node,于是加上TC的名稱一起用Node公鑰加密后傳送給Node節點.
M3:Node→ TC:{{{N1,UserID,MLis-tRequest\\(m1,m2,…\\)}BK-1User}BKTC,TC}BKNode,{{N2,PCR1~kNode}AIK-1Node}BKTC
Node節點接收到CLC轉發而來的數據,得知需要向TC提交平臺證明報告,開始和TC進行交互.Node節點將User的簽名加密過的請求數據與自身平臺證明信息一起發送給TC.
M4:TC → Node:{{{N3,UserID,MLis-tRequest\\(m1,m2,…\\)}BK-1TC}BKTC
TC接收到Node節點發送的數據,解密驗證簽名,首先得到User的度量驗證請求,然后驗證Node節點平臺配置,如果平臺配置正確\\(TVMM成功啟動\\)則向Node節點發出度量命令,度量租戶VM相關組件MListRequest\\(m1,m2,…\\);如果Node配置有誤,則TC直接向租戶反饋驗證失敗信息.
M5:Node→TC:{{MListResponse\\(m1,m2,…\\)}BK-1Node,N2,N3}BKTC
Node根據TC要求,將對應組件度量值經過簽名后發送給TC進行完整性校驗.
M6:TC→User:{{N1,Request}BK-1TC}BKUser
TC解密M5中提交的度量結果,首先通過隨機數N2、N3驗證報告的新鮮性,然后通過Node BK的私鑰驗證報告的真實性,將報告值取出后,與注冊階段注冊過的組件完整性參考值進行比對.最后將隨機數N1與驗證結果以及附加驗證信息簽名并加密后反饋給User.至此,完整性度量協議完成.
上述的協議過程必須完成目標1和目標2.其中完成目標1需要確保Node節點平臺證據的真實性和新鮮性;而目標2需要確保組件度量值的真實性和新鮮性;同時目標1和目標2的完成都需要確保反饋結果的真實性和新鮮性.接下來將對協議安全目標進行驗證.
2 協議安全性證明
協議對安全性、完備性要求很高,SVO邏輯基于作為一種廣泛使用的形式化方法能夠通過嚴格的邏輯推理有效驗證協議的安全性和完備性.本文采用SVO邏輯對完整性度量協議進行安全性、完備性證明.
2.1 SVO邏輯
在SVO邏輯的推理中需要首先給出協議的初始化假設集Ω,即用SVO邏輯語言表示出主體的初始信念、接收到的消息和對消息的理解和解釋;然后給出協議可能或者應該達到的目標集Γ,最后通過利用推理規則和公理對假設和協議步驟進行推導,判定協議能否達到預期目標.
SVO邏輯總共有20條公理,下面列出本文過程中需要使用的一些推理規則和公理:
P0:Pbelieves PKσ\\(Q,K\\)∧Preceived{X}k-1\ue01c Pbelieves\\(Qsaid X\\),PKσ\\(Q,K\\)表示K是主體Q的數字簽名驗證密鑰.如果主體P收到密鑰K-1簽名的消息,就可以確定發送者是Q.
P1:Preceived{ }Xk∧Phas K-1\ue01cPreceivedX如果主體P收到公鑰K加密的消息{X}K,且P擁有私鑰K-1,那么P就能收到消息X.
P2:Preceived\\(X1,…,Xn\\)\ue01cPreceived X
P3:Pbelieves\\(Psees X\\)\ue01cPbelieves\\(PseesX\\)F\\(X\\)表示消息X的函數.
P4:Preceived F\\(X\\)∧Pbelieves\\(Psees X\\)\ue01cPbelieve\\(Preceived F\\(X\\)\\)
P5:P believe PKσ\\(Q,K\\)∧P received X∧SV\\(X,K,Y\\)\ue01cPbelieve\\(Qsaid Y\\).表明P相信K是Q的簽名密鑰,且P收到了消息X,同時用密鑰K可以驗證X是Y的簽名,那么P相信Q說過Y.
P6:fresh\\(Xi\\)\ue01cfresh\\(X1,…,Xn\\)
P7:fresh\\(X1,…,Xn\\)\ue01cfresh\\(F\\(X1,…,Xn\\)\\)
P8:fresh\\(X\\)∧Psaid X\ue01cPsays X
P9:fresh\\(X\\)∧Psaid X\ue01cPsaid X.
2.2 協議證明
協議證明之前需要首先對協議的運行環境、實體和消息做出以下合理假設:所有交互實體在協議運行之前通過信任的CA能夠得到其他實體的AIK和BK公鑰證書,因此能夠提前確信實體對應的AIK和BK的公鑰;實體能夠確信自己產生的隨機數的新鮮性,假設具體如下:
A0:協議的運行環境是不安全的
A1:每個主體的公鑰是公開的
A2:每個主體的私鑰僅為其所知
A3:每個主體都相信自己產生的隨機數的新鮮性,即User,Node和TC分別相信N1,N2和N3的新鮮性.
本文將完整性度量協議目標細化為以下5個子目標,并分別進行證明,過程如下:
G1:TC believes\\(User said\\(N1,UserID,MListReq-uest\\)\\),該目標表明TC確信度量請求的發起者是User.
證由M3,P2,A2和P1得到
TC received\\(N1,UserID,MlistRequest\\)BK-1user,該式 利 用 公 理P0得 到TC believes\\(User said\\(N1,UserID,MlistRequest\\),G1得證.
G2:TC believes\\(Node said\\(PCR1-knode\\)\\),該目標表明TC確信平臺配置信息的發送者是節點Node.
證由M3,P2,A2和P1得 到TC received\\(N2,PCR1-knode\\)AIK-1node,該式利用公理P0得到TCbelieves\\(Node said\\(PCR1-knode\\)\\),G2得證.
G3:TC believes\\(Node said\\(MlistResponse\\)\\)該目標表明TC相信租戶VM組件的度量值是真實的,是由TVMM簽名過的.
證由M5、A2、P2和P1得 到TC received\\(MlistResponse\\)AIK-1node,該式通過公理P0得到TCbelieves\\(Node said\\(MlistResponse\\)\\),G3得證.
G4:TC believes fresh\\(MListResponse\\)目標表明TC確信Node的可信報告是新鮮的.
證由M5和P6和P7得到G4,得證.
G5:User believes\\(TC Says N1,{ }Result\\),該目標表明租戶相信VM的反饋信息的真實性和時效性.即租戶相信反饋結果來自于信任的第三方TC,且返回的結果是新鮮的.
證由M6,P2和A2得到User believes{N1,Result}BK-1TC,該式利用通過P0和A1得到Userbelieves\\(TC Said{N1,Result}\\),該式與A3通過P6和P8得到User believes\\(TC Says{N1,result}\\),G5得證.
上述過程表明,在TVMM安全可靠地遵循協議且按照協議與底層TPM硬件與交互執行動態度量,而IaaS服務提供商和租戶完全信任TC的條件下,該協議是安全有效的.G1成功證明TC能夠判定度量請求來自于真實的租戶;G2,G3成功證明TC能夠判定Node節點提交平臺配置屬性是合法的\\(即成功運行有TVMM\\),并且TC相信租戶VM的執行環境度量值來源是真實的,G5證明租戶得到的反饋結果是來自于信任的第三方實體TC.最后G4,G5能夠判定協議傳送的關鍵數據是新鮮的,能夠有效抵抗重放攻擊.租戶通過自身發起的動態度量請求,能夠有效授權TC對VM執行環境和組件完整性進行度量和驗證.租戶通過TC反饋信息獲知VM執行環境的可信狀況\\(目標1\\)并得到其定制組件的完整性狀況\\(目標2\\).
通過SVO邏輯分析,本文面向租戶的完整性度量協議能夠滿足1.2節提出的兩個目標:即對執行環境的可信認證和對定制組件的完整性驗證.同時本協議能夠保持會話的新鮮性、機密性、完整性等,有效抵御重放攻擊、假冒攻擊等多種形式的攻擊.
3 實驗
針對面向租戶資源的完整性度量協議的安全性和有效性驗證,本文開發原型系統對協議的抗攻擊性和性能進行了實驗驗證.
3.1 實驗環境
本研究以Eucalyptus云服務平臺為基礎搭建協議驗證平臺.本實驗環境為:4臺配有Intel E5-2620 6核CPU、16GB RAM的 國 產 服 務 器 作 為CLC、2個NC和TC\\(實驗將CLC和CC作為一個節點\\),1臺配有Intel Corei3-550CPU、2.0GB內存的HP臺式機作為租戶客戶端.本實驗使用的操作系統是WindowsXP和Ubuntu12.04Server,虛擬機監控器采用的是Xen4.3,IaaS管理平臺選用的是Eucalyptus3.1.
本文借鑒HyperSentry的度量框架,如圖3所示,利用TVMM對租戶VM執行度量,TVMM受到SMI handler安全保護,而SMI handler自身存儲在SRAM中,受到主板的硬件保護.SMI han-dler和物理TPM一起作為Node節 點的可 信基TCB,在Node啟動之初,TCB通過“遲啟動”的方式把信任傳遞到TVMM.TVMM安全啟動并正常工作,為協議執行提供基礎.當協議執行時,租戶授權TC通過IPMI通道觸發TVMM對租戶VM的度量,并通過TVMM與TPM的安全交互,將度量值迭代存儲到TPM的寄存器中.
協議驗證平臺搭建完成之后,通過模擬各種攻擊方式對協議實施攻擊,驗證協議能否真實向租戶展示其資源的完整性.同時針對協議的性能問題,實驗得出了協議的平均時間消耗,并做出了相應分析。
3.2 協議實驗結果
3.2.1 安全性分析
為了驗證完整性度量協議能否抵御目前常見的攻擊,我們模擬假冒攻擊、重放攻擊、信息偽造3種攻擊手段.攻擊的前提假設是TC、TPM是安全可信的,同時SMI handler由于受到SRAM的保護,不會受到篡改.
本實驗通過以下攻擊方式對協議進行攻擊實驗:
1\\)假冒攻擊:攻擊者冒充物理節點向TC提交完整性報告;攻擊者冒充TC向租戶反饋錯誤的信息\\(比如租戶資源完整性已經受到破壞,但是攻擊者冒充TC向租戶反饋結果表明其資源完整性沒有受到破壞\\);2\\)重放攻擊:假設節點被攻擊者控制,重復提交過去生成的正確的組件度量值,用以獲取TC的信任;3\\)信息偽造:攻擊者通過篡改Node提交的可信報告,該攻擊可能導致TC驗證錯誤.
攻擊效果如表1所示,1\\)當攻擊者冒充Node節點和可信第三方實體在協議中發送消息時,由于交互之前需要通過驗證簽名驗證對方實體的身份,因此,能夠區分真實協議實體和假冒實體;2\\)重放攻擊主要針對Node節點重復發送度量值的情況,假設攻擊者能夠獲取完整的協議交互的消息,攻擊者通過重復提交度量值試圖獲取TC的信任,但是TC在每次度量驗證時產生一個隨機數N3,能夠利用N3校驗提交的度量值的新鮮性,防止重放攻擊;3\\)攻擊者獲取度量值,試圖篡改度量值并發送給TC,但是由于消息加密,TC收到的是一個不能解密的消息,因此,TC能夠判定發送的消息受到了篡改.
針對上述3類攻擊,租戶發起度量、Node節點執行度量到和TC驗證度量值等過程,協議最終能夠向租戶反饋其資源的真實完整性,如圖4所示,針對上述三類攻擊,TC的可信報告都正確顯示出組件是否受到篡改或者是執行環境Node節點是否可信;同時,如圖5所示,租戶能夠通過TC反饋結果中附加的相關日志文件,能夠查看其資源的度量、驗證信息,提高租戶對自身資源完整狀態的可見性.
通過上述實驗可得,完整性度量協議能夠抵御常見的假冒攻擊、重放攻擊和信息篡改等攻擊方式.協議在受攻擊的情況下,能夠向租戶如實報告租戶資源的完整性狀態,提高租戶對自身資源完整狀態的可見性.
3.2.2 性能分析
本文提出的協議允許租戶對IaaS資源的完整性進行校驗,從租戶發起請求到接收反饋信息的時間消耗關系到租戶的使用體驗.因此,本文需要驗證租戶提出請求到接受反饋結果的時間消耗.由于租戶可以對VM組件進行選擇性的度量\\(度量組件包括中斷表、超級調用表、VM系統敏感數據等\\),為了實驗方便,我們在度量測試時,選擇最大開銷的情況.實驗結果如圖6所示.
根據圖6,租戶從發起度量驗證請求到接收到反饋結果,其平均時間消耗為864.2ms.我們分析其時間主要消耗在對Node節點的平臺度量、對VM組件的度量以及交互證明的執行,并且完整性度量協議時耗隨度量組件的個數增加而增加.實驗度量組件采取最大開銷的情況,因此864.2ms可以作為完整性度量協議的時間上限,租戶從發起請求到接收到反饋結果,其時間消耗不會超過864.2ms,可以認為不會影響租戶體驗.
4 結論
針對IaaS租戶對自身資源缺乏度量和驗證的現狀,本文將可信度量引入到IaaS環境,并設計面向租戶的IaaS完整性校驗協議,使租戶主動發起對自身資源的完整性驗證,增強租戶對資源完整狀態的可見性.文章通過SVO邏輯對協議的安全性、完備性進行了證明,并搭建實驗平臺對協議的抗攻擊性和性能進行了實驗.分析和實驗表明,協議能夠抵御常見的假冒攻擊、重放攻擊和篡改攻擊等攻擊模式,能向租戶反饋其資源完整性的真實狀態;同時,協議時間消耗在可接受范圍內,對租戶的使用體驗影響不大.【圖略】
