王 進(jìn) 黃志球

(南京航空航天大學(xué)計(jì)算機(jī)科學(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ù)由于其簡(jiǎn)單、可伸縮和高共享等特性，已經(jīng)越來越多地被應(yīng)用于云計(jì)算、物聯(lián)網(wǎng)等典型的泛在服務(wù)應(yīng)用中[2].截止2013年，RESTful服務(wù)已超過傳統(tǒng)SOAPWS-*Web服務(wù)成為以互聯(lián)網(wǎng)為核心的應(yīng)用系統(tǒng)中使用最廣泛的消息交互方式.

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

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

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

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

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

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

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

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

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

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

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

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

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

1.2 相關(guān)工作

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

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

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

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

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

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

③ 基于形式化方法的建模和驗(yàn)證

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

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

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

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

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

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

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

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

從隱私數(shù)據(jù)的角度，目的(purpose)在所有文獻(xiàn)中都被作為1個(gè)核心元素.文獻(xiàn)[45]中的粒度(granularity)和文獻(xiàn)[4]中的敏感級(jí)別(degrees of sensitivity)都共同表述了隱私數(shù)據(jù)的層次結(jié)構(gòu)和偏序關(guān)系.文獻(xiàn)[45]中的可見性(visibility)、文獻(xiàn)[5]中的數(shù)據(jù)主體(data subject)和數(shù)據(jù)控制者(data controller)以及文獻(xiàn)[5]中的角色和權(quán)限(actors and roles)則都用于表征隱私數(shù)據(jù)的上下文關(guān)系.綜上，我們最終選取3個(gè)屬性作為必須在隱私需求描述語言中涵蓋的關(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)的動(dòng)作和約束的角度，主要可總結(jié)為目的規(guī)約和隱私操作限制2項(xiàng)原則.其中前者主要指明隱私活動(dòng)的目的應(yīng)該與具體的角色和參與方關(guān)聯(lián)，且包含其發(fā)生條件和未來義務(wù)的約束定義；后者則闡述了隱私操作的多樣性.本文隱私活動(dòng)的元模型基于以上分析展開.如圖2所示是本文隱私活動(dòng)的元模型UML類圖，我們?cè)?.2節(jié)將針對(duì)此元模型中不同元素給出其詳細(xì)說明和形式化定義.

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

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

2.2.1 參與方與角色模型

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

為了保證上下文的完整性，我們引入角色和參與方之間進(jìn)行關(guān)聯(lián).設(shè)R為所有角色的集合，角色賦值關(guān)系集合AS是PA×R的1個(gè)子集.考慮到角色之間往往存在層次關(guān)系，我們進(jìn)一步對(duì)不同角色之間的偏序關(guān)系進(jìn)行定義.對(duì)?r1,r2∈R,我們用r1≤r2來表示r2是r1的泛化.例如，角色第3方(the 3rd party)是角色支付服務(wù)(payment service)的1個(gè)泛化.角色賦值集合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ù)項(xiàng)，而將與角色關(guān)聯(lián)后的隱私數(shù)據(jù)項(xiàng)稱為隱私數(shù)據(jù).例如“姓名”為1個(gè)隱私數(shù)據(jù)項(xiàng)，而“家長(zhǎng)的姓名”則為1個(gè)隱私數(shù)據(jù).設(shè)D為所有隱私數(shù)據(jù)項(xiàng)的集合，?d∈D,r∈R,隱私數(shù)據(jù)da=(r,d)∈R×D表示角色r是隱私數(shù)據(jù)項(xiàng)d的數(shù)據(jù)主體.例如，(Parent，Name)和(Child，Name)分別表示家長(zhǎng)的姓名和孩子的姓名.一些隱私數(shù)據(jù)項(xiàng)可以通過某些規(guī)則從另一些隱私項(xiàng)中推理得到，如使用(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個(gè)子集，用于表示DA2中的隱私數(shù)據(jù)可以通過DA1中的隱私數(shù)據(jù)推理得到.

2.2.3 隱私操作模型

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

任意1個(gè)RESTful服務(wù)的資源都可以由URI唯一標(biāo)識(shí)，而1個(gè)資源中又包含了多個(gè)不同操作.這些資源操作既可能針對(duì)不同的HTTP動(dòng)作，也可能針對(duì)同一HTTP動(dòng)作的不同表述.

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

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

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

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

定義5. 鏈接.1個(gè)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}代表此鏈接的不同級(jí)別;condition用于指定此鏈接的發(fā)生條件，對(duì)于協(xié)議級(jí)鏈接，其condition即為對(duì)應(yīng)的HTTP返回代碼，對(duì)于超媒體級(jí)鏈接，其condition則為對(duì)應(yīng)ContentType的是鏈接選擇器所指定的謂詞表達(dá)式.由于鏈接所指向資源的響應(yīng)中又可能會(huì)包含對(duì)新資源的引用，資源和鏈接之間存在著迭代關(guān)系.我們使用資源鏈接關(guān)聯(lián)樹來表示這種多層的迭代關(guān)系，其形式化定義如下:

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

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

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

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

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

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

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

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

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

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

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

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

3.2 資源操作與隱私活動(dòng)的映射

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

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

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

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

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

2) 角色與參與方

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

3) 隱私動(dòng)作

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

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

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

4) 約束

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

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

① 若DaIn(op)≠?∧(method(op)=GET∨method(op)=POST)∧sender(op)≠receiver(op)，則對(duì)應(yīng)隱私活動(dò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)，則對(duì)應(yīng)隱私活動(dò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))，則對(duì)應(yīng)隱私活動(dòng)pa=〈DaIn(op),Use,sender(op),receiver(op),δ(op)〉；

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

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

按照上述對(duì)應(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個(gè)服務(wù)參與方為Online;“Advertise”參與方為Ad_Service;“History”,“DomHistory”,“OverseaHistory”這3個(gè)服務(wù)的參與方為History_Service;關(guān)注的隱私數(shù)據(jù)項(xiàng)集合D={name,location,hobby,history}，則圖3中的RESTful服務(wù)對(duì)應(yīng)的隱私活動(dò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),?〉.

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

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

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

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

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

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

① 構(gòu)造初始狀態(tài)s1、一般狀態(tài)s2和終止?fàn)顟B(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〉.

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

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

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

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

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é)點(diǎn)SFA模型

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

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

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

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

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

① 創(chuàng)建1個(gè)新的非終止?fàn)顟B(tài)sk;

② 刪除所有此HTTP狀態(tài)碼所對(duì)應(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之間標(biāo)記上關(guān)聯(lián)關(guān)系，用函數(shù)Trans(t(de))表示.

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

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

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

② 超媒體級(jí)鏈接的本質(zhì)是在1個(gè)資源操作響應(yīng)中自動(dòng)觸發(fā)對(duì)另一個(gè)資源操作的請(qǐng)求，為此需要在自動(dòng)機(jī)模型中將這2個(gè)資源操作的自動(dòng)機(jī)連接到一起.?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é)點(diǎn)集合，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é)點(diǎn)為源節(jié)點(diǎn)的所有子節(jié)點(diǎn)都將順序執(zhí)行.順序邊的目標(biāo)節(jié)點(diǎn)都僅可能為1個(gè)資源操作，因此僅需要將每個(gè)目標(biāo)節(jié)點(diǎn)對(duì)應(yīng)的自動(dòng)機(jī)簡(jiǎn)單連接在一起，即可完成順序邊的轉(zhuǎn)化.設(shè)節(jié)點(diǎn)n對(duì)應(yīng)的所有順序邊集合為DES(n)?DE，des(i)表示DES(n)中的第i條邊，對(duì)SFA(t(des(i)))和SFA(t(des(i+1)))，我們采用3個(gè)步驟進(jìn)行連接:

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

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

③ 將SFA(t(des(i)))中的終止?fàn)顟B(tài)集SA修改為SFA(t(des(i+1)))的終止?fàn)顟B(tài)集.

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

4) 終止?fàn)顟B(tài)合并

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

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

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

5 案例分析與實(shí)驗(yàn)

5.1 案例分析

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

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

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

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

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

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

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

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〉.

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

根據(jù)圖7所示的資源鏈接關(guān)聯(lián)樹和之前生成的隱私活動(dòng)集，采用第4節(jié)所提出的轉(zhuǎn)換算法，最終可得上述場(chǎng)景所對(duì)應(yīng)的單事件自動(dòng)機(jī)，如圖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ù)單事件確定有限自動(dòng)機(jī)

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

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

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

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

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

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

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

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

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

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

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

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

為得到本文所需的資源鏈接關(guān)聯(lián)樹以及對(duì)應(yīng)的形式化模型，必須首先對(duì)RESTful服務(wù)資源中的鏈接進(jìn)行分析，表2從鏈接的表示、鏈接的類型以及協(xié)議級(jí)鏈接的數(shù)量3個(gè)方面對(duì)4個(gè)不同的服務(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)用級(jí)鏈接(以_link表示)和超媒體級(jí)鏈接(以_embed表示)且支持嵌套表達(dá)；后者則主要通過@rel來界定不同類型的鏈接，其鏈接是屬于應(yīng)用級(jí)鏈接還是超媒體級(jí)鏈接，需要通過人工干預(yù)進(jìn)行區(qū)分.在協(xié)議級(jí)鏈接的表征上，目前僅有Amazon Appstream顯示界定了哪些返回代碼可作為協(xié)議級(jí)鏈接使用(總計(jì)14個(gè)返回代碼中的6個(gè))，其他提供商或者僅指定了支持的返回代碼(Paypal和Huddle)，或者完全未指定返回代碼(Foxycart).通過以上分析可知，目前由于針對(duì)HATEOAS的RESTful服務(wù)尚處于起步階段，尚不具備統(tǒng)一的鏈接分類和表征體系，因此目前在分析資源鏈接關(guān)聯(lián)樹之前，必須通過人工干預(yù)來完成鏈接類型的確定和鏈接的獲取.

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

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

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

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

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

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

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

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