支持模型檢測的云計算隱私建模方法研究.pdf

1、可伸縮性，按需付費以及基于網(wǎng)絡(luò)的消息傳遞是云計算的三個核心特征。云計算強調(diào)一切皆服務(wù)。基礎(chǔ)設(shè)施層、平臺層以及面向最終用戶的軟件層都被包裝為不同形式的服務(wù)，并通過不同的交互方式和數(shù)據(jù)協(xié)議完成協(xié)作。這種分層可伸縮的協(xié)作方式為云計算使用者帶來了極大的便利，如:減輕了數(shù)據(jù)存儲管理的負(fù)擔(dān)，具備了與地理位置無關(guān)的數(shù)據(jù)訪問能力，避免了硬件、軟件等方面的投資損失等。但與此同時，云計算服務(wù)提供者(Cloud Service Provider)的中間操作過

2、程對用戶透明，用戶將喪失對其數(shù)據(jù)的部分控制權(quán)，進而引發(fā)了用戶對云計算安全與隱私保護的擔(dān)憂。
　　云計算環(huán)境下最終應(yīng)用是一系列服務(wù)的有機聚合。這種聚合，既包括了Web服務(wù)組合方式下通過結(jié)構(gòu)化活動對原子服務(wù)的編排與編制，也包含了高層服務(wù)與底層服務(wù)之間的依賴關(guān)系。且云計算應(yīng)用中所涉及的服務(wù)往往由不同服務(wù)提供商提供，具備跨機構(gòu)特性，而即使同一服務(wù)提供商內(nèi)部的服務(wù)也存在著數(shù)據(jù)與平臺的異構(gòu)。這種以服務(wù)聚合為基礎(chǔ)的應(yīng)用形態(tài)，使傳統(tǒng)隱私保護方法面

3、臨了新的挑戰(zhàn)。最終用戶的隱私需求往往直接與服務(wù)聚合的結(jié)構(gòu)，行為以及參與方相關(guān)，而隱私收集與使用目的、暴露方式、保持時間等屬性更與應(yīng)用業(yè)務(wù)邏輯直接關(guān)聯(lián)，無法通過單一針對數(shù)據(jù)的加密與檢驗完成。同時，不同服務(wù)提供商難以引入統(tǒng)一的數(shù)據(jù)保護策略，單一提供商無法強制其他參與方采用相同的數(shù)據(jù)加密與保護方案，因此難以通過加密和訪問控制等傳統(tǒng)手段保證多參與方的應(yīng)用中隱私不出現(xiàn)泄露。
　　為了應(yīng)對這一挑戰(zhàn)，最新的隱私保護規(guī)范都將“提供可驗證的方式，確

4、保軟件的實現(xiàn)滿足對應(yīng)的隱私需求”列為隱私保護需要滿足的最重要原則之一。目前針對云計算環(huán)境下隱私需求的驗證在國內(nèi)外都尚處于起步階段，本課題針對這一問題，從支持模型檢測的隱私建模方面開展工作，分別對云計算環(huán)境下隱私需求的建模方法和云計算系統(tǒng)中靜態(tài)服務(wù)和動態(tài)服務(wù)的隱私建模方法進行了研究。主要的研究工作包括：
　?。?）提出了隱私活動的元模型以及基于此元模型的隱私需求建模和系統(tǒng)隱私建?？蚣?。支持模型檢測的模型要求系統(tǒng)模型和需求模型都基于語

5、義相同的原子命題集合。本文所提出的隱私活動元模型，系統(tǒng)歸納并精化了目前被采納的隱私保護規(guī)范中的核心概念，并進一步分析了這些概念元素之間的關(guān)系，給出了其精確的形式語義。在此基礎(chǔ)上，討論了基于隱私活動元模型的隱私需求建模和系統(tǒng)隱私建模的框架。本研究后續(xù)工作都圍繞此元模型及相關(guān)框架展開。
　　（2）在隱私需求的建模方面。提出了一種聲明式隱私需求描述語言(DPPL)，該語言不僅考慮了數(shù)據(jù)、角色和目的的層次結(jié)構(gòu)，而且通過定義可擴展的聲明式約

6、束模板提供了時序約束的表達能力。在此基礎(chǔ)上，分析了隱私活動包含關(guān)系對最終建模結(jié)果的影響，給出了針對該語言定義的隱私需求的形式化建模算法?？紤]到傳統(tǒng)形式化驗證由于空間爆炸而帶來的實用性限制，進一步結(jié)合隱私活動的特征提出了隱私需求模型的約簡方法。最后，通過實例分析和仿真檢驗了本研究所提出方法的可行性。
　?。?）在云計算靜態(tài)服務(wù)的隱私建模方面。針對SOAP/WS-*服務(wù)及其業(yè)務(wù)流程執(zhí)行語言BPEL流程的隱私建模開展了研究。首先，對于服

7、務(wù)組合流程中 SOAP/WS-*原子活動中包含的隱私數(shù)據(jù)進行了建模分析。其次，提出了一種擴展內(nèi)部變遷的遷移系統(tǒng)，用以將BPEL里所有可能牽涉隱私活動的變量訪問，謂詞表達式等都建模為獨立的變遷。之后，針對此變遷系統(tǒng)中的每一個變遷進行轉(zhuǎn)換，從數(shù)據(jù)、目的、參與方和謂詞約束4個方面入手，將原有的變遷轉(zhuǎn)換為可能的隱私活動，從而建立起面向隱私活動的BPEL模型。最后，通過案例分析和仿真實驗對該方法所建立的模型和原有的BPEL建模結(jié)果在狀態(tài)空間方面進

8、行了比較，以確保該方法的建模結(jié)果不會加劇狀態(tài)空間爆炸。
　?。?）在云計算動態(tài)服務(wù)的隱私建模方面。針對云計算動態(tài)服務(wù)的典型代表——Restful服務(wù)的應(yīng)用狀態(tài)開展隱私建模研究?？紤]到由于超媒體作為應(yīng)用引擎特征而引發(fā)的服務(wù)內(nèi)部變遷，提出了一種Restful服務(wù)應(yīng)用狀態(tài)的隱私模型并研究了從Restful服務(wù)描述向此模型的自動轉(zhuǎn)換方法。在該模型中，不僅利用隱私活動的元模型確保了隱私操作的精確刻畫，同時形式化定義了 Restful服務(wù)資源