基于π演算的云服務(wù)安全檢測(cè)

劉 磊，任俊綺，張 鵬，申 春

（1.吉林大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，長(zhǎng)春 130012；2.吉林大學(xué) 軟件學(xué)院，長(zhǎng)春 130012）

云計(jì)算因其寬帶互聯(lián)、資源池共享、彈性配置、按需服務(wù)和按服務(wù)收費(fèi)等優(yōu)勢(shì)在各行業(yè)中廣泛應(yīng)用，但云安全問(wèn)題限制了云計(jì)算的發(fā)展.云服務(wù)的安全問(wèn)題包括云計(jì)算架構(gòu)是否安全、是否存在可攻擊面、對(duì)惡意軟件的處理是否全面及訪問(wèn)權(quán)限是否安全等［1］.非法入侵和云服務(wù)不完整是云安全中的兩個(gè)重要問(wèn)題.入侵是指利用服務(wù)器的弱點(diǎn)對(duì)服務(wù)器進(jìn)行攻擊.入侵檢測(cè)技術(shù)主要分為兩類(lèi)：異常入侵檢測(cè)和誤用入侵檢測(cè)［2］.用戶越權(quán)訪問(wèn)是一種較常見(jiàn)的入侵，是指用戶經(jīng)過(guò)了授權(quán)，但對(duì)所授權(quán)的數(shù)據(jù)和資源使用不合法或?yàn)E用授權(quán)，這可能使云服務(wù)中斷，導(dǎo)致服務(wù)不完整.服務(wù)不完整是指云不能按照服務(wù)流程向用戶提供完整的服務(wù).入侵的發(fā)生可能使服務(wù)中斷，導(dǎo)致服務(wù)不完整；另一方面，服務(wù)不完整會(huì)引發(fā)服務(wù)異常，增加入侵的可能性.

針對(duì)上述問(wèn)題，Kruegel等［3］提出建立異常入侵檢測(cè)Bayes網(wǎng)分析異常檢測(cè)結(jié)果的方法檢測(cè)入侵行為；Teng等［4］提出利用時(shí)間推理的方法產(chǎn)生用戶正常行為規(guī)則集，通過(guò)動(dòng)態(tài)修改這些規(guī)則實(shí)現(xiàn)入侵行為檢測(cè)；Lane等［5］提出通過(guò)機(jī)器學(xué)習(xí)實(shí)現(xiàn)入侵檢測(cè)；Lee等［6］提出利用數(shù)據(jù)挖掘技術(shù)在數(shù)據(jù)和數(shù)據(jù)流中提取相關(guān)知識(shí)，并利用這些知識(shí)檢測(cè)入侵行為；Sailer等［7］提出利用TCG可信平臺(tái)完整性測(cè)量框架驗(yàn)證服務(wù)的完整性；Clark等［8］提出使用Clark－Wilson模型保證服務(wù)的完整性.

當(dāng)前檢測(cè)方法或偏重于入侵檢測(cè)，或偏重于服務(wù)完整性檢測(cè).利用不同檢測(cè)方法對(duì)兩種問(wèn)題分別檢測(cè)時(shí)，存在對(duì)異常行為的重復(fù)檢測(cè)，檢測(cè)成本較高，同時(shí)需要預(yù)測(cè)的非法行為集合可能不全面［9］，檢測(cè)準(zhǔn)確率較低.本文針對(duì)這兩個(gè)問(wèn)題提出了一種安全檢測(cè)方法，運(yùn)用π演算對(duì)云服務(wù)的通信過(guò)程進(jìn)行建模，通過(guò)對(duì)通信原語(yǔ)的形式化描述，檢測(cè)出通信過(guò)程中所出現(xiàn)的用戶越權(quán)訪問(wèn)問(wèn)題和服務(wù)不完整問(wèn)題.利用π演算的方法不需要預(yù)測(cè)非法行為集合，減少了交叉行為的檢測(cè)，可有效減少檢測(cè)計(jì)算量和檢測(cè)時(shí)間.

1 π演算

π演算是對(duì)通信系統(tǒng)演算的擴(kuò)充與發(fā)展，它主要研究進(jìn)程間移動(dòng)通信的并發(fā)理論［10］.π演算的研究對(duì)象是名字和進(jìn)程，其中名字不僅包含CCS中的變量和值，同時(shí)也包含通道名字本身［11］，使π演算對(duì)建立新通道有了描述語(yǔ)法.因此，π演算適合描述動(dòng)態(tài)變化的云服務(wù).本文利用π演算這種形式化描述工具對(duì)云服務(wù)進(jìn)行建模描述，利用π演算的強(qiáng)模擬性、弱模擬性和對(duì)偶性等性質(zhì)對(duì)模型中的用戶越權(quán)問(wèn)題及服務(wù)過(guò)程不完整問(wèn)題進(jìn)行檢測(cè).

π演算語(yǔ)法：假設(shè)一個(gè)無(wú)窮的名字集N，其中的元素用小寫(xiě)字母x，y，z…表示，進(jìn)程表達(dá)式用大寫(xiě)字母P，Q，R…表示.π演算可定義為

2 基于π演算的云服務(wù)建模

2.1 云服務(wù)的描述

通過(guò)對(duì)salesforce CRM，Amazon Webservices和Goole App Engine等云服務(wù)的理解與分析［12－13］，本文將云服務(wù)抽象成一個(gè)三元組（S，C，A），其中：A表示邏輯服務(wù)原子；C表示服務(wù)間的關(guān)系；S表示整個(gè)服務(wù).A是指根據(jù)要檢測(cè)的問(wèn)題，將某個(gè)或某些服務(wù)組合在一起所構(gòu)成的模塊，它是一個(gè)五元組（a，e，s，t，c），其中：a表示A中的服務(wù)；e表示對(duì)外發(fā)出的信息及通道；s表示接收的消息及通道；t表示服務(wù)原子在接收或發(fā)出消息后的動(dòng)作；c表示兩個(gè)e或s之間的關(guān)系；c1表示順序關(guān)系；c2表示并發(fā)關(guān)系.通常情況下，對(duì)于a1發(fā)出的消息和通道e必存在a2接收相同消息的通道s，將二者合并記為es.C中有3個(gè)元素｛C1，C2，C3｝，其中C1表示順序執(zhí)行服務(wù)，C2表示并發(fā)執(zhí)行服務(wù)，C3表示選擇執(zhí)行服務(wù)，且C2，C3優(yōu)先級(jí)相同均高于C1.從而每個(gè)服務(wù)原子可描述為

兩個(gè)服務(wù)原子之間通信過(guò)程可描述為

整個(gè)云服務(wù)可描述為

其中：A1必為啟動(dòng)整個(gè)服務(wù)的服務(wù)原子；An為結(jié)束整個(gè)服務(wù)的服務(wù)原子.

上述過(guò)程中忽略了某些與越權(quán)問(wèn)題和完整性檢測(cè)無(wú)關(guān)的內(nèi)容，將關(guān)注點(diǎn)放在邏輯服務(wù)原子、服務(wù)原子間通信內(nèi)容和通信通道及服務(wù)原子間的邏輯關(guān)系這3個(gè)內(nèi)容上.

2.2 基于π演算的云服務(wù)形式化描述

利用π演算對(duì)云服務(wù)進(jìn)行描述，需有如下過(guò)程：1）將每個(gè)邏輯服務(wù)原子視為一個(gè)進(jìn)程，該進(jìn)程可根據(jù)實(shí)際要驗(yàn)證或檢測(cè)的問(wèn)題細(xì)化或組合；2）將進(jìn)行通信的兩個(gè)進(jìn)程之間順序傳遞消息的通道合并為一個(gè)，并保證這兩個(gè)進(jìn)程間至少有一條通道；3）將并發(fā)的多條消息通道映射為多個(gè)通道，保證每個(gè)并發(fā)的消息通道對(duì)應(yīng)一個(gè)通道.云服務(wù)與π演算的映射關(guān)系列于表1.

表1 云服務(wù)與π演算映射關(guān)系Table 1 Mappings between cloud service andπ－calculus

3 基于π演算對(duì)安全問(wèn)題的檢測(cè)

3.1 越權(quán)問(wèn)題的檢測(cè)

3.2 服務(wù)過(guò)程不完整的檢測(cè)

檢測(cè)服務(wù)是否完整需要用到π演算性質(zhì)：若P強(qiáng)模擬Q，則表示P至少能完成Q的所有任務(wù)和動(dòng)態(tài)變化；若P弱模擬Q，則表示P的外部行為至少能表達(dá)所有Q的外部行為.若用Atomicn表示每個(gè)邏輯服務(wù)原子的進(jìn)程表達(dá)式，ReverceAn表示每個(gè)邏輯服務(wù)原子對(duì)偶系統(tǒng)的進(jìn)程表達(dá)式，T表示服務(wù)完整，F(xiàn)表示服務(wù)不完整表示π演算中的反應(yīng)符號(hào)，則有如下算法.

4 實(shí)例分析

云中存在大量的虛擬機(jī)，虛擬機(jī)部署是云中常見(jiàn)的服務(wù).虛擬機(jī)部署過(guò)程中會(huì)伴隨大量的用戶訪問(wèn)和部署過(guò)程中斷.因此，本文以虛擬機(jī)部署服務(wù)為例，對(duì)所給方法進(jìn)行驗(yàn)證與說(shuō)明.

4.1 服務(wù)流程與抽象

一次虛擬機(jī)部署服務(wù)過(guò)程如圖1所示.發(fā)出部署命令的可能是用戶也可能是某個(gè)物理機(jī)，本文將其統(tǒng)稱(chēng)為用戶.將用戶、應(yīng)用服務(wù)器、云管理和目標(biāo)宿主機(jī)作為4個(gè)邏輯服務(wù)原子進(jìn)行建模，即A＝｛Client，Service，Management，Host｝，且這些模塊是按順序依次發(fā)生的，即

圖1 虛擬機(jī)的部署服務(wù)Fig.1 Deployment of the virtual machine

一次部署請(qǐng)求發(fā)出后，應(yīng)用服務(wù)器對(duì)當(dāng)前環(huán)境進(jìn)行衡量，確定部署請(qǐng)求是否可以接受，若接受則對(duì)相應(yīng)的物理資源進(jìn)行部署，并將部署成功的虛擬機(jī)交付使用.

部署名字集合

其中：Request（Req）表示用戶向應(yīng)用服務(wù)器發(fā)出虛擬機(jī)部署請(qǐng)求；Refuse（Ref）表示應(yīng)用服務(wù)器根據(jù)當(dāng)前環(huán)境判斷不滿足部署要求，向用戶發(fā)出拒絕請(qǐng)求的回應(yīng)消息；AskInfo（Ask）表示應(yīng)用服務(wù)器根據(jù)當(dāng)前環(huán)境判斷可以部署服務(wù)，則向用戶發(fā)出詢(xún)問(wèn)部署虛擬機(jī)所需的具體信息；ProInfo（Pro）表示用戶回應(yīng)應(yīng)用服務(wù)器，提供部署虛擬機(jī)所需的信息；GetResInfo（Get）表示應(yīng)用服務(wù)器根據(jù)用戶所提出的請(qǐng)求，向云管理系統(tǒng)發(fā)出請(qǐng)求部署信息；ResInfo（Res）表示云管理系統(tǒng)向應(yīng)用服務(wù)器發(fā)送相應(yīng)部署信息；DeploymentCommand（DeC）表示應(yīng)用服務(wù)器根據(jù)云管理系統(tǒng)提供信息向目標(biāo)宿主機(jī)發(fā)布部署命令，并傳遞部署請(qǐng)求；DeploymentSuccess（Des）表示部署成功并啟動(dòng)虛擬機(jī)，通知用戶部署結(jié)果并交付使用.

圖2 虛擬機(jī)部署映射成π演算的過(guò)程Fig.2 Virtual machine deployment mapping intoπ－calculus

4.2 服務(wù)建模

根據(jù)云服務(wù)與π演算的映射關(guān)系，可以將圖1映射成圖2，其中x，y，z，v分別表示用戶與應(yīng)用服務(wù)器、應(yīng)用服務(wù)器與云管理服務(wù)器、應(yīng)用服務(wù)器與目標(biāo)宿主機(jī)、用戶與目標(biāo)宿主機(jī)間的通道.

在對(duì)虛擬機(jī)部署過(guò)程進(jìn)行映射后，即可利用π演算對(duì)每個(gè)邏輯服務(wù)原子和整個(gè)服務(wù)過(guò)程進(jìn)行建模，建模過(guò)程如下.

4.3 虛擬機(jī)部署中越權(quán)檢測(cè)與服務(wù)過(guò)程的不完整檢測(cè)

4.4 與現(xiàn)有安全檢測(cè)方法的對(duì)比

在云服務(wù)中，越權(quán)檢測(cè)與服務(wù)完整性檢測(cè)密不可分，越權(quán)的發(fā)生可能使服務(wù)中斷，導(dǎo)致服務(wù)不完整；而服務(wù)不完整會(huì)引發(fā)服務(wù)異常，增加越權(quán)的可能性.因此，需要對(duì)這兩種安全問(wèn)題同時(shí)檢測(cè).

表2通過(guò)對(duì)多種檢測(cè)方法的研究，給出了各種檢測(cè)方法的能力范圍.由表2可見(jiàn)，Bayes網(wǎng)檢測(cè)方法利用先驗(yàn)知識(shí)對(duì)可能入侵事件基于概率值分類(lèi)，只能針對(duì)預(yù)測(cè)出的服務(wù)過(guò)程入侵事件進(jìn)行檢測(cè)，未對(duì)系統(tǒng)提供的服務(wù)進(jìn)行預(yù)測(cè)，忽略了云服務(wù)過(guò)程不完整性帶來(lái)的安全問(wèn)題；預(yù)測(cè)規(guī)則集和時(shí)間序列學(xué)習(xí)方法都是基于已定義好的正常行為集合，分別利用時(shí)間推理和機(jī)器學(xué)習(xí)方法檢測(cè)試圖訓(xùn)練系統(tǒng)的入侵者，這兩種檢測(cè)方法雖然可保證用戶行為的合法性，但并未對(duì)系統(tǒng)行為進(jìn)行檢測(cè)，無(wú)法保證用戶請(qǐng)求得到響應(yīng)；TCG檢測(cè)方法通過(guò)一種平臺(tái)服務(wù)完整性檢測(cè)架構(gòu)，對(duì)平臺(tái)服務(wù)完整性進(jìn)行檢測(cè)，但該方法的檢測(cè)只是針對(duì)服務(wù)流程，忽略了用戶越權(quán)行為對(duì)服務(wù)過(guò)程的影響.而本文方法可同時(shí)檢測(cè)兩種安全問(wèn)題，相對(duì)于傳統(tǒng)方法有效減少了檢測(cè)計(jì)算量.

表2 檢測(cè)能力對(duì)比Table 2 Contrast of detection capability

［1］Ryan M D.Cloud Computing Seurity：The Scientific Challenge，and a Survey of Solutions［J］.Journal of Systems and Software，2013，86（9）：2263－2268.

［2］楊智君，田地，馬駿驍，等.入侵檢測(cè)技術(shù)研究綜述 ［J］.計(jì)算機(jī)工程與設(shè)計(jì)，2006，27（12）：2119－2123.（YANG Zhijun，TIAN Di，MA Junrao，et al.Survey of Intrusion Detection Technology ［J］.Computer Engineering and Design，2006，27（12）：2119－2123.）

［3］Kruegel C，Mutz D，Robertson W，et al.Bayesian Event Classification for Intrusion Detection［C］／／Proc of the 19th Annual Computer Security Applications Conference（ACSAC）.Washington DC：IEEE Computer Society，2003：14－23.

［4］Teng H S，Chen K，Lu S C Y.Security Audit Trail Analysis Using Inductively Generated Predictive Rules［C］／／Proceeding of the Sixth Conference on Artificial Intelligence Applications.Washington DC：IEEE Computer Society，1990：24－29.

［5］Lane T，Brodley C E.Temporal Sequence Learning and Data Reduction for Anomaly Detection ［J］.ACM Transactions on Information and System Security，1999，2（3）：295－331.

［6］Lee W，Stolfo S J，Chan P K，et al.Real Time Data Mining－Based Intrusion Detection［C］／／Proceedings of 2nd DARPA Information Survivability Conference and Exposition（DIsCEX）.Washington DC：IEEE Computer Society，2001：89－100.

［7］Sailer R，Zhang X，Jaeger T，et al.Design and lmplementation of a TCG－Based Integrity Measurement Architeclure［C］／／Proc of the 13rd USENIX Security Symposium.Berkeley：USENIX Association，2004：223－238.

［8］Clark D D，Wilson D R.A Comparison of Commercial and Military Computer Security Policies［C］／／Proc of the l987IEEE Symp on Security and Privacy.Washington DC：IEEE Computer Society，1987：184－194.

［9］蔣建春，馬恒太，任黨恩，等.網(wǎng)絡(luò)安全入侵檢測(cè)：研究綜述 ［J］.軟件學(xué)報(bào)，2000，11（11）：1460－1466.（JIANG Jianchun，MA Hengtai，REN Dang’en，et al.Network Security Intrusion Detection：The Review of the Research［J］.Journal of Software，2000，11（11）：1460－1466.）

［10］Milner R.Communicating and Mobile Systems：The Pi－Calculus［M］.Cambridge：Cambridge University Press，1999：77－159.

［11］廖軍，譚浩，劉錦德.基于Pi－演算的 Web服務(wù)組合的描述和驗(yàn)證 ［J］.計(jì)算機(jī)學(xué)報(bào)，2005，28（4）：635－643.（LIAO Jun，TAN Hao，LIU Jinde.Describing and Verifying Web Service Using Pi－Calculus［J］.Chinese Journal of Computers，2005，28（4）：635－643.）

［12］吳朱華.云計(jì)算核心技術(shù)剖析 ［M］.北京：人民郵電出版社，2011：2－30.（WU Zhuhua.Analysis of the Cloud Computing Core Technology［M］.Beijing：Post ＆ Telecom Press，2011：2－30.）

［13］郭小群，郝克剛.Web服務(wù)的 Pi演算描述 ［J］.計(jì)算機(jī)科學(xué)，2006，33（3）：261－262.（GUO Xiaoqun，HAO Kegang.Pi Calculi－Based Model for Web Services［J］.Computerscience，2006，33（3）：261－262.）