面向行為可信的大數(shù)據(jù)安全系統(tǒng)形式化描述*

閆 智，詹 靜,2,3

（1.北京工業(yè)大學(xué)計(jì)算機(jī)學(xué)院 北京100124；2.可信計(jì)算北京市重點(diǎn)實(shí)驗(yàn)室 北京100124；3.信息安全等級(jí)保護(hù)關(guān)鍵技術(shù)國(guó)家工程實(shí)驗(yàn)室 北京100124）

1 引言

隨著各個(gè)領(lǐng)域數(shù)據(jù)生成速度的加快，需要處理的數(shù)據(jù)量急劇膨脹。有效地分析和利用這些龐大的數(shù)據(jù)資源能夠帶來(lái)巨大的價(jià)值。利用傳統(tǒng)存儲(chǔ)和分析工具對(duì)內(nèi)容龐大、種類(lèi)繁多的大數(shù)據(jù)進(jìn)行處理已經(jīng)不能滿(mǎn)足其要求。Hadoop提供了一個(gè)可靠的大數(shù)據(jù)共享存儲(chǔ)和分析系統(tǒng)[1]。它是由開(kāi)源組織Apache在Google云計(jì)算的map/reduce和GFS（Google file system，Google文件系統(tǒng)）思想啟發(fā)下開(kāi)發(fā)出的計(jì)算框架，并成功應(yīng)用到諸如亞馬遜、Yahoo、Facebook等公司的應(yīng)用中。而CSP（cloud service provider，云計(jì)算服務(wù)提供商）擁有大數(shù)據(jù)存儲(chǔ)能力和計(jì)算資源，因此往往通過(guò)云計(jì)算平臺(tái)對(duì)大數(shù)據(jù)進(jìn)行處理。目前許多組織選擇在租賃硬件所搭建的云端運(yùn)行Hadoop或提供Hadoop服務(wù)。例如Cloudera提供在公共（或私有）云端運(yùn)行Hadoop的工具；Amazon提供Hadoop云服務(wù)，名為Elastic MapReduce。

由于云計(jì)算的服務(wù)模式是數(shù)據(jù)外包，數(shù)據(jù)的所有權(quán)轉(zhuǎn)移給了CSP，云中存儲(chǔ)的大數(shù)據(jù)通常是明文的，一旦CSP擁有數(shù)據(jù)的使用權(quán)，惡意的CSP可能會(huì)竊取用戶(hù)數(shù)據(jù)，云平臺(tái)亦可能受到黑客攻擊致使安全機(jī)制失效或被非法控制，從而導(dǎo)致非授權(quán)人讀取數(shù)據(jù)，給大數(shù)據(jù)安全帶來(lái)了威脅。因此要保障在云端應(yīng)用Hadoop處理大數(shù)據(jù)的安全，應(yīng)從行為角度控制對(duì)數(shù)據(jù)的非法使用。

2 研究背景及相關(guān)工作

Hadoop是當(dāng)前最廣為人知的大數(shù)據(jù)技術(shù)實(shí)施方案。它在設(shè)計(jì)之初并未考慮過(guò)安全問(wèn)題，在Hadoop 1.0.0或者CDH3版本之后，Hadoop在安全方面加入了基于Kerberos的身份認(rèn)證機(jī)制和基于ACL的訪問(wèn)控制機(jī)制。然而Kerberos的認(rèn)證機(jī)制只是針對(duì)機(jī)器級(jí)別的安全認(rèn)證，并未對(duì)Hadoop平臺(tái)本身進(jìn)行認(rèn)證[2]。而基于ACL的訪問(wèn)控制雖然限制了用戶(hù)與組成員對(duì)Hadoop中資源的訪問(wèn)或節(jié)點(diǎn)間的通信，但該機(jī)制依賴(lài)于管理員對(duì)hadoop-policy.xml中訪問(wèn)列表的配置，這種基于傳統(tǒng)的訪問(wèn)控制列表容易在服務(wù)器端被篡改而不易察覺(jué)。況且對(duì)于企業(yè)，訪問(wèn)控制列表需要經(jīng)常被更新，操作過(guò)于繁瑣且不易維護(hù)。因此Hadoop自身的安全機(jī)制是不完善的。

國(guó)內(nèi)相關(guān)研究[2]通過(guò)密碼技術(shù)改善Hadoop的安全問(wèn)題。使用基于公鑰體制的身份認(rèn)證，并采用了數(shù)字信封技術(shù)對(duì)傳輸數(shù)據(jù)進(jìn)行加密，同時(shí)對(duì)存儲(chǔ)在云端的數(shù)據(jù)也進(jìn)行加密存儲(chǔ)。但該方案在數(shù)據(jù)運(yùn)算過(guò)程中仍然需要解密，在增加系統(tǒng)運(yùn)算復(fù)雜性的同時(shí)也會(huì)產(chǎn)生安全問(wèn)題。

Indrajit Roy等人提出了基于強(qiáng)制訪問(wèn)控制和差分隱私技術(shù)的Airavat系統(tǒng)[3]。該系統(tǒng)解決了在某種場(chǎng)景下MapReduce的安全問(wèn)題，在該場(chǎng)景中計(jì)算程序提供者希望借助數(shù)據(jù)擁有者的數(shù)據(jù)做相關(guān)研究，這里假設(shè)程序提供者寫(xiě)的mapper函數(shù)不安全，可能會(huì)對(duì)敏感字段進(jìn)行輸出。Airavat系統(tǒng)通過(guò)限制網(wǎng)絡(luò)向外發(fā)送中間數(shù)據(jù)，并將標(biāo)簽附在輸入、輸出和中間數(shù)據(jù)上用于訪問(wèn)控制，還預(yù)定義mapper函數(shù)的輸出范圍來(lái)保障數(shù)據(jù)安全。因此Airavat系統(tǒng)保障了在對(duì)敏感數(shù)據(jù)執(zhí)行不受信任的代碼進(jìn)行數(shù)據(jù)集的一般特性或綜合特性計(jì)算的情況下的安全。這里主要保障了MapReduce中map步驟的安全。然而該系統(tǒng)并沒(méi)有對(duì)存儲(chǔ)在HDFS中的所有數(shù)據(jù)進(jìn)行保護(hù)，還需要在更底層對(duì)信息流進(jìn)行進(jìn)一步的保護(hù)。

Sedic系統(tǒng)[4]通過(guò)對(duì)數(shù)據(jù)添加標(biāo)簽，使用字符串掃描器搜索預(yù)定義的敏感數(shù)據(jù)集，依據(jù)數(shù)據(jù)安全等級(jí)自動(dòng)分離MapReduce的計(jì)算任務(wù)，在私有云中進(jìn)行敏感數(shù)據(jù)的計(jì)算，在公有云中進(jìn)行其他部分的計(jì)算，以此保護(hù)MapReduce中的數(shù)據(jù)安全。該系統(tǒng)有效防范了公有云的控制者對(duì)隱私數(shù)據(jù)的獲取。由于加入大數(shù)拆分步驟，增加了數(shù)據(jù)處理的復(fù)雜度。

Samir Saklikar在2012年RSA信息安全大會(huì)上提出了MapReduce需要內(nèi)嵌安全和可信基[5]。對(duì)MapReduce提出了內(nèi)省架構(gòu)實(shí)施可擴(kuò)展的動(dòng)態(tài)訪問(wèn)控制。他認(rèn)為需要對(duì)數(shù)據(jù)進(jìn)行細(xì)粒度的訪問(wèn)控制，在訪問(wèn)控制決策執(zhí)行點(diǎn)構(gòu)建基于內(nèi)容的訪問(wèn)控制。在策略執(zhí)行點(diǎn)部署基于內(nèi)容的訪問(wèn)控制請(qǐng)求、MapReduce任務(wù)分析、訪問(wèn)控制策略。該方案通過(guò)安全內(nèi)省機(jī)制有效控制了MapReduce中不滿(mǎn)足安全策略的行為請(qǐng)求的執(zhí)行。該方案當(dāng)前只是提出一種設(shè)想，并未真正實(shí)現(xiàn)。

本文以Hadoop平臺(tái)為研究背景，從行為角度描述云計(jì)算中大數(shù)據(jù)行為模型，定義可信行為與惡意行為，通過(guò)控制惡意行為的執(zhí)行，保障大數(shù)據(jù)服務(wù)安全。

3 行為模型定義

對(duì)于云計(jì)算中的行為操作，定義為兩類(lèi)：一類(lèi)行為是合法的，例如數(shù)據(jù)擁有者對(duì)數(shù)據(jù)的處理，CSP對(duì)用戶(hù)數(shù)據(jù)的正常維護(hù)等，這類(lèi)行為稱(chēng)為可信行為；另一類(lèi)行為是非法的，例如沒(méi)有操作權(quán)限的用戶(hù)對(duì)文件的讀取，CSP對(duì)文件的不徹底刪除等，定義為惡意行為。為了給出行為模型，需要使用通用的形式化方法描述行為，用軟件形式規(guī)格說(shuō)明語(yǔ)言——Z語(yǔ)言[6,7]對(duì)行為模型進(jìn)行定義。這種基于模型的形式方法也被稱(chēng)為基于狀態(tài)的形式方法，其基本的思想是利用已知特性的數(shù)學(xué)抽象來(lái)為目標(biāo)系統(tǒng)的狀態(tài)特征和行為特征構(gòu)造模型。Z形式化方法的優(yōu)點(diǎn)在于它基于一階謂詞邏輯和集合論，具有嚴(yán)格的數(shù)學(xué)基礎(chǔ)和描述特性，相對(duì)于自然語(yǔ)言具有精確無(wú)歧義性。利用Z語(yǔ)言書(shū)寫(xiě)規(guī)格說(shuō)明，可以提高工程質(zhì)量，更有利于團(tuán)隊(duì)設(shè)計(jì)和實(shí)現(xiàn)代碼[8]，同時(shí)為編寫(xiě)和驗(yàn)證計(jì)算機(jī)程序的正確性提供了依據(jù)。

3.1 狀態(tài)模式

云計(jì)算中存在兩類(lèi)實(shí)體，主體為用戶(hù)，客體為資源，用戶(hù)Person與資源Resource存在關(guān)系映射。用戶(hù)Person涉及4類(lèi)人，owner對(duì)應(yīng)數(shù)據(jù)擁有者、user對(duì)應(yīng)數(shù)據(jù)使用者、computer對(duì)應(yīng)數(shù)據(jù)計(jì)算者、CSP對(duì)應(yīng)云服務(wù)提供商。操作的資源按照粒度粗細(xì)可以劃分為文件系統(tǒng)filesystem和文件file。

一個(gè)用戶(hù)可以對(duì)多個(gè)資源進(jìn)行操作，一個(gè)資源同樣可以被多個(gè)用戶(hù)使用。這里的關(guān)系是一個(gè)多對(duì)多的映射。具體的資源內(nèi)容可以通過(guò)抽象資源與具體內(nèi)容的映射來(lái)表示，這種映射是一對(duì)一的，因?yàn)槊總€(gè)資源只能指向其相應(yīng)的資源內(nèi)容，這種關(guān)系可以用部分入射函數(shù)表示。綜上可以定義Cloud中的集合類(lèi)型為[Person,Resource,Content]。在Hadoop中，為了保障服務(wù)可靠性，對(duì)原始數(shù)據(jù)在不同節(jié)點(diǎn)進(jìn)行了備份，資源具有相同的屬主及內(nèi)容，將Resource定義為包類(lèi)型（Z形式語(yǔ)言中一種特有的類(lèi)型，是一種無(wú)序、可重復(fù)的數(shù)據(jù)集合類(lèi)型），允許資源具有重復(fù)內(nèi)容。引入模式對(duì)Cloud進(jìn)行進(jìn)一步描述。Cloud狀態(tài)模式定義如下：

當(dāng)對(duì)云計(jì)算進(jìn)行初始化時(shí)，不存在用戶(hù)以及資源，所以behavior、match和copies關(guān)系均為空集。

對(duì)于改變了behavior和match關(guān)系的任意操作的模式為：

如果云計(jì)算中的某些操作行為不會(huì)引起云計(jì)算狀態(tài)的任何改變，把該模式定義為：

3.2 操作模式

狀態(tài)模式定義完成之后，定義操作模式。Hadoop中對(duì)資源的操作包括讀、寫(xiě)和修改。HDFS設(shè)計(jì)之初并不支持對(duì)文件內(nèi)容的追加，從HDFS 2.x開(kāi)始支持對(duì)文件追加。因此這里的修改操作指的是對(duì)內(nèi)容的追加以及權(quán)限的修改。操作的資源分為兩類(lèi)：數(shù)據(jù)資源以及權(quán)限資源，這里數(shù)據(jù)資源又分為兩級(jí)（文件系統(tǒng)級(jí)、文件級(jí)）。將行為抽象合并為4類(lèi)，讀?。≧ead）、更新（Update）、添加（Add）、刪除（Delete）。Read對(duì)應(yīng)所有需要顯示的操作，包括文件系統(tǒng)大小、數(shù)量的顯示，文件目錄的顯示，文件內(nèi)容的顯示等；Update對(duì)應(yīng)修改操作，包括數(shù)據(jù)資源及權(quán)限資源的修改；Add操作包括文件的備份及文件的上傳等，對(duì)應(yīng)的是文件級(jí)資源；Delete也是對(duì)文件級(jí)資源的操作。將Hadoop中所有操作指令[9]對(duì)應(yīng)到抽象行為中，具體見(jiàn)表1。而類(lèi)似mv（移動(dòng)資源到其他位置）的這種操作可以看作Delete與Add操作的組合。

表1 抽象云計(jì)算操作

下面分別給出每一個(gè)操作的完整規(guī)格說(shuō)明。

3.2.1 Read：讀取操作

在定義的系統(tǒng)中可信行為是可以執(zhí)行的，這里DoRead是可信行為模型：

對(duì)于可信行為，給出成功提示信息，對(duì)于惡意行為，需要中止并給出出錯(cuò)提示信息。因此需要擴(kuò)展提示信息并引入操作結(jié)果判定，包括允許執(zhí)行及拒絕執(zhí)行。定義如下：

Report∷=Success|Illegal_Person|Not_Authorized|Reach_Max_Copies|File_Not_Clear

Action∷=allow|deny

成功操作模式定義為：

給出Read操作的前置條件，見(jiàn)表2。

表2 Read操作前置條件

根據(jù)前置條件，Read操作完整規(guī)格說(shuō)明可以定義為：Read堞DoRead∨IllegalPerson∨NotAuthorized，垂直形式的模式為：

3.2.2 Update：更新操作

與Read操作類(lèi)似，DoUpdate為可信行為，IllegalPerson和NotAuthorized操作為不可信行為，不再分別描述，直接給出Update操作的完整規(guī)格說(shuō)明：Update堞DoUpdate∨IllegalPerson∨NotAuthorized，Update操作的前置條件見(jiàn)表3。

表3 Update操作前置條件

根據(jù)前置條件，Update垂直形式的操作模式為：

在Update中DoUpdate對(duì)兩類(lèi)資源進(jìn)行修改，behavior′=behavior茌{p?r?}指的是對(duì)權(quán)限資源的更改，而match′=match茌{r?c?}指的是對(duì)數(shù)據(jù)資源的更改。

3.2.3 Add：添加操作

用相同的方法定義Add操作模式，Add操作的完整規(guī)格說(shuō)明為：

Add堞DoAdd∨IllegalPerson∨MaxCopies

Add操作的前置條件見(jiàn)表4。

表4 Add操作前置條件

依據(jù)前置條件，給出Add垂直形式的操作模式為：

3.2.4 Delete：刪除操作

Delete操作的完整規(guī)格說(shuō)明為：Delete堞DoDelete∨IllegalPerson∨NotAuthorized，Delete操作的前置條件見(jiàn)表5。

表5 Delete操作前置條件

Delete操作垂直形式的模式為：

4 行為模型證明

Z/EVES[10,11]是加拿大ORA公司開(kāi)發(fā)的一個(gè)Z支持工具，它具有規(guī)格說(shuō)明編輯、語(yǔ)法和類(lèi)型檢查、定義域檢查和定理證明等功能。通過(guò)使用Z/EVES工具，驗(yàn)證了所有定義的模式的正確性。驗(yàn)證界面如圖1所示，左側(cè)Syntax列下顯示字母Y，表示段落已被檢查且無(wú)類(lèi)型和語(yǔ)法錯(cuò)誤；Proof列下顯示字母Y，表示右側(cè)的模式已被證明。

5 安全性分析

基于云的大數(shù)據(jù)安全風(fēng)險(xiǎn)的根本在于，云計(jì)算是一種委托計(jì)算，即他人委托云平臺(tái)、遠(yuǎn)程完成的計(jì)算。資源所有權(quán)被轉(zhuǎn)移，因此可能存在不可信但具有底層控制權(quán)的實(shí)體對(duì)未授權(quán)文件的惡意讀取。網(wǎng)上曾披露政府部門(mén)通過(guò)云服務(wù)提供商來(lái)獲取數(shù)據(jù)，就是因?yàn)樵贫舜_實(shí)存在未授權(quán)人員對(duì)數(shù)據(jù)的非法訪問(wèn)。Microsoft、Google和Facebook等均 收到過(guò)外國(guó)情報(bào)監(jiān)控法庭對(duì)用戶(hù)數(shù)據(jù)的請(qǐng)求。云服務(wù)商或政府部門(mén)等未授權(quán)者對(duì)數(shù)據(jù)的非法訪問(wèn)、分析均會(huì)導(dǎo)致隱私泄露。而Hadoop的自身安全機(jī)制薄弱以及明文存儲(chǔ)、處理數(shù)據(jù)加深了安全風(fēng)險(xiǎn)。

根據(jù)對(duì)上述模型中4種操作模式的安全分析，可以得到4種不可信行為。

（1）對(duì)于Read操作，DoRead為合法行為，只有用戶(hù)歸屬于Person類(lèi)，即屬于云用戶(hù)，并且對(duì)請(qǐng)求的資源具有權(quán)限的情況下可以執(zhí)行。IllegalPerson和NotAuthorized為不可信行為。IllegalPerson操作指的是云服務(wù)商創(chuàng)建的未授權(quán)用戶(hù)、政府人員或者由于安全機(jī)制失效而引入的黑客等對(duì)資源的惡意讀取。這類(lèi)人員不歸屬Person類(lèi)，所以請(qǐng)求被拒絕執(zhí)行。NotAuthorized操作針對(duì)的是歸屬于Person類(lèi)的人員，其擁有對(duì)云中部分資源的操作權(quán)，但是卻越權(quán)訪問(wèn)其他數(shù)據(jù)。

（2）對(duì)于Update操作，惡意行為為IllegalPerson和NotAuthorized，與Read操作類(lèi)似，這里不再贅述。

（3）對(duì)于Delete操作，DoDelete定義為可信行為，因?yàn)槟Ｊ街袑?duì)3個(gè)關(guān)系的定義域或值域的限定減操作要求對(duì)原始數(shù)據(jù)及備份數(shù)據(jù)進(jìn)行徹底刪除。然而云計(jì)算服務(wù)商可能并未真正徹底刪除所有備份數(shù)據(jù)，因此存在FileNotClear不可信行為。在模式中體現(xiàn)為刪除時(shí)，并未對(duì)Resource包中對(duì)應(yīng)資源的所有副本進(jìn)行刪除，copies′≠copies{r?maxcopies}，進(jìn)行刪除操作后，Resource包中仍含有被刪除資源與數(shù)量的映射#({r?}茳c(diǎn)opies′)≠0。IllegalPerson和NotAuthorized與上述內(nèi)容類(lèi)似。

（4）Add操作中，除IllegalPerson外，惡意行為還包括MaxCopies操作。因?yàn)閷?duì)于存儲(chǔ)在Hadoop中的文件，不允許文件副本數(shù)多于用戶(hù)通過(guò)setrep設(shè)定的備份數(shù)量，以此防止對(duì)文件的非法復(fù)制。

對(duì)于上述安全威脅，可以針對(duì)提出的行為模型描述的惡意行為實(shí)施相應(yīng)安全機(jī)制。例如，針對(duì)IllegalPerson和NotAuthorized不可信行為問(wèn)題，應(yīng)對(duì)大數(shù)據(jù)應(yīng)用平臺(tái)增加監(jiān)控機(jī)制，監(jiān)控機(jī)制可以利用LSM（Linux security module，Linux安全模塊），依據(jù)行為模型設(shè)定訪問(wèn)控制策略，插入鉤子函數(shù)，控制底層信息的訪問(wèn)，對(duì)可信行為予以通過(guò)，對(duì)惡意行為進(jìn)行終止，遏制CSP及非法人員的惡意操作。針對(duì)MaxCopies和FileNotClear不可信行為問(wèn)題，可以通過(guò)加密機(jī)制，對(duì)文件內(nèi)容進(jìn)行加密，保障內(nèi)容的機(jī)密性，即使文件被非法復(fù)制或保留，也不能獲取有價(jià)值的文件內(nèi)容。

6 結(jié)束語(yǔ)

本文通過(guò)分析大數(shù)據(jù)在云計(jì)算中的應(yīng)用可能引起的安全問(wèn)題，提出了云端大數(shù)據(jù)行為模型，劃分了可信行為與惡意行為，并提出了防止不可信行為執(zhí)行，保障大數(shù)據(jù)服務(wù)安全的相關(guān)方法。該模型以數(shù)學(xué)理論為基礎(chǔ)，通過(guò)形式化描述，精確定義出該系統(tǒng)的狀態(tài)模式及操作模式，為后期安全策略的提出奠定了理論基礎(chǔ)，從而指導(dǎo)實(shí)際系統(tǒng)的安全設(shè)計(jì)。接下來(lái)將在增加模型描述粒度，完善行為模型，建立相關(guān)安全策略方面進(jìn)行進(jìn)一步研究。

1 周品.Hadoop云計(jì)算實(shí)戰(zhàn).北京:清華大學(xué)出版社,2012

2 馬媛.基于Hadoop的云計(jì)算平臺(tái)安全機(jī)制研究.信息安全與保密通信,2012(6):89～92

3 Roy I,Setty S T V,Kilzer A,et al.Airavat:security and privacy for MapReduce.Proceedings of the 7th USENIX Symposium on Networked Systems Design and Implementation,San Jose,CA,USA,2010

4 Zhang K H,Zhou X Y,Chen Y Y,et al.Sedic:privacy-aware data intensive computing on hybrid clouds.Proceedings of the 18th ACM Conference on Computer and Communications Security,Chicago,Illinois,USA,2011

5 Saklikar S.Embedding security and trust primitives within MapReduce.http://www.emc-china.com/rsaconference/2012/en/download.php?pdf_file=TC-2003_EN.pdf,2012

6 廖淮扣，陳怡海.軟件形式規(guī)格說(shuō)明語(yǔ)言-Z.北京:清華大學(xué)出版社,2012

7 Spivey J M.The Z notation:a reference manual.Second Edition.UK:Prentice Hall International(UK)Ltd,1998

8 Hasson P,Cooper S.A case study involving the use of Z to aid requirements specification in the software engineering course.Proceedings of the 17th Conference on Software Engineering Education and Training,Norfolk,Virginia,USA,2004

9 Lam C.Hadoop in Action.韓冀中譯.北京:人民郵電出版社,2011

10 Saaltink M.The Z/EVES system.Proceedings of the 10th International Conference of Z Users on the Z Formal Specification Notation,London,UK,1997

11 Meisels I.Software manual for Windows Z/EVES Version 2.1.http://www.docin.com/p-147668972.html,2000