面向行為可信的大數據安全系統形式化描述*

閆 智，詹 靜,2,3

（1.北京工業大學計算機學院 北京100124；2.可信計算北京市重點實驗室 北京100124；3.信息安全等級保護關鍵技術國家工程實驗室 北京100124）

1 引言

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

由于云計算的服務模式是數據外包，數據的所有權轉移給了CSP，云中存儲的大數據通常是明文的，一旦CSP擁有數據的使用權，惡意的CSP可能會竊取用戶數據，云平臺亦可能受到黑客攻擊致使安全機制失效或被非法控制，從而導致非授權人讀取數據，給大數據安全帶來了威脅。因此要保障在云端應用Hadoop處理大數據的安全，應從行為角度控制對數據的非法使用。

2 研究背景及相關工作

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

國內相關研究[2]通過密碼技術改善Hadoop的安全問題。使用基于公鑰體制的身份認證，并采用了數字信封技術對傳輸數據進行加密，同時對存儲在云端的數據也進行加密存儲。但該方案在數據運算過程中仍然需要解密，在增加系統運算復雜性的同時也會產生安全問題。

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

Sedic系統[4]通過對數據添加標簽，使用字符串掃描器搜索預定義的敏感數據集，依據數據安全等級自動分離MapReduce的計算任務，在私有云中進行敏感數據的計算，在公有云中進行其他部分的計算，以此保護MapReduce中的數據安全。該系統有效防范了公有云的控制者對隱私數據的獲取。由于加入大數拆分步驟，增加了數據處理的復雜度。

Samir Saklikar在2012年RSA信息安全大會上提出了MapReduce需要內嵌安全和可信基[5]。對MapReduce提出了內省架構實施可擴展的動態訪問控制。他認為需要對數據進行細粒度的訪問控制，在訪問控制決策執行點構建基于內容的訪問控制。在策略執行點部署基于內容的訪問控制請求、MapReduce任務分析、訪問控制策略。該方案通過安全內省機制有效控制了MapReduce中不滿足安全策略的行為請求的執行。該方案當前只是提出一種設想，并未真正實現。

本文以Hadoop平臺為研究背景，從行為角度描述云計算中大數據行為模型，定義可信行為與惡意行為，通過控制惡意行為的執行，保障大數據服務安全。

3 行為模型定義

對于云計算中的行為操作，定義為兩類：一類行為是合法的，例如數據擁有者對數據的處理，CSP對用戶數據的正常維護等，這類行為稱為可信行為；另一類行為是非法的，例如沒有操作權限的用戶對文件的讀取，CSP對文件的不徹底刪除等，定義為惡意行為。為了給出行為模型，需要使用通用的形式化方法描述行為，用軟件形式規格說明語言——Z語言[6,7]對行為模型進行定義。這種基于模型的形式方法也被稱為基于狀態的形式方法，其基本的思想是利用已知特性的數學抽象來為目標系統的狀態特征和行為特征構造模型。Z形式化方法的優點在于它基于一階謂詞邏輯和集合論，具有嚴格的數學基礎和描述特性，相對于自然語言具有精確無歧義性。利用Z語言書寫規格說明，可以提高工程質量，更有利于團隊設計和實現代碼[8]，同時為編寫和驗證計算機程序的正確性提供了依據。

3.1 狀態模式

云計算中存在兩類實體，主體為用戶，客體為資源，用戶Person與資源Resource存在關系映射。用戶Person涉及4類人，owner對應數據擁有者、user對應數據使用者、computer對應數據計算者、CSP對應云服務提供商。操作的資源按照粒度粗細可以劃分為文件系統filesystem和文件file。

一個用戶可以對多個資源進行操作，一個資源同樣可以被多個用戶使用。這里的關系是一個多對多的映射。具體的資源內容可以通過抽象資源與具體內容的映射來表示，這種映射是一對一的，因為每個資源只能指向其相應的資源內容，這種關系可以用部分入射函數表示。綜上可以定義Cloud中的集合類型為[Person,Resource,Content]。在Hadoop中，為了保障服務可靠性，對原始數據在不同節點進行了備份，資源具有相同的屬主及內容，將Resource定義為包類型（Z形式語言中一種特有的類型，是一種無序、可重復的數據集合類型），允許資源具有重復內容。引入模式對Cloud進行進一步描述。Cloud狀態模式定義如下：

當對云計算進行初始化時，不存在用戶以及資源，所以behavior、match和copies關系均為空集。

對于改變了behavior和match關系的任意操作的模式為：

如果云計算中的某些操作行為不會引起云計算狀態的任何改變，把該模式定義為：

3.2 操作模式

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

表1 抽象云計算操作

下面分別給出每一個操作的完整規格說明。

3.2.1 Read：讀取操作

在定義的系統中可信行為是可以執行的，這里DoRead是可信行為模型：

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

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

Action∷=allow|deny

成功操作模式定義為：

給出Read操作的前置條件，見表2。

表2 Read操作前置條件

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

3.2.2 Update：更新操作

與Read操作類似，DoUpdate為可信行為，IllegalPerson和NotAuthorized操作為不可信行為，不再分別描述，直接給出Update操作的完整規格說明：Update堞DoUpdate∨IllegalPerson∨NotAuthorized，Update操作的前置條件見表3。

表3 Update操作前置條件

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

在Update中DoUpdate對兩類資源進行修改，behavior′=behavior茌{p?r?}指的是對權限資源的更改，而match′=match茌{r?c?}指的是對數據資源的更改。

3.2.3 Add：添加操作

用相同的方法定義Add操作模式，Add操作的完整規格說明為：

Add堞DoAdd∨IllegalPerson∨MaxCopies

Add操作的前置條件見表4。

表4 Add操作前置條件

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

3.2.4 Delete：刪除操作

Delete操作的完整規格說明為：Delete堞DoDelete∨IllegalPerson∨NotAuthorized，Delete操作的前置條件見表5。

表5 Delete操作前置條件

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

4 行為模型證明

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

5 安全性分析

基于云的大數據安全風險的根本在于，云計算是一種委托計算，即他人委托云平臺、遠程完成的計算。資源所有權被轉移，因此可能存在不可信但具有底層控制權的實體對未授權文件的惡意讀取。網上曾披露政府部門通過云服務提供商來獲取數據，就是因為云端確實存在未授權人員對數據的非法訪問。Microsoft、Google和Facebook等均 收到過外國情報監控法庭對用戶數據的請求。云服務商或政府部門等未授權者對數據的非法訪問、分析均會導致隱私泄露。而Hadoop的自身安全機制薄弱以及明文存儲、處理數據加深了安全風險。

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

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

（2）對于Update操作，惡意行為為IllegalPerson和NotAuthorized，與Read操作類似，這里不再贅述。

（3）對于Delete操作，DoDelete定義為可信行為，因為模式中對3個關系的定義域或值域的限定減操作要求對原始數據及備份數據進行徹底刪除。然而云計算服務商可能并未真正徹底刪除所有備份數據，因此存在FileNotClear不可信行為。在模式中體現為刪除時，并未對Resource包中對應資源的所有副本進行刪除，copies′≠copies{r?maxcopies}，進行刪除操作后，Resource包中仍含有被刪除資源與數量的映射#({r?}茳copies′)≠0。IllegalPerson和NotAuthorized與上述內容類似。

（4）Add操作中，除IllegalPerson外，惡意行為還包括MaxCopies操作。因為對于存儲在Hadoop中的文件，不允許文件副本數多于用戶通過setrep設定的備份數量，以此防止對文件的非法復制。

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

6 結束語

本文通過分析大數據在云計算中的應用可能引起的安全問題，提出了云端大數據行為模型，劃分了可信行為與惡意行為，并提出了防止不可信行為執行，保障大數據服務安全的相關方法。該模型以數學理論為基礎，通過形式化描述，精確定義出該系統的狀態模式及操作模式，為后期安全策略的提出奠定了理論基礎，從而指導實際系統的安全設計。接下來將在增加模型描述粒度，完善行為模型，建立相關安全策略方面進行進一步研究。

1 周品.Hadoop云計算實戰.北京:清華大學出版社,2012

2 馬媛.基于Hadoop的云計算平臺安全機制研究.信息安全與保密通信,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 廖淮扣，陳怡海.軟件形式規格說明語言-Z.北京:清華大學出版社,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