面向超媒體鏈接的RESTful服務隱私建模方法

王 進 黃志球

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

(woodenwang55@hotmail.com)

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

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

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

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

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

2) 建立RESTful服務關鍵概念的精確語義以及RESTful服務中應用狀態和隱私活動間的映射關系；

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

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

同時，在以上理論工作的基礎上結合案例分析和工具實現，對上述方法的可用性展開討論.

1 背景與相關工作

1.1 RESTful服務核心概念

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

Fig. 1 Kernel concepts in RESTful service圖1 RESTful服務核心概念

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

1.2 相關工作

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

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

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

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

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

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

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

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

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

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

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

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

2 RESTful服務中的隱私活動建模

2.1 RESTful服務中隱私活動元模型

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

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

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

2) 數據層次(data hierarchy)定義了隱私數據的結構和偏序關系；

3) 參與方角色(role of participants)定義隱私數據相關的不同參與方和角色層次結構.

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

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

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

2.2.1 參與方與角色模型

RESTful服務應用中存在多參與方，不同參與方又各自承擔著不同的角色.設PA為參與方集合，?pa∈PA，我們用Inst(pa)表示pa的運行時實例.如設用戶(User)是某參與方，Inst(User)則表示某次執行時所關聯的某個具體用戶.

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

2.2.2 隱私數據模型

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

2.2.3 隱私操作模型

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

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

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

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

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

Da?DA是一組關聯了角色的隱私數據；

opr∈OPR×PUR是1個關聯了目的的隱私動作；

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

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

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

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

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

3 RESTful服務資源操作隱私建模

3.1 RESTful服務的形式化語義

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

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

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

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

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

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

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

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

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

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

N?OP∪⊥為節點集合，其中空節點⊥不對應任何資源操作，僅用以表征和后續資源間的關系；

root∈N為根節點，對于表征應用狀態的資源操作，其根節點唯一；

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

CO?DE×CON為觸發條件定義，其中CON為服務響應鏈接集合中所有condition的集合.

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

1) 僅有root無父節點.

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

2)DE中無環.

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

圖3所示服務對應的資源鏈接關聯樹如圖4所示：

Fig. 4 Sample of resource link relation tree圖4 資源鏈接關聯樹示例

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

上述模型中并未包含任何隱私信息，我們進一步分析RESTful服務和2.2.3節隱私活動模型間的對應關系并藉此討論RESTful服務應用狀態的隱私模型.第2節的隱私活動模型中包含了隱私數據項、角色與參與方、隱私動作、和約束4方面內容，我們將其與RESTful服務一一進行對應.

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

1) 隱私數據

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

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

2) 角色與參與方

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

3) 隱私動作

我們在第2節將隱私動作定義為收集、使用、暴露和維持.RESTful服務所使用的HTTP協議動作可以和上述的隱私動作之間形成精確的對應關系如表1所示.

定義1中，對于每個隱私動作還指明了其對應的目的(purpose)，由于目的是1個主觀性較強的定義，無法直接從資源描述中獲取，需要在后續分析過程中，由領域專家和系統設計人員共同人工方式確認.因此由資源描述所生成的隱私活動中不會包含目的.

Table 1 Mapping Relation between Privacy Operation and RESTful Service表1 隱私動作和RESTful服務的對應關系

4) 約束

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

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

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

② ?hc∈HC，若DaOut(op,hc)≠?∧(method(op)=GET∨method(op)=POST)∧sender(op)≠receiver(op)，則對應隱私活動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))，則對應隱私活動pa=〈DaIn(op),Use,sender(op),receiver(op),δ(op)〉；

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

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

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

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),?〉.

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

4 RESTful服務隱私模型的形式化模型

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

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

1) 非空節點轉化

資源鏈接關聯樹中的任意1個非空節點都代表了1個資源操作，對?n∈N∧n≠⊥，其對應資源操作為op∈OP，可經過4個步驟轉化為SFA：

① 構造初始狀態s1、一般狀態s2和終止狀態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〉.

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

算法1. 資源關聯樹節點轉化算法.

輸入:N,Datum;*N為資源關聯樹中的節點集合，Datum為需要分析的隱私數據項集合*

輸出:Map〈n,SFA〉.*n∈N，SFA為此節點對應的單事件自動機*

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 資源鏈接關聯樹非空節點SFA模型

2) 選擇邊轉化

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

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

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

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

① 創建1個新的非終止狀態sk;

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

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

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

⑤ 將t(de)與sk之間標記上關聯關系，用函數Trans(t(de))表示.

在處理完所有協議級鏈接對應的選擇邊后，資源鏈接關聯樹中的所有空節點都會和1個自動機狀態建立關聯.在此基礎上，我們進一步轉化超媒體鏈接的選擇邊.

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

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

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

選擇邊轉化算法如算法2所示，圖6(a)為圖4經過選擇邊轉化后的結果.

算法2. 資源關聯樹選擇邊轉化算法.

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

輸出:Slist.*SList為經過轉化后生成的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) 順序邊轉化

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

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

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

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

圖6(b)為圖4經過順序邊轉化后的結果.

4) 終止狀態合并

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

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

Fig. 6 Transformation from resource-link mapping tree to SFA圖6 從資源鏈接關聯樹向SFA轉換示例

5 案例分析與實驗

5.1 案例分析

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

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

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

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

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

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

基于以上基礎數據，對上述場景所涉及到的資源操作進行自動信息抽取和轉化后，可得到本場景中涉及的所有隱私活動(從資源操作涉及的輸入和輸出，共包含25個可能的轉換，最終可得非空的隱私活動11個)，考慮到篇幅關系，我們僅僅列出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〉.

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

根據圖7所示的資源鏈接關聯樹和之前生成的隱私活動集，采用第4節所提出的轉換算法，最終可得上述場景所對應的單事件自動機，如圖8所示.

Fig. 7 Resource link mapping tree for e-Bay “add to watch list” service圖7 e-Bay加入比較列表服務資源鏈接關聯樹

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

Fig. 9 Implementation framework for RESTful AS privacy modeling圖9 RESTful應用狀態隱私建模實現框架

5.2 工具實現與實驗

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

針對以上的實現框架，我們開發了RESTful應用狀態隱私模型的原型工具.該工具采用Eclipse的WindowBuilder插件進行可視化部分開發，使用MySQL數據庫來存儲分析的中間結果.整個工具的執行6個步驟：

1) 在工具中輸入所有此應用狀態中牽涉的資源信息，確定每個資源的輸入和輸出中牽涉的數據;

2) 結合領域專家知識，標識資源中牽涉到的不同參與方、角色以及待分析的隱私數據集，并輸入工具中；

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

4) 根據自動追蹤每個資源描述中的鏈接信息,生成資源和鏈接映射關系的資源鏈接關聯樹；

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

Fig. 10 Experimental results of resource link mapping tree圖10 資源鏈接關聯樹實驗結果

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

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

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

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

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

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

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

Fig. 11 Screenshot for resource link mapping tree implementation圖11 資源鏈接關聯樹工具實現截圖

Fig. 12 Comparison between SFA and resource link mapping tree.圖12 SFA和資源鏈接關聯樹比較分析

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

6 總結與未來工作

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

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

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