王 進 黃志球

(南京航空航天大學(xué)計算機科學(xué)與技術(shù)學(xué)院 南京 210016)

(woodenwang55@hotmail.com)

泛在服務(wù)(X as a service, XaaS)將互聯(lián)網(wǎng)生態(tài)圈中的軟件、物理資源和人廣泛連接，并通過特定的交互方式使這些元素深度融合.表述性狀態(tài)傳遞(representational state transfer， REST)最早作為一種面向分布式超媒體系統(tǒng)的體系結(jié)構(gòu)被提出[1]，基于REST的服務(wù)被稱為RESTful服務(wù).作為一種資源為中心且完全基于基本HTTP協(xié)議的服務(wù)交互方式，RESTful服務(wù)由于其簡單、可伸縮和高共享等特性，已經(jīng)越來越多地被應(yīng)用于云計算、物聯(lián)網(wǎng)等典型的泛在服務(wù)應(yīng)用中[2].截止2013年，RESTful服務(wù)已超過傳統(tǒng)SOAPWS-*Web服務(wù)成為以互聯(lián)網(wǎng)為核心的應(yīng)用系統(tǒng)中使用最廣泛的消息交互方式.

文獻[1,3]中提出了RESTful服務(wù)的核心特征和成熟度模型.目前，國外諸多知名廠商，如Paypal，e-Bay，Amazon等的RESTful服務(wù)實現(xiàn)已經(jīng)進入了RESTful成熟度3級，也即以超媒體鏈接作為應(yīng)用狀態(tài)引擎(hypermedia as the engine of application state， HATEOAS)階段.與原子SOAPWS-*Web服務(wù)中的1次服務(wù)請求中輸入和輸出相對確定不同，符合HATEOAS原則的RESTful服務(wù)允許在服務(wù)響應(yīng)中包含鏈接(link)，這些鏈接可能被作為后續(xù)操作的定位，也可能被作為狀態(tài)引擎引發(fā)對新資源的訪問.HATEOAS特性使得1次RESTful服務(wù)請求和響應(yīng)過程中，可能包含了涉及不同角色多參與方的內(nèi)部狀態(tài)變遷和數(shù)據(jù)轉(zhuǎn)移，而這種轉(zhuǎn)移通過鏈接自動觸發(fā)，對于用戶完全透明，用戶將喪失對自身隱私數(shù)據(jù)的控制權(quán)，從而引入了額外的隱私風(fēng)險.

OECD[4]，ISO29100[5]等隱私保護標準和規(guī)范都將“提供可驗證的方式，確保軟件的實現(xiàn)滿足對應(yīng)的隱私需求”列為隱私保護需要滿足的最重要原則之一.因此，如何從隱私角度建模RESTful服務(wù)鏈接驅(qū)動的應(yīng)用狀態(tài)并支持隱私需求的驗證也即成為面向RESTful服務(wù)隱私保護中的1個基本問題.目前已有部分研究針對HATEOAS特性，對RESTful服務(wù)的建模開展了研究，如文獻[6-7]分別采用UML的狀態(tài)圖和類圖從不同側(cè)面對RESTful服務(wù)組合的結(jié)構(gòu)和行為進行了建模.文獻[8]采用時序邏輯刻畫了RESTful服務(wù)的組合.文獻[9-10]則分別使用Petri網(wǎng)和有限狀態(tài)機對RESTful的HATEOAS鏈接進行了建模.但這些研究工作多集中于由鏈接引發(fā)的資源之間的行為交互，對于如何從隱私數(shù)據(jù)保護的角度刻畫RESTful服務(wù)的應(yīng)用狀態(tài)尚未有研究.另一方面，上述建模工作尚主要依賴于人工建模，缺乏從服務(wù)描述文檔向所生成模型自動轉(zhuǎn)化的能力.

為了能精確反映RESTful服務(wù)中的隱私相關(guān)操作并支持自動化的模型生成，本文提出了一種形式化的RESTful服務(wù)應(yīng)用狀態(tài)隱私模型以及從RESTful服務(wù)描述向此模型的自動轉(zhuǎn)換方法，其總體思路有4點：

1) 針對RESTful系統(tǒng)中隱私活動的特征，建立隱私活動的元模型和形式化定義；

2) 建立RESTful服務(wù)關(guān)鍵概念的精確語義以及RESTful服務(wù)中應(yīng)用狀態(tài)和隱私活動間的映射關(guān)系；

3) 通過跟蹤資源描述文檔，生成資源鏈接關(guān)聯(lián)樹描述RESTful服務(wù)由HATEOS所引發(fā)的鏈接和資源操作間的迭代關(guān)系；

4) 將資源鏈接樹中不同類型節(jié)點和邊自動轉(zhuǎn)化為語義精確的單事件確定有限自動機模型.

同時，在以上理論工作的基礎(chǔ)上結(jié)合案例分析和工具實現(xiàn)，對上述方法的可用性展開討論.

1 背景與相關(guān)工作

1.1 RESTful服務(wù)核心概念

圖1(a)描述了RESTful中的核心概念——資源(resource)，一個資源由一個URI唯一指定，且可能包含多個針對不同HTTP方法的資源操作，Request和Response分別代表了HTTP協(xié)議的請求和響應(yīng)，在請求中主要輸入外部參數(shù)，并通過method指定對應(yīng)的HTTP方法(GET，POST，PUT，DELETE).1個請求可能對應(yīng)多種不同結(jié)果的響應(yīng)，每種響應(yīng)都會對應(yīng)1個HTTP的返回狀態(tài)碼，以及對應(yīng)的消息響應(yīng)頭和響應(yīng)體.每個資源操作的請求和響應(yīng)又被稱為一個應(yīng)用狀態(tài)(application state, AS).由于針對一個資源的各應(yīng)用狀態(tài)之間互相獨立，因此我們建模的重點主要圍繞一個應(yīng)用狀態(tài)展開.

Fig. 1 Kernel concepts in RESTful service圖1 RESTful服務(wù)核心概念

在服務(wù)響應(yīng)中攜帶鏈接，是支持HATEOAS RESTful服務(wù)的1個典型特征.這些鏈接不僅作為數(shù)據(jù)返回，同時也作為驅(qū)動引擎，引發(fā)對新資源的請求.文獻[10]將RESTful服務(wù)響應(yīng)中的鏈接進一步分為3類：協(xié)議級、超媒體級和應(yīng)用級.協(xié)議級的鏈接是包含在HTTP狀態(tài)碼(如400，500等)返回頭中的鏈接;超媒體級的鏈接是指在響應(yīng)體中會自動引發(fā)對新內(nèi)容引用的鏈接，如HTML中的〈IMG〉和〈Script〉標簽等；應(yīng)用級的鏈接則為需要通過業(yè)務(wù)流程執(zhí)行才會被觸發(fā)的鏈接，如HTML中的〈a〉和〈button〉等標簽所代表的鏈接.圖1(b)描述了這3類不同鏈接在服務(wù)響應(yīng)里的體現(xiàn).由于協(xié)議級鏈接和超媒體級鏈接都會自動引發(fā)對新資源的請求，我們必須跟蹤所有這2類鏈接，才能獲得完整的隱私數(shù)據(jù)在各個服務(wù)和參與方之間的使用和暴露情況.而對于應(yīng)用級鏈接，主要通過業(yè)務(wù)流程語言進行描述，目前已有大量工作針對諸如服務(wù)組合執(zhí)行語言(business process execution language, BPEL)開展了建模，將前2類鏈接的建模結(jié)果與業(yè)務(wù)流程語言模型相結(jié)合即可對應(yīng)用級鏈接開展相關(guān)分析.

1.2 相關(guān)工作

我們分別從隱私的描述與建模、RESTful服務(wù)的建模以及面向服務(wù)的隱私建模與驗證3方面介紹相關(guān)工作.

1) 在隱私描述與建模驗證方面，當前的工作主要包含3大類別：

① 基于標記語言(如XML)的定義

W3C組織提出的P3P(the platform for privacy preferences)描述語言[11]以及對應(yīng)的隱私偏好描述語言[12](a P3P preference exchange language, APPEL)、OASIS組織提出的用于訪問控制的XACML(extensible access control markup language)及其隱私Profile擴展[13]、IBM提出的隱私策略描述語言[14](enterprise privacy authorization language， EPAL)等都采用標記語言進行隱私定義.這類方法的共同問題是缺乏精確的語義，且缺乏隱私活動發(fā)生條件和對應(yīng)義務(wù)的定義方式，因此難以和系統(tǒng)模型間進行驗證與確認.

② 基于角色訪問控制模型的建模

基于角色的訪問控制模型(role based access control, RBAC)[15]最早被用于角色授權(quán)和訪問，并不包含對于隱私數(shù)據(jù)和目的的定義.文獻[16]擴展了此模型，增加了否定條件和目的定義，并首次將此模型應(yīng)用于英國電子健康記錄的管理.但此模型無法表征隱私活動的未來義務(wù)和隱私數(shù)據(jù)的層次特性.隱私敏感的角色訪問控制模型(privacy-aware role-based access control, PARBAC)[17]注意到了角色、目的、數(shù)據(jù)主體中的偏序關(guān)系，但缺乏對于這些關(guān)系以及隱私活動交互的形式化精確定義，且缺乏對于隱私活動發(fā)生條件的定義機制.P-RBAC[18]是第1個以隱私數(shù)據(jù)為中心的RBAC擴展，其中明確定義了角色、數(shù)據(jù)、目的和約束的關(guān)系，但其策略描述和約束定義主要基于自然語言，使得難以直接在系統(tǒng)模型中驗證相關(guān)隱私需求的可滿足性.

③ 基于形式化方法的建模和驗證

形式化方法由于具備精確描述的表達能力并能執(zhí)行對應(yīng)的驗證和模型檢測，被廣泛應(yīng)用于軟件和系統(tǒng)建模中.文獻[19]提出了一種隱私API及其邏輯框架，并將此模型轉(zhuǎn)化為Promela語言利用模型檢測工具SPIN進行了模型驗證；文獻[20]提出了一種基于線性時序邏輯(linear temporal logic, LTL)的隱私框架，用于進行隱私規(guī)約一致性的檢測；文獻[21]基于體系機構(gòu)，采用對認知邏輯(epistemic logic)的隱私擴展來表述隱私策略，并提供了一種在設(shè)計階段對隱私分析(privacy by design)的思路;本文所在團隊也對隱私需求的建模進行了研究，從語義和行為上對隱私策略進行了精確刻畫[22-23]；在隱私需求的驗證與分析方面，文獻[24-25]分別采用π演算和度量一階時序邏輯(metric first-order temporal logic， MFOTL)對靜態(tài)和運行時的隱私進行了驗證，但這些工作都未回答如何對所要驗證的系統(tǒng)進行隱私建模.

2) 在RESTful服務(wù)的描述和建模方面

Web應(yīng)用描述語言WADL[26]是目前使用最廣泛的RESTful服務(wù)描述語言.WADL基于XML，支持RESTful中資源、資源間關(guān)系、資源表述以及鏈接等核心概念的描述.最新版本的WSDL[27]也增加了對基于HTTP協(xié)議服務(wù)交互的支持，以上描述都基于標記性語言，難以直接建立語義精確的形式化模型.文獻[6-7]分別采用UML的狀態(tài)圖和類圖從不同側(cè)面對RESTful服務(wù)組合的結(jié)構(gòu)和行為進行了建模；文獻[8]采用時序邏輯刻畫了RESTful服務(wù)的組合；在RESTful服務(wù)的HATEOAS特性方面，文獻[9-10]分別使用Petri網(wǎng)和有限狀態(tài)機對RESTful的HATEOAS鏈接進行了建模；文獻[28-29]更進一步關(guān)注了由于HATEOAS特性所引發(fā)的多角色參與和內(nèi)部的控制流狀態(tài)變遷，分別使用自定義的角色網(wǎng)絡(luò)和UML時序圖對HATEOAS特性引發(fā)的狀態(tài)變遷進行了建模.以上工作主要面向功能建模，對于數(shù)據(jù)，尤其是隱私相關(guān)數(shù)據(jù)的模型都未有涉及，且上述工作主要依賴于人工手段完成建模，無法自動從服務(wù)描述文檔中生成模型.文獻[30]意識到了RESTful服務(wù)數(shù)據(jù)建模的重要性，從概念層面對RESTful服務(wù)中的數(shù)據(jù)交互和數(shù)據(jù)流進行了分析，但未提出具體的模型，也沒有提供進一步的分析方法.針對RESTful的數(shù)據(jù)流，JOpera[31]滿足RESTful服務(wù)的各項原則，是目前最成熟的RESTful服務(wù)組合語言，JOprea通過可視覺化的控制流依賴圖和數(shù)據(jù)流轉(zhuǎn)換圖來描述RESTful服務(wù)組合，且與針對服務(wù)組合執(zhí)行語言(business process execution language, BPEL)的RESTful擴展[32-33]之間可以互相映射.與之類似的Bite[34]采用對BPEL擴展的方式支持RESTful服務(wù)組合描述，但僅支持部分HTTP操作(PUT操作不被支持[34]).文獻[35]則采用擴展的影響圖(extended influence diagram)作為可視化的建模語言用于描述RESTful服務(wù).這些方法關(guān)注了RESTful服務(wù)中的數(shù)據(jù)流，但其主要研究對象為不同應(yīng)用狀態(tài)的應(yīng)用級鏈接組合后的模型，對由于協(xié)議級或超媒體級鏈接而引發(fā)的應(yīng)用狀態(tài)內(nèi)部變遷未進行討論.

3) 在面向服務(wù)的隱私建模和驗證方面

文獻[36]將BPEL與P3P策略描述進行了對應(yīng)，并開展了驗證分析;文獻[37-38]利用日志分析中的事件流捕捉技術(shù)，對服務(wù)組合的執(zhí)行進行了運行期的監(jiān)控和隱私時間屬性的分析;文獻[39]將用戶的隱私屬性表達為一系列的LTL公式，并基于現(xiàn)有的服務(wù)組合模型進行了驗證;文獻[40-41]則分別對如何在SOAPWS-*服務(wù)組合的編制和編排過程中保持隱私約束進行了研究;本團隊之前也開展了這方面的研究，采用基于接口自動機和超圖對服務(wù)組合中的最小隱私暴露和最優(yōu)隱私授權(quán)以及特定類型的隱私需求的驗證進行了研究[42-44].以上這些工作都主要面向SOAPWS-*Web服務(wù)組合，對于如何在RESTful服務(wù)中進行隱私建模和驗證仍基本空白.且上述工作大多僅關(guān)注1次服務(wù)調(diào)用中的隱私數(shù)據(jù)傳遞，對于與隱私數(shù)據(jù)相關(guān)的目的、角色等少有涉及，難以完整地刻畫系統(tǒng)執(zhí)行過程中的隱私活動.

2 RESTful服務(wù)中的隱私活動建模

2.1 RESTful服務(wù)中隱私活動元模型

隱私活動是指在1個或多個參與方之間針對隱私數(shù)據(jù)的特定隱私操作.不同的組織和研究者，對于隱私活動中包含的元素給出了不同的定義.文獻[4-5,45]分析了隱私活動所必須包含的基本元素.

從隱私數(shù)據(jù)的角度，目的(purpose)在所有文獻中都被作為1個核心元素.文獻[45]中的粒度(granularity)和文獻[4]中的敏感級別(degrees of sensitivity)都共同表述了隱私數(shù)據(jù)的層次結(jié)構(gòu)和偏序關(guān)系.文獻[45]中的可見性(visibility)、文獻[5]中的數(shù)據(jù)主體(data subject)和數(shù)據(jù)控制者(data controller)以及文獻[5]中的角色和權(quán)限(actors and roles)則都用于表征隱私數(shù)據(jù)的上下文關(guān)系.綜上，我們最終選取3個屬性作為必須在隱私需求描述語言中涵蓋的關(guān)鍵屬性：

1) 目的(purpose)定義了使用隱私數(shù)據(jù)的意圖；

2) 數(shù)據(jù)層次(data hierarchy)定義了隱私數(shù)據(jù)的結(jié)構(gòu)和偏序關(guān)系；

3) 參與方角色(role of participants)定義隱私數(shù)據(jù)相關(guān)的不同參與方和角色層次結(jié)構(gòu).

從隱私數(shù)據(jù)相關(guān)的動作和約束的角度，主要可總結(jié)為目的規(guī)約和隱私操作限制2項原則.其中前者主要指明隱私活動的目的應(yīng)該與具體的角色和參與方關(guān)聯(lián)，且包含其發(fā)生條件和未來義務(wù)的約束定義；后者則闡述了隱私操作的多樣性.本文隱私活動的元模型基于以上分析展開.如圖2所示是本文隱私活動的元模型UML類圖，我們在2.2節(jié)將針對此元模型中不同元素給出其詳細說明和形式化定義.

Fig. 2 Privacy action meta model for RESTful service圖2 RESTful服務(wù)中隱私活動的元模型

2.2 RESTful服務(wù)中隱私活動元模型形式化語義

2.2.1 參與方與角色模型

RESTful服務(wù)應(yīng)用中存在多參與方，不同參與方又各自承擔(dān)著不同的角色.設(shè)PA為參與方集合，?pa∈PA，我們用Inst(pa)表示pa的運行時實例.如設(shè)用戶(User)是某參與方，Inst(User)則表示某次執(zhí)行時所關(guān)聯(lián)的某個具體用戶.

為了保證上下文的完整性，我們引入角色和參與方之間進行關(guān)聯(lián).設(shè)R為所有角色的集合，角色賦值關(guān)系集合AS是PA×R的1個子集.考慮到角色之間往往存在層次關(guān)系，我們進一步對不同角色之間的偏序關(guān)系進行定義.對?r1,r2∈R,我們用r1≤r2來表示r2是r1的泛化.例如，角色第3方(the 3rd party)是角色支付服務(wù)(payment service)的1個泛化.角色賦值集合AS必須在角色泛化關(guān)系下封閉，也即若r1≤r2∧a1=(pa,r1)∈AS則a2=(pa,r2)∈AS，我們使用a1

2.2.2 隱私數(shù)據(jù)模型

我們將未與任何角色關(guān)聯(lián)的隱私數(shù)據(jù)的名稱稱為隱私數(shù)據(jù)項，而將與角色關(guān)聯(lián)后的隱私數(shù)據(jù)項稱為隱私數(shù)據(jù).例如“姓名”為1個隱私數(shù)據(jù)項，而“家長的姓名”則為1個隱私數(shù)據(jù).設(shè)D為所有隱私數(shù)據(jù)項的集合，?d∈D,r∈R,隱私數(shù)據(jù)da=(r,d)∈R×D表示角色r是隱私數(shù)據(jù)項d的數(shù)據(jù)主體.例如，(Parent，Name)和(Child，Name)分別表示家長的姓名和孩子的姓名.一些隱私數(shù)據(jù)項可以通過某些規(guī)則從另一些隱私項中推理得到，如使用(Parent，Postal_address)易得到(Parent，Postal_code)，而(Child，F(xiàn)irst_name)則可從(Child，F(xiàn)ull_name)中推出.設(shè)DA為所有隱私數(shù)據(jù)集合，RU是所有數(shù)據(jù)推理規(guī)則集合，?DA1,DA2?DA，ru=(DA1,DA2)∈RU是DA×DA的1個子集，用于表示DA2中的隱私數(shù)據(jù)可以通過DA1中的隱私數(shù)據(jù)推理得到.

2.2.3 隱私操作模型

對于1個RESTful服務(wù)，其通過GET，PUT，POST，DELETE這4個HTTP動作完成資源提交，而傳統(tǒng)的隱私操作分類中最常見的為“收集”、“使用”、“暴露”和“維持”.這4個操作和HTTP動作間存在較好的對應(yīng)關(guān)系，我們在本文中將隱私操作集合OPR定義為{Collect，Disclose，Use，Delete}，通常來說在SOAPWS-*的服務(wù)中，其每個服務(wù)所對應(yīng)的操作需要根據(jù)服務(wù)具體的語義和語境人工決定.但RESTful服務(wù)的HTTP動作和隱私操作間存在著清晰的對應(yīng)關(guān)系，我們將在3.2節(jié)中利用此關(guān)系自動完成服務(wù)中隱私操作的生成.隱私操作必須和具體的目的相關(guān)聯(lián).

Fig. 3 Sample RESTful service with HATEOAS constraints圖3 帶有HATEOAS 特性的RESTful 服務(wù)示例

如2.1節(jié)所述，隱私操作目的間也存在層次關(guān)系.和角色賦值的層次關(guān)系不同，每個目的都最多僅有1個直系祖先，也即所有目的最終可組成一棵樹，我們使用全集T作為這棵樹的根節(jié)點.設(shè)PUR為所有目的的集合，對?pu1,pu2∈PUR，我們使用pu1pu2來表示pu1是pu2的泛化.

1個隱私活動可以視為在謂詞約束關(guān)系下針對一系列隱私數(shù)據(jù)的1個隱私操作,其形式定義如定義1所示.

定義1. 隱私活動.1個隱私活動可以用五元組p=〈Da,opr,sender,receiver,θ〉表示，其中：

Da?DA是一組關(guān)聯(lián)了角色的隱私數(shù)據(jù)；

opr∈OPR×PUR是1個關(guān)聯(lián)了目的的隱私動作；

sender和receiver是帶有角色賦值的2個參與方，用于表示隱私動作的發(fā)起者和接受者,對于僅牽涉到1個參與方的隱私動作(如刪除和使用)，我們令sender=receiver；

θ是一系列與Da，sender和receiver相關(guān)的謂詞約束，用于表示此隱私活動的發(fā)生條件.

假設(shè)OP={Collect，Disclose}，PUR={Consent}，R={Child，Parent，SP}，PA={User，Website}，其中SP表示服務(wù)提供方，Consent表示取得家長的同意.“1個13歲以下的兒童提供其姓名和其家長的電子郵件給某網(wǎng)站以便讓網(wǎng)站取得其家長的同意”可以被定義為

〈{(Child，Name)，(Parent，Email)}，(Disclose，Consent)，(User，Child)，(Website，SP)，{Inst(Child).age<13}〉.

從隱私的角度看，1次系統(tǒng)的執(zhí)行可以被視為一系列隱私活動的序列，我們將其稱為隱私執(zhí)行序列.假設(shè)所有的系統(tǒng)執(zhí)行都將在有限步后終止，則隱私執(zhí)行序列也必然是有限序列.設(shè)P為所有隱私活動集合，任意的隱私執(zhí)行序列σ=p1p2…pn，其中p1,p2,…,pn∈P∩P也為有限.

3 RESTful服務(wù)資源操作隱私建模

3.1 RESTful服務(wù)的形式化語義

圖3描述了1個帶有HATEOAS特性的RESTful服務(wù)(圖3中所有資源的操作都為GET)，用戶通過“Login”服務(wù)的HTTP Request提交用戶名和密碼，“Login”服務(wù)決定用戶登錄是否成功.如登錄成功則以狀態(tài)碼201通過HTTP Response返回包含2個多媒體級鏈接“HobbyLink”和“HistoryLink”的響應(yīng)結(jié)果，這2個鏈接對應(yīng)“Hobby”和“History”2個資源，在收到響應(yīng)后將自動依次向這2個資源發(fā)起進一步請求，分別獲得用戶的興趣列表和網(wǎng)站歷史列表.“History”資源根據(jù)用戶名返回其所在地區(qū)，并根據(jù)地區(qū)再自動發(fā)起對“DomHistory”或“Oversea”資源的請求，并分別返回對應(yīng)地區(qū)的廣告列表和用戶操作歷史.如“Login”登錄失敗則以狀態(tài)碼403通過HTTP Response返回包含“ADLink”鏈接的響應(yīng)結(jié)果，并在收到響應(yīng)后自動請求此鏈接代表的“Advertise”資源，獲得網(wǎng)站廣告列表.如登錄資源未找到，則以狀態(tài)碼404直接返回錯誤消息.上述例子顯示了由HATEOAS特性引發(fā)的RESTful服務(wù)應(yīng)用狀態(tài)和傳統(tǒng)服務(wù)SOAPWS-*原子服務(wù)之間的差別.鏈接在RESTful服務(wù)中不再僅作為數(shù)據(jù)存在而且起到了部分業(yè)務(wù)流程引擎的作用，從而在1次服務(wù)請求中可能引發(fā)對多個資源的多次操作，而且包含了內(nèi)部狀態(tài)的變遷.

RESTful服務(wù)由一系列資源構(gòu)成，其中每個資源都通過1個URI標識其唯一性，表征資源的URI至少包含2個部分——表征HOST的base部分和與某HTTP動作相結(jié)合用以刻畫具體操作的path部分.與一般意義上的URI不同，資源所對應(yīng)的URI中常包含運行時參數(shù).如Github上，對1個gists加星操作對應(yīng)的URI為gists:idstar，其中id將在運行期被替換為具體gists的id，由于這些運行時參數(shù)常會包含隱私數(shù)據(jù)信息，我們必須對其單獨記錄，據(jù)此我們可得RESTful服務(wù)中的資源URI如定義2.

定義2. 資源URI.設(shè)1個資源URI中所有運行時參數(shù)集合為RUN，1個資源URI可被定義為1個四元組〈base，path，RD，PAR〉，其中base為URI的HOST部分，path為對應(yīng)的相對路徑，RD用以記錄此URI中所包含的所有運行時參數(shù)，PAR則為此資源訪問時通過形如“?u=xx&v=yy”方式所指定的參數(shù)列表.

任意1個RESTful服務(wù)的資源都可以由URI唯一標識，而1個資源中又包含了多個不同操作.這些資源操作既可能針對不同的HTTP動作，也可能針對同一HTTP動作的不同表述.

定義3. 資源.1個RESTful服務(wù)資源res可以用四元組res=〈URI，name，desc，OP〉表示，其中URI，name和desc分別代表此資源對應(yīng)URI的名稱和描述，OP則為此資源對應(yīng)的所有操作集合.對于任意op∈OP，我們進一步給出其定義.

定義4. 資源操作.針對URI資源的操作op可表示為多元組:op=(URI，method，inType，outType，IN，OUT，LINK，Σ，Δ)，其中:

URI和method為該操作對應(yīng)的資源和HTTP動作，method∈{GET,POST,PUT，DELETE};inType和outType分別為請求和響應(yīng)的表述類別，一般由HTTP Request和HTTP Response中的content type屬性決定，常見的表述類別如texthtml,applicationxml等;IN，OUT分別為HTTP Request和HTTP Response消息體中的數(shù)據(jù)集合，其中OUT集合包含了針對不同HTTP響應(yīng)代碼的所有返回消息體，設(shè)HC為HTTP響應(yīng)代碼集合，?hc∈HC，O(hc)?OUT表示針對某一特定HTTP返回代碼的消息體中的數(shù)據(jù)集；LINK為鏈接集合，用于記錄此操作對應(yīng)服務(wù)響應(yīng)中包含的所有級別的鏈接，對于?link∈LINK,我們在定義5中給出其形式化定義;Σ(OUT):2OUT→2LINK映射關(guān)系用以表示HTPP Response消息體中所包含的超媒體鏈接集合Δ∈HC×LINK×Σ(O(hc))表示此操作在特定HTTP返回代碼下包含的所有協(xié)議鏈接和超媒體鏈接集合.

服務(wù)響應(yīng)中所包含的鏈接既可能指向某個RESTful服務(wù)資源，也可能僅指向通用意義的地址如網(wǎng)頁或圖片等.對于指向資源的鏈接，為避免建模過程中產(chǎn)生死鎖，需要區(qū)分是指向當前資源還是指向新的資源，同時為描述此鏈接的觸發(fā)方式和觸發(fā)時機，還需要明確此鏈接的級別(協(xié)議級、超媒體級或應(yīng)用級).RESTful服務(wù)響應(yīng)中所包含鏈接的另一個重要特性是可以指定鏈接發(fā)生的條件或約束，這種條件可能與某個特定HTTP返回代碼關(guān)聯(lián)，也可能基于XPath或其他數(shù)據(jù)選擇語言的鏈接選擇器(selector).我們據(jù)此可得RESTful服務(wù)中的鏈接如定義5

定義5. 鏈接.1個RESTful服務(wù)響應(yīng)中的鏈接link∈LINK，可表示為多元組：link=〈location，isResource，type，level，condition〉.其中,location為此鏈接的URI地址;isResouce∈{true，false}表明此鏈接是否指向RESTful資源;type∈{self，target}表明此鏈接指向的是自身資源還是新資源;level∈{protocol，hypermedia，application}代表此鏈接的不同級別;condition用于指定此鏈接的發(fā)生條件，對于協(xié)議級鏈接，其condition即為對應(yīng)的HTTP返回代碼，對于超媒體級鏈接，其condition則為對應(yīng)ContentType的是鏈接選擇器所指定的謂詞表達式.由于鏈接所指向資源的響應(yīng)中又可能會包含對新資源的引用，資源和鏈接之間存在著迭代關(guān)系.我們使用資源鏈接關(guān)聯(lián)樹來表示這種多層的迭代關(guān)系，其形式化定義如下:

定義6. 資源鏈接關(guān)聯(lián)樹.RESTful服務(wù)中的資源操作op所對應(yīng)的資源鏈接關(guān)聯(lián)樹T(op)可被定義為1個五元組(N，root，λ，DE，CO).其中：

N?OP∪⊥為節(jié)點集合，其中空節(jié)點⊥不對應(yīng)任何資源操作，僅用以表征和后續(xù)資源間的關(guān)系；

root∈N為根節(jié)點，對于表征應(yīng)用狀態(tài)的資源操作，其根節(jié)點唯一；

DE?N×λ×N，表示樹中的邊集，對?de∈DE，我們分別用s(de)和t(de)表示此邊的源節(jié)點和目標節(jié)點;

CO?DE×CON為觸發(fā)條件定義，其中CON為服務(wù)響應(yīng)鏈接集合中所有condition的集合.

我們假定所有的資源操作中都可正確執(zhí)行，也即不存在資源操作a中的響應(yīng)鏈接請求資源操作b，b中的響應(yīng)鏈接又請求a的死鎖狀況.則任意1個T(op)都滿足：

1) 僅有root無父節(jié)點.

?n∈N,?n′∈N→(n′,n)∈DE?n=root.

2)DE中無環(huán).

?n1,n2,…,nk∈N,?n1→n2→…→nk→n1.

圖3所示服務(wù)對應(yīng)的資源鏈接關(guān)聯(lián)樹如圖4所示：

Fig. 4 Sample of resource link relation tree圖4 資源鏈接關(guān)聯(lián)樹示例

3.2 資源操作與隱私活動的映射

上述模型中并未包含任何隱私信息，我們進一步分析RESTful服務(wù)和2.2.3節(jié)隱私活動模型間的對應(yīng)關(guān)系并藉此討論RESTful服務(wù)應(yīng)用狀態(tài)的隱私模型.第2節(jié)的隱私活動模型中包含了隱私數(shù)據(jù)項、角色與參與方、隱私動作、和約束4方面內(nèi)容，我們將其與RESTful服務(wù)一一進行對應(yīng).

通過表2可以看出，東成站注水系統(tǒng)、丘陵35 MPa注水系統(tǒng)、勝北25 MPa注水系統(tǒng)和鄯善聯(lián)合站25 MPa注水系統(tǒng)（溫西六區(qū)域）4個注水系統(tǒng)的注水泵運行負荷比額定偏差較大，東成站注水系統(tǒng)、丘陵35 MPa注水系統(tǒng)和勝北25 MPa注水系統(tǒng)使用了變頻控制柜裝置，有效提高了注水泵機組效率，但仍然存在一定的提升空間；鄯善聯(lián)合站25 MPa注水系統(tǒng)（溫西六區(qū)域）運行負荷低且沒有使用變頻控制柜，泵機組效率僅為52.68%。根據(jù)實際情況提出相應(yīng)的節(jié)能措施。

1) 隱私數(shù)據(jù)

在服務(wù)的請求中可能有3部分內(nèi)容包含了隱私數(shù)據(jù)：1)URI中的運行時參數(shù)RD;2)URI中由問號引導(dǎo)的形如“?u=xx&v=yy”方式的參數(shù)集合PAR;3)Request對象〈BODY〉部分包含的提交數(shù)據(jù).由于〈BODY〉部分的數(shù)據(jù)封裝方式不固定，因此并沒有通用的方法直接從RESTful服務(wù)請求中抽取數(shù)據(jù)項，但RESTful服務(wù)描述語言WADL或WSDL 2.0的結(jié)構(gòu)化方式使得我們針對具體應(yīng)用進行分析并獲取對應(yīng)的隱私數(shù)據(jù)成為可能.我們用DaIn(op)表示1個RESTful資源操作所對應(yīng)輸入中包含的隱私數(shù)據(jù)項.

在服務(wù)的響應(yīng)中，不同的HTTP返回代碼可能對應(yīng)不同的響應(yīng)內(nèi)容，對?op∈OP,hc∈HC,我們用DaOut(op，hc)表示針對某一HTTP返回代碼的服務(wù)響應(yīng)中所包含的隱私數(shù)據(jù)項集合.

2) 角色與參與方

RESTful服務(wù)URI的base部分事實上已經(jīng)區(qū)分了不同資源所面向的參與方，我們僅需要將URI的base部分和服務(wù)參與方集合PA之間進行映射即可.角色和具體操作相關(guān)，針對角色集合R，我們用sender(op)和receiver(op):op→PA×R分別代表RESTful服務(wù)中的資源操作op的發(fā)起方與接收方.

3) 隱私動作

我們在第2節(jié)將隱私動作定義為收集、使用、暴露和維持.RESTful服務(wù)所使用的HTTP協(xié)議動作可以和上述的隱私動作之間形成精確的對應(yīng)關(guān)系如表1所示.

定義1中，對于每個隱私動作還指明了其對應(yīng)的目的(purpose)，由于目的是1個主觀性較強的定義，無法直接從資源描述中獲取，需要在后續(xù)分析過程中，由領(lǐng)域?qū)＜液拖到y(tǒng)設(shè)計人員共同人工方式確認.因此由資源描述所生成的隱私活動中不會包含目的.

Table 1 Mapping Relation between Privacy Operation and RESTful Service表1 隱私動作和RESTful服務(wù)的對應(yīng)關(guān)系

4) 約束

對于協(xié)議級鏈接所指向的資源操作，其約束條件即為對應(yīng)的HTTP響應(yīng)代碼，對于超媒體級鏈接所指向的資源操作，其約束條件即為由對應(yīng)表述類型的選擇器(selector)所描述的謂詞表達式，我們用δ(op)表示1個隱私操作發(fā)生的約束條件.

最終，1個資源操作op的請求將可能對應(yīng)0個或1個隱私活動，而其響應(yīng)則可能對應(yīng)多個隱私活動，其具體對應(yīng)規(guī)則為

① 若DaIn(op)≠?∧(method(op)=GET∨method(op)=POST)∧sender(op)≠receiver(op)，則對應(yīng)隱私活動pa=〈DaIn(op)，Collect，sender(op)，receiver(op)，δ(op)〉；

② ?hc∈HC，若DaOut(op,hc)≠?∧(method(op)=GET∨method(op)=POST)∧sender(op)≠receiver(op)，則對應(yīng)隱私活動pa=〈DaOut(op,hc),Disclose,receiver(op),sender(op),hc〉；

③ 若(DaIn(op)≠?∧method(op)=PUT)∨(DaIn(op)≠?∧(method(op)=GET∨method(op)=POST)∧sender(op)=receiver(op))，則對應(yīng)隱私活動pa=〈DaIn(op),Use,sender(op),receiver(op),δ(op)〉；

④ 若(DaIn(op)≠?∧method(op)=DELETE)則對應(yīng)隱私活動pa=〈DaIn(op),Delete,sender(op),receiver(op),δ(op)〉.

我們分別使用pain(op)和paout(op，hc)表示資源操作op的請求對應(yīng)的隱私活動以及op在返回特定HTTP狀態(tài)碼hc時對應(yīng)的隱私活動.

按照上述對應(yīng)規(guī)則，假設(shè)圖3中的RESTful服務(wù)的參與方集合PA={User,Online,Ad_Service,History_Service}分別表示用戶、在線服務(wù)、廣告服務(wù)和歷史查詢服務(wù)，角色集合R={User,Server,3rd}分別代表用戶、服務(wù)提供商和第3方.“Login”和“Hobby”2個服務(wù)參與方為Online;“Advertise”參與方為Ad_Service;“History”,“DomHistory”,“OverseaHistory”這3個服務(wù)的參與方為History_Service;關(guān)注的隱私數(shù)據(jù)項集合D={name,location,hobby,history}，則圖3中的RESTful服務(wù)對應(yīng)的隱私活動集合如下：

pain(Login)=〈{(User,name)},Collect,(User,User),(Online,Server),?〉；

paout(Login,201)=paout(Login,403)=paout(Login,404)=pain(Advertise)=paout(Advertise,201)=?；

pain(Hobby)=〈{(User,name)},Use,(Online,Server),(Online,Server),?〉；

paout(Hobby,201)=〈{(User,hobby),Use,(Online,Server),(Online,Server),?〉；

pain(History)=〈{(User,name)},Collect,(Online,Server),(History_Service,3rd),?〉；

paout(History,201)=〈{(User,location)},Disclose,(History_Service,3rd),(Online,Server),?〉；

pain(DomHistory)=〈{(User,name),(User,location)},Collect,(Online,Server),(History_Service,3rd),?〉；

paout(DomHistory,201)=〈{(User,history),Disclose,(History_Service,3rd),(Online,Server),?〉；

pain(Oversea)=〈{(User,name),(User,location)},Collect,(Online,Server),(History_Service,3rd),?〉；

paout(Oversea,201)=〈{(User,history),Disclose,(History_Service,3rd),(Online,Server),?〉.

這個從資源描述中所生成的隱私活動并不包含目的，如果在后續(xù)分析中需要單獨基于隱私動作的目的進行分析，則尚需要在上述生成的隱私活動中，手動為每個活動中的隱私動作指定目的(由于本文的后續(xù)部分不涉及到基于目的的分析，我們直接使用從資源描述中生成的隱私活動集合).

4 RESTful服務(wù)隱私模型的形式化模型

為進一步開展面向隱私屬性的驗證與分析，我們需要將1個資源操作所對應(yīng)的資源鏈接關(guān)聯(lián)樹轉(zhuǎn)化為表征遷移系統(tǒng)的形式化模型.由于RESTful服務(wù)的應(yīng)用狀態(tài)是1個典型的有限系統(tǒng)，因此能轉(zhuǎn)化為Kripke結(jié)構(gòu)的自動機、進程代數(shù)或者Petri網(wǎng)都具備了等價且足夠的表達能力來刻畫這一內(nèi)部遷移過程.與通常意義上的遷移系統(tǒng)不同的是，針對1次資源操作，任意時刻僅會最多發(fā)生1個隱私活動.也即意味著不需要在1次變遷上同時監(jiān)測多個獨立屬性，這樣一來，進程代數(shù)和Petri網(wǎng)在處理并發(fā)活動時的優(yōu)勢就不復(fù)存在，而自動機則能夠更直觀地表征這種單事件系統(tǒng).另一方面，考慮到本文所針對的僅僅是RESTful服務(wù)應(yīng)用狀態(tài)的靜態(tài)分析，其中并不牽涉到服務(wù)的演化或變遷的不確定性，因此我們最終使用單事件確定有限自動機來進行RESTful服務(wù)應(yīng)用狀態(tài)的形式化建模，其形式化定義如下：

定義7. 單事件有限自動機.1個單事件有限自動機SFA可以被表示為1個五元組SFA=〈A,S,δ,s0,SA〉，其中:A是1個有限標簽集合；S是1個有限狀態(tài)集;δ?S×2A∪A×S是1個變遷關(guān)系，其中A={a|a∈A}，對于任意t，(si-1,t,si)∈δ僅可能t={p}，p∈A或t?A;s0∈S是初始狀態(tài);SA?S是可接受的終止狀態(tài)集，對于1個資源操作而言，由于其代表了1個應(yīng)用狀態(tài)，其終止狀態(tài)應(yīng)有且僅有1個.資源鏈接關(guān)聯(lián)樹與SFA之間存在唯一的映射關(guān)系，其轉(zhuǎn)化方式步驟如下：

1) 非空節(jié)點轉(zhuǎn)化

資源鏈接關(guān)聯(lián)樹中的任意1個非空節(jié)點都代表了1個資源操作，對?n∈N∧n≠⊥，其對應(yīng)資源操作為op∈OP，可經(jīng)過4個步驟轉(zhuǎn)化為SFA：

① 構(gòu)造初始狀態(tài)s1、一般狀態(tài)s2和終止狀態(tài)s3；

② 若pain(op)≠?，則建立變遷〈s1,pain(op),s2〉；若pain(op)=?，則建立變遷〈s1,ε,s2〉；

③ ?hc∈HC,若op的Δ(hc)≠?且paout(op,hc)≠?，則建立變遷〈s2,paout(op,hc),s3〉；

④ ?hc∈HC,若op的Δ(hc)≠?且paout(op,hc)=?，則建立變遷〈s2,(ε,hc),s3〉.

對應(yīng)的算法實現(xiàn)如算法1所示.算法1生成資源鏈接關(guān)聯(lián)樹中的所有資源操作對應(yīng)的SFA，針對某節(jié)點n的單事件自動機記為SFA(n).值得注意的是，資源鏈接樹中可能出現(xiàn)不同節(jié)點指向同一資源操作的情況，考慮到即使是同一資源操作，由于發(fā)生條件不同，其對應(yīng)自動機也可能不同，我們對每個節(jié)點建立獨立單事件自動機.圖4所示的資源鏈接關(guān)聯(lián)樹各節(jié)點轉(zhuǎn)化后的SFA如圖5所示.

算法1. 資源關(guān)聯(lián)樹節(jié)點轉(zhuǎn)化算法.

輸入:N,Datum;*N為資源關(guān)聯(lián)樹中的節(jié)點集合，Datum為需要分析的隱私數(shù)據(jù)項集合*

輸出:Map〈n,SFA〉.*n∈N，SFA為此節(jié)點對應(yīng)的單事件自動機*

for eachninN

if (n≠⊥)

sfa←createNullNFA();

s1←sfa.createInit();

s2←sfa.createState();

s3←sfa.createAccepting();

op←n.getResourceOperation();

pain←op.getInputPrivacyData();

end if

if (pain≠null)

sfa.createTransition(s1,pain,s2);

else

sfa.createTransition(s1,ε,s2);

end if

HTTPCodeList←op.getResponeCodes();

for eachhttpCodeinHTTPCodeList

paout←op.getOutputPrivacyData(httpCode);

if (paout≠null)

sfa.createTransition(s2,paout,s3);

else

sfa.createTransition(s2,(ε,httpCode),s3);

end if

SFAMap.put(n,sfa);

end for

end for

returnSFAMap.

Fig. 5 SFA for each non-empty node in resource-link mapping tree圖5 資源鏈接關(guān)聯(lián)樹非空節(jié)點SFA模型

2) 選擇邊轉(zhuǎn)化

?n∈N，若λ(n)=?表示將在以此節(jié)點為源節(jié)點的所有邊中選擇一條.所有協(xié)議級的鏈接對應(yīng)的邊都為選擇邊，而超媒體級的鏈接也可能為選擇邊，我們首先轉(zhuǎn)化所有協(xié)議級鏈接對應(yīng)的選擇邊.

若s(de)≠⊥∧t(de)=⊥，則表示此選擇邊后續(xù)對應(yīng)的是協(xié)議級鏈接，對SFA(s(de))，如果

〈s2,paout(op,co(de)),s3〉∈δ(SFA(s(de)))∨
〈s2,(ε,co(de)),s3〉∈δ(SFA(s(de)))，

則表示此邊上條件約束所代表HTTP狀態(tài)碼與其源節(jié)點所代表的資源操作自動機中的某變遷對應(yīng)，且系統(tǒng)會在此變遷后與協(xié)議級鏈接中資源操作所對應(yīng)的SFA關(guān)聯(lián).為標記這種關(guān)聯(lián)，我們對SFA(s(de))做如下修改：

① 創(chuàng)建1個新的非終止狀態(tài)sk;

② 刪除所有此HTTP狀態(tài)碼所對應(yīng)的變遷〈s2,paout(op,co(de)),s3〉或〈s2,(ε,co(de)),s3〉；

③ 創(chuàng)建新變遷〈s2,paout(op,co(de)),sk〉或〈s2,(ε,co(de)),sk〉；

④ 若s2與s3間不存在任何變遷，則刪除s3;

⑤ 將t(de)與sk之間標記上關(guān)聯(lián)關(guān)系，用函數(shù)Trans(t(de))表示.

在處理完所有協(xié)議級鏈接對應(yīng)的選擇邊后，資源鏈接關(guān)聯(lián)樹中的所有空節(jié)點都會和1個自動機狀態(tài)建立關(guān)聯(lián).在此基礎(chǔ)上，我們進一步轉(zhuǎn)化超媒體鏈接的選擇邊.

若s(de)=⊥∧t(de)≠⊥，則表示此選擇邊為超媒體級鏈接.超媒體級鏈接的轉(zhuǎn)化分為2步：

① 對FA(t(de))，需要將de所對應(yīng)的選擇條件體現(xiàn)在變遷上.如果〈s1,ε,s2〉∈δ(SFA(t(de)))∧co(de)≠?，則用〈s1,(ε,co(de)),s2〉替換原變遷;否則s1與s2之間的變遷必然為一隱私活動pa，我們將pa上的觸發(fā)條件θ修改為θ∪co(de).

② 超媒體級鏈接的本質(zhì)是在1個資源操作響應(yīng)中自動觸發(fā)對另一個資源操作的請求，為此需要在自動機模型中將這2個資源操作的自動機連接到一起.?a∈A,若〈s1,a,s2〉∈δ(SFA(t(de)))，則將此變遷替換為〈Trans(s(de)),a,s2〉.

選擇邊轉(zhuǎn)化算法如算法2所示，圖6(a)為圖4經(jīng)過選擇邊轉(zhuǎn)化后的結(jié)果.

算法2. 資源關(guān)聯(lián)樹選擇邊轉(zhuǎn)化算法.

輸入:N,DE,S;*N為節(jié)點集合，DE為邊集，S=Map〈n,SFA〉為算法1的輸出*

輸出:Slist.*SList為經(jīng)過轉(zhuǎn)化后生成的SFA集合*

for eachninN

if (n.getType()=?)

edgeList←n.getEdges();

for eachedgeinedgeList

if (edge.getSource()≠⊥ &&edge.getTarget()=⊥)

httpCode←edge.getCondition();

trans1←S.get(n).getByHttpCode(httpCode);

newState←S.get(n).createState();

tran1.setTarget(newState);

accepting←false;

for eachtransactioninS.get(n).

getTranstions()

if (transaction.getTarget()=

S.get(n).getAccepting())

accepting←true;

end if

end for

if (!accepting)S.get(n).removeState

(s.get(n).getAccepting())

edge.getTarget().setRelatedState(newState);

end if

end if

end for

end if

end for

for eachninN

if (n.getType()=?)

edgeList←n.getEdges();

for eachedgeinedgeList

if (edge.getSource()=⊥ &&edge.

getTarget()≠⊥)

condition←edge.getCondition();

if (condition≠null)

SFA←S.get(de.getTarget());

if (SFA.getTransitionLabel(s1,

s2)=ε)

SFA.setTransitionLabel(s1,s2,condition);

else

pa←SFA.getTransitionLabel(s1,s2).getPrivacyAction();

pa.setCondition(pa.getCondition∪condition);

SFA.setTransitionLabel(s1,s2,pa);

end if

end if

SFA1←edge.getSource().getState().getSFA();

SFA2←Merge(SFA,SFA1);state1←SFA.getState(s2);

SFA2.createTransition(edge.

getSource().getState(),state1,

SFA.getTransitionLabel(s1,s2));

SFA2.removeTransition

(sfa.getInitState(),state1,SFA.getTransitionLabel(s1,s2));

SFA2.removeState(sfa.

getInitState());

S.put(edge.getSource(),SFA2);

end if

end for

end if

end for

3) 順序邊轉(zhuǎn)化

?n∈N，若λ(n)=⊕表示以此節(jié)點為源節(jié)點的所有子節(jié)點都將順序執(zhí)行.順序邊的目標節(jié)點都僅可能為1個資源操作，因此僅需要將每個目標節(jié)點對應(yīng)的自動機簡單連接在一起，即可完成順序邊的轉(zhuǎn)化.設(shè)節(jié)點n對應(yīng)的所有順序邊集合為DES(n)?DE，des(i)表示DES(n)中的第i條邊，對SFA(t(des(i)))和SFA(t(des(i+1)))，我們采用3個步驟進行連接:

① 將SFA(t(des(i+1)))中由初始狀態(tài)所引發(fā)的變遷的發(fā)起方修改為SFA(t(des(i)))中的終止狀態(tài);

② 將SFA(t(des(i+1)))中除初始狀態(tài)外的所有狀態(tài)和變遷加入SFA(t(des(i)));

③ 將SFA(t(des(i)))中的終止狀態(tài)集SA修改為SFA(t(des(i+1)))的終止狀態(tài)集.

圖6(b)為圖4經(jīng)過順序邊轉(zhuǎn)化后的結(jié)果.

4) 終止狀態(tài)合并

經(jīng)過上述轉(zhuǎn)化的自動機中，將可能包含多個終止狀態(tài)，這與應(yīng)用狀態(tài)僅有1個終止狀態(tài)的定義不符，為此，需要將所有終止狀態(tài)節(jié)點進行合并，將指向不同終止狀態(tài)的變遷，統(tǒng)一指向1個終止狀態(tài).經(jīng)過終止狀態(tài)合并后，最終生成的應(yīng)用狀態(tài)對應(yīng)的SFA如圖6(c)所示.

根據(jù)形式化模型檢測理論，在對系統(tǒng)完成建模后，將需求也表征為形式化規(guī)約，即可開展進一步的驗證.我們在之前的工作中，已經(jīng)就隱私需求的建模開展了工作，提出了一種可以表述時序約束的聲明式隱私策略語言(declarative privacy policy language, DPPL)及其形式化模型，該語言所采用的形式化模型和本文的模型基于同一隱私活動的元模型，也即意味模型和規(guī)約之間具備了相同的原子命題(atomic proposition)集合.另一方面，DPPL所對應(yīng)的形式化模型也為1個單事件變遷系統(tǒng)，目前已有面向單事件自動機的形式化驗證工具——Declare,本文所建立的模型和隱私需求模型共同作為Declare工具的輸入，即可進行形式化模型檢測，以確定本文所建模的模型是否滿足特定的需求規(guī)約.

Fig. 6 Transformation from resource-link mapping tree to SFA圖6 從資源鏈接關(guān)聯(lián)樹向SFA轉(zhuǎn)換示例

5 案例分析與實驗

5.1 案例分析

目前，大量企業(yè)的RESTful實現(xiàn)對HATEOAS的支持仍相當有限，但e-Bay,Paypal,Twitter等知名廠商在其應(yīng)用中已經(jīng)全面引入了HATEOAS.我們在本節(jié)中，結(jié)合e-Bay的“加入比較列表”(add to watch list)這一服務(wù)實例，來分析本文所提出方法的有效性.這一服務(wù)在被點擊后，其之后的應(yīng)用狀態(tài)交互包括了4個步驟：

針對以上場景的應(yīng)用狀態(tài)，我們首先確定待分析的隱私數(shù)據(jù)集合，以及這些資源操作中牽涉的角色和參與方如下:

參與方集合PA={EB,BI,Twitter,FB,Shipper,User},分別表示e-Bay、商業(yè)智能服務(wù)提供商、Twitter、Facebook、貨運服務(wù)提供商和用戶.

角色集合R={EB,AU,3rd,Seller,Buyer},分別表示e-Bay、認證服務(wù)(包括Twitter和FB)、第3方(包括BI和Shipper)、買房和賣方.

待分析的隱私數(shù)據(jù)項目集合D={name,address,transactionHistory,rateHistory,phone,country,email}，分別表示姓名、地址、交易歷史、評價歷史、電話、國家和電子郵件.

更進一步地，將隱私數(shù)據(jù)項集合D與角色集合相結(jié)合，并針對此實例場景，可得待分析的隱私數(shù)據(jù)集合DA={(Seller,name)，(Buyer,name)，(Seller,address)，(Buyer,address)，(Seller,transactionHistory)，(Seller,rateHistory)，(Buyer,phone)，(Buyer,country)，(Buyer,email)}.

基于以上基礎(chǔ)數(shù)據(jù)，對上述場景所涉及到的資源操作進行自動信息抽取和轉(zhuǎn)化后，可得到本場景中涉及的所有隱私活動(從資源操作涉及的輸入和輸出，共包含25個可能的轉(zhuǎn)換，最終可得非空的隱私活動11個)，考慮到篇幅關(guān)系，我們僅僅列出4個具備代表性的隱私活動如下:

pain(WatchList)=〈{(Seller,name)，(Buyer,name)，Use，(EB,EB)，(EB,EB)，?〉;

pain(RepuStar)=〈{(Seller,name)，(Seller,transactionHistory)，(Seller,rateHistory)}，Use，(3rd,BI)，(3rd,BI)，?〉;

paout(TwitterUser，201)=〈{(Buyer,name)，(Buyer,address)，(Buyer,phone)}，Disclose，(AU,Twitter)，(EB,EB)，twitterAuthorized=true〉;

paout(FBUser，500)=〈{(Buyer,country)}，Disclose，(AU,FB)，(EB,EB)，facebookAuthorized=false〉.

在生成了所有隱私活動集合后，我們可進一步分析上述資源及其所包含的鏈接之間的嵌套關(guān)系，并構(gòu)建資源鏈接關(guān)聯(lián)樹.這一過程由于目前各家廠商鏈接描述的不一致，需要人工干預(yù).本節(jié)場景所對應(yīng)的資源鏈接樹如圖7所示.

根據(jù)圖7所示的資源鏈接關(guān)聯(lián)樹和之前生成的隱私活動集，采用第4節(jié)所提出的轉(zhuǎn)換算法，最終可得上述場景所對應(yīng)的單事件自動機，如圖8所示.

Fig. 7 Resource link mapping tree for e-Bay “add to watch list” service圖7 e-Bay加入比較列表服務(wù)資源鏈接關(guān)聯(lián)樹

Fig. 8 SFA for e-Bay “add to watch list” service圖8 e-Bay加入比較列表服務(wù)單事件確定有限自動機

Fig. 9 Implementation framework for RESTful AS privacy modeling圖9 RESTful應(yīng)用狀態(tài)隱私建模實現(xiàn)框架

5.2 工具實現(xiàn)與實驗

本文理論工作所對應(yīng)的實現(xiàn)框架如圖9所示，我們對其中的模塊和步驟逐一進行解釋:步驟①和②分別從RESTful資源操作描述中抽取出對應(yīng)的內(nèi)嵌資源集和鏈接集合，并交由內(nèi)嵌資源管理器(embedded resource manager)和鏈接管理器(link manager)進行存儲和管理，由于1個內(nèi)嵌資源中可能包含新的鏈接，而1個鏈接又會指向新的資源，因此這一抽取過程必須迭代進行.內(nèi)嵌資源管理器主要管理由HATEOAS特性引發(fā)的內(nèi)部變遷中可能牽涉到的資源操作，而鏈接管理器中則根據(jù)鏈接類別不同，分別存貯協(xié)議級鏈接(protocol link, PL)和超媒體級鏈接(hypermedia link, HL).內(nèi)嵌資源管理器和鏈接管理器之間，通過步驟③進一步建立兩者之間的迭代映射關(guān)系，通過資源鏈接映射模塊(resource link mapping module)生成資源鏈接關(guān)聯(lián)樹(resource link mapping tree).另一方面隱私分析人員確定所需分析的隱私數(shù)據(jù)、參與方、約束等信息，并結(jié)合內(nèi)嵌資源管理器中的資源定義，通過隱私活動生成器(privacy action generator)，生成對應(yīng)每個內(nèi)嵌資源操作的隱私活動列表(步驟④).最后步驟④的輸出結(jié)果和資源鏈接關(guān)聯(lián)樹結(jié)合，通過本文提出的單事件自動機生成算法，在隱私SFA生成器(privacySFAgenerator)中，產(chǎn)生針對RESTful應(yīng)用狀態(tài)的形式化模型(步驟⑤).

針對以上的實現(xiàn)框架，我們開發(fā)了RESTful應(yīng)用狀態(tài)隱私模型的原型工具.該工具采用Eclipse的WindowBuilder插件進行可視化部分開發(fā)，使用MySQL數(shù)據(jù)庫來存儲分析的中間結(jié)果.整個工具的執(zhí)行6個步驟：

1) 在工具中輸入所有此應(yīng)用狀態(tài)中牽涉的資源信息，確定每個資源的輸入和輸出中牽涉的數(shù)據(jù);

2) 結(jié)合領(lǐng)域?qū)＜抑R，標識資源中牽涉到的不同參與方、角色以及待分析的隱私數(shù)據(jù)集，并輸入工具中；

3) 通過分析輸入的資源信息，并和生成的參與方、角色、隱私數(shù)據(jù)集對應(yīng)，按本文中提供的轉(zhuǎn)化方法，由工具自動生成隱私活動集合；

4) 根據(jù)自動追蹤每個資源描述中的鏈接信息,生成資源和鏈接映射關(guān)系的資源鏈接關(guān)聯(lián)樹；

5) 通過本文的算法，轉(zhuǎn)化為SFA單事件自動機，單事件自動機以符合Graphviz工具的文本方式記錄；

Fig. 10 Experimental results of resource link mapping tree圖10 資源鏈接關(guān)聯(lián)樹實驗結(jié)果

6) 通過Graphviz工具可以直接將生成的文本，轉(zhuǎn)換為可見的圖形化自動機形式.

利用上述工具，我們選取了Paypal，Amazon AppStream，Huddle，F(xiàn)oxycart這4個代表性的基于HATEOAS的RESTful服務(wù)提供商從鏈接表征、資源鏈接關(guān)聯(lián)樹生成以及最終生成的SFA模型3個不同的角度開展實驗.

為得到本文所需的資源鏈接關(guān)聯(lián)樹以及對應(yīng)的形式化模型，必須首先對RESTful服務(wù)資源中的鏈接進行分析，表2從鏈接的表示、鏈接的類型以及協(xié)議級鏈接的數(shù)量3個方面對4個不同的服務(wù)提供商開展了分析.

Table 2 Links in Different Service Providers表2 不同服務(wù)提供商的鏈接

Notes: PL stands for protocol link; HL stands for hypermedia link; AL stands for application link; HAL stands for hypertext application language.

從鏈接的表征角度看，目前主要有2種方式：1)通過超文本應(yīng)用語言(hypertext application language, HAL);2)通過服務(wù)提供商自定義的鏈接模型.其中，前者顯示區(qū)分了應(yīng)用級鏈接(以_link表示)和超媒體級鏈接(以_embed表示)且支持嵌套表達；后者則主要通過@rel來界定不同類型的鏈接，其鏈接是屬于應(yīng)用級鏈接還是超媒體級鏈接，需要通過人工干預(yù)進行區(qū)分.在協(xié)議級鏈接的表征上，目前僅有Amazon Appstream顯示界定了哪些返回代碼可作為協(xié)議級鏈接使用(總計14個返回代碼中的6個)，其他提供商或者僅指定了支持的返回代碼(Paypal和Huddle)，或者完全未指定返回代碼(Foxycart).通過以上分析可知，目前由于針對HATEOAS的RESTful服務(wù)尚處于起步階段，尚不具備統(tǒng)一的鏈接分類和表征體系，因此目前在分析資源鏈接關(guān)聯(lián)樹之前，必須通過人工干預(yù)來完成鏈接類型的確定和鏈接的獲取.

在針對不同資源人工標定其不同類型的鏈接后，我們進一步分析其生成的資源鏈接關(guān)聯(lián)樹.圖10(a)～(d)分別為針對4家服務(wù)提供商中的典型RESTful應(yīng)用狀態(tài)生成的資源鏈接關(guān)聯(lián)樹的結(jié)果.圖11為通過工具所分析產(chǎn)生的資源鏈接關(guān)聯(lián)樹的截圖.從圖11中可見，對于類似paypal或amazon這類提供平臺級服務(wù)的廠商，其資源鏈接關(guān)系的嵌套層數(shù)往往較少(paypal最多4層，amazon全部在3層內(nèi)完成)，也即意味著其單一應(yīng)用狀態(tài)中所牽涉的參與方和隱私暴露風(fēng)險相對較少，而對于huddle和foxycart這類應(yīng)用級服務(wù)提供商，其中往往存在較多的資源和鏈接的嵌套關(guān)系，也因此存在著較大的隱私風(fēng)險.

Fig. 11 Screenshot for resource link mapping tree implementation圖11 資源鏈接關(guān)聯(lián)樹工具實現(xiàn)截圖

Fig. 12 Comparison between SFA and resource link mapping tree.圖12 SFA和資源鏈接關(guān)聯(lián)樹比較分析

我們進一步分析所生成的SFA自動機的狀態(tài)和變遷數(shù)與資源鏈接關(guān)聯(lián)樹節(jié)點和邊數(shù)量之間的關(guān)系，圖12(a)為上述4家服務(wù)提供商的18個應(yīng)用狀態(tài)對應(yīng)的資源鏈接關(guān)聯(lián)樹節(jié)點和最終生成的自動機的狀態(tài)數(shù)的對比；圖12(b)為資源鏈接關(guān)聯(lián)樹中的邊數(shù)和自動機的變遷數(shù)的對比.為進行有效比較，我們在生成自動機時假定對上述服務(wù)全部分析同一隱私數(shù)據(jù)集合，并為上述所分析的應(yīng)用狀態(tài)中牽涉的資源逐一指定角色和參與方，從實驗結(jié)果可見，最終生成的自動機的節(jié)點數(shù)和變遷數(shù)總體上和資源鏈接關(guān)聯(lián)樹中的節(jié)點和變遷數(shù)呈線性關(guān)系，這意味著我們在生成形式化模型之前可以通過對資源鏈接關(guān)聯(lián)樹的規(guī)模分析，預(yù)估最終模型的狀態(tài)空間，從而可以在設(shè)計的早期回避可能的狀態(tài)爆炸問題.

6 總結(jié)與未來工作

RESTful服務(wù)借助HTTP協(xié)議的標準動作，提供了一種統(tǒng)一接口的服務(wù)交互方式，作為一種輕量級的SOA實現(xiàn)，其簡單、易伸縮、高兼容的特點，使之迅速成為了云計算和物聯(lián)網(wǎng)等新型體系結(jié)構(gòu)中平臺層和基礎(chǔ)設(shè)施層的事實標準.作為一種底層服務(wù)的提供方式，RESTful服務(wù)不僅需要和其他的RESTful服務(wù)間進行協(xié)作完成業(yè)務(wù)功能，還需要面臨來自不同角色和參與方的服務(wù)請求.如何確保RESTful服務(wù)在這種復(fù)雜的上下文環(huán)境下對于隱私數(shù)據(jù)的操作滿足隱私需求，也隨之成為目前新型計算環(huán)境下隱私保護的最關(guān)鍵問題之一.

本文針對這一問題，采用單事件確定有限自動機對RESTful服務(wù)應(yīng)用狀態(tài)中的隱私活動進行了建模.具體而言，我們首先對RESTful服務(wù)中的隱私活動和資源操作進行了精確的定義.針對隱私活動，我們系統(tǒng)分析了1個隱私操作中所涉及到的數(shù)據(jù)、角色、交互以及約束等元素之間的關(guān)聯(lián)和偏序關(guān)系，給出了隱私活動的元模型及其中每一元素的形式化語義.針對資源操作，我們同樣從涉及到的URI、資源、鏈接等方面對其進行了形式化的描述，并通過一種語義精確的資源鏈接關(guān)聯(lián)樹，表征了1個資源操作所代表的應(yīng)用狀態(tài)中資源和鏈接之間的迭代關(guān)系.在此基礎(chǔ)上，我們討論了資源操作和隱私活動之間的對應(yīng)關(guān)系，建立了RESTful資源操作與對應(yīng)的隱私活動間的映射規(guī)則.更進一步，為了支撐進一步的驗證，我們研究了基于確定有限自動機的RESTful服務(wù)應(yīng)用狀態(tài)的隱私模型，提出了從資源鏈接關(guān)聯(lián)樹向單事件確定有限自動機的轉(zhuǎn)換方法，并給出了算法實現(xiàn).在以上理論工作的基礎(chǔ)上，我們討論了實現(xiàn)上述理論的技術(shù)框架和難點問題，并通過自行開發(fā)的原型工具說明了上述方法的可用性.

本文的方法依然存在一定局限性，這些局限性也將是我們未來工作的重點.形式化驗證的1個最大困難在于狀態(tài)空間的爆炸，在本文建立的模型中，我們并未研究如何對所建立的形式化模型進行有效約簡，在自動機約簡的相關(guān)研究中，已有部分工作利用對自動機中的變遷分類進而將自動機分區(qū)拆分的方式降低自動機的狀態(tài)空間，考慮到我們所驗證的隱私數(shù)據(jù)彼此間往往互相獨立，我們計劃沿著上述工作的思路，對隱私活動形式化模型進行狀態(tài)約簡.另一方面，本文的研究只針對了RESTful服務(wù)的應(yīng)用狀態(tài)建模，而對于1個實際應(yīng)用而言，其往往包含了應(yīng)用狀態(tài)的組合以及RESTful服務(wù)同其他異構(gòu)服務(wù)間的混成.如何有效刻畫這種組合關(guān)系，并將本文所建立的應(yīng)用狀態(tài)模型與組合關(guān)系結(jié)合，確立整個系統(tǒng)的隱私活動模型，也將是我們的未來工作之一.最后，本文的建模工作并未針對具體的RESTful服務(wù)描述語言，我們計劃在未來結(jié)合WADL或WSDL 2.0等常見的RESTful描述語言，更進一步地研究本文工作的可用性.