面向超媒体链接的RESTful服务隐私建模方法
2017-11-07黄志球
王 进 黄志球
(南京航空航天大学计算机科学与技术学院 南京 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描述了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 资源链接关联树示例 上述模型中并未包含任何隐私信息，我们进一步分析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),∅〉. 这个从资源描述中所生成的隐私活动并不包含目的，如果在后续分析中需要单独基于隐私动作的目的进行分析，则尚需要在上述生成的隐私活动中，手动为每个活动中的隐私动作指定目的(由于本文的后续部分不涉及到基于目的的分析，我们直接使用从资源描述中生成的隐私活动集合). 为进一步开展面向隐私属性的验证与分析，我们需要将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)))∨ 则表示此边上条件约束所代表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转换示例 目前，大量企业的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应用状态隐私建模实现框架 本文理论工作所对应的实现框架如图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)为资源链接关联树中的边数和自动机的变迁数的对比.为进行有效比较，我们在生成自动机时假定对上述服务全部分析同一隐私数据集合，并为上述所分析的应用状态中牵涉的资源逐一指定角色和参与方，从实验结果可见，最终生成的自动机的节点数和变迁数总体上和资源链接关联树中的节点和变迁数呈线性关系，这意味着我们在生成形式化模型之前可以通过对资源链接关联树的规模分析，预估最终模型的状态空间，从而可以在设计的早期回避可能的状态爆炸问题. RESTful服务借助HTTP协议的标准动作，提供了一种统一接口的服务交互方式，作为一种轻量级的SOA实现，其简单、易伸缩、高兼容的特点，使之迅速成为了云计算和物联网等新型体系结构中平台层和基础设施层的事实标准.作为一种底层服务的提供方式，RESTful服务不仅需要和其他的RESTful服务间进行协作完成业务功能，还需要面临来自不同角色和参与方的服务请求.如何确保RESTful服务在这种复杂的上下文环境下对于隐私数据的操作满足隐私需求，也随之成为目前新型计算环境下隐私保护的最关键问题之一. 本文针对这一问题，采用单事件确定有限自动机对RESTful服务应用状态中的隐私活动进行了建模.具体而言，我们首先对RESTful服务中的隐私活动和资源操作进行了精确的定义.针对隐私活动，我们系统分析了1个隐私操作中所涉及到的数据、角色、交互以及约束等元素之间的关联和偏序关系，给出了隐私活动的元模型及其中每一元素的形式化语义.针对资源操作，我们同样从涉及到的URI、资源、链接等方面对其进行了形式化的描述，并通过一种语义精确的资源链接关联树，表征了1个资源操作所代表的应用状态中资源和链接之间的迭代关系.在此基础上，我们讨论了资源操作和隐私活动之间的对应关系，建立了RESTful资源操作与对应的隐私活动间的映射规则.更进一步，为了支撑进一步的验证，我们研究了基于确定有限自动机的RESTful服务应用状态的隐私模型，提出了从资源链接关联树向单事件确定有限自动机的转换方法，并给出了算法实现.在以上理论工作的基础上，我们讨论了实现上述理论的技术框架和难点问题，并通过自行开发的原型工具说明了上述方法的可用性. 本文的方法依然存在一定局限性，这些局限性也将是我们未来工作的重点.形式化验证的1个最大困难在于状态空间的爆炸，在本文建立的模型中，我们并未研究如何对所建立的形式化模型进行有效约简，在自动机约简的相关研究中，已有部分工作利用对自动机中的变迁分类进而将自动机分区拆分的方式降低自动机的状态空间，考虑到我们所验证的隐私数据彼此间往往互相独立，我们计划沿着上述工作的思路，对隐私活动形式化模型进行状态约简.另一方面，本文的研究只针对了RESTful服务的应用状态建模，而对于1个实际应用而言，其往往包含了应用状态的组合以及RESTful服务同其他异构服务间的混成.如何有效刻画这种组合关系，并将本文所建立的应用状态模型与组合关系结合，确立整个系统的隐私活动模型，也将是我们的未来工作之一.最后，本文的建模工作并未针对具体的RESTful服务描述语言，我们计划在未来结合WADL或WSDL 2.0等常见的RESTful描述语言，更进一步地研究本文工作的可用性.
3 RESTful服务资源操作隐私建模
3.1 RESTful服务的形式化语义
3.2 资源操作与隐私活动的映射
4 RESTful服务隐私模型的形式化模型
〈s2,(ε,co(de)),s3〉∈δ(SFA(s(de)))，
5 案例分析与实验
5.1 案例分析
5.2 工具实现与实验
6 总结与未来工作
