可伸缩性,按需付费以及基于网络的消息传递是云计算的三个核心特征。云计算强调一切皆服务。基础设施层、平台层以及面向最终用户的软件层都被包装为不同形式的服务,并通过不同的交互方式和数据协议完成协作。这种分层可伸缩的协作方式为云计算使用者带来了极大的便利,如:减轻了数据存储管理的负担,具备了与地理位置无关的数据访问能力,避免了硬件、软件等方面的投资损失等。但与此同时,云计算服务提供者(Cloud Service Provider)的中间操作过程对用户透明,用户将丧失对其数据的部分控制权,进而引发了用户对云计算安全与隐私保护的担忧。云计算环境下最终应用是一系列服务的有机聚合。这种聚合,既包括了Web服务组合方式下通过结构化活动对原子服务的编排与编制,也包含了高层服务与底层服务之间的依赖关系。且云计算应用中所涉及的服务往往由不同服务提供商提供,具备跨机构特性,而即使同一服务提供商内部的服务也存在着数据与平台的异构。这种以服务聚合为基础的应用形态,使传统隐私保护方法面临了新的挑战。最终用户的隐私需求往往直接与服务聚合的结构,行为以及参与方相关,而隐私收集与使用目的、暴露方式、保持时间等属性更与应用业务逻辑直接关联,无法通过单一针对数据的加密与检验完成。同时,不同服务提供商难以引入统一的数据保护策略,单一提供商无法强制其他参与方采用相同的数据加密与保护方案,因此难以通过加密和访问控制等传统手段保证多参与方的应用中隐私不出现泄露。为了应对这一挑战,最新的隐私保护规范都将“提供可验证的方式,确保软件的实现满足对应的隐私需求”列为隐私保护需要满足的最重要原则之一。目前针对云计算环境下隐私需求的验证在国内外都尚处于起步阶段,本课题针对这一问题,从支持模型检测的隐私建模方面开展工作,分别对云计算环境下隐私需求的建模方法和云计算系统中静态服务和动态服务的隐私建模方法进行了研究。主要的研究工作包括:(1)提出了隐私活动的元模型以及基于此元模型的隐私需求建模和系统隐私建模框架。支持模型检测的模型要求系统模型和需求模型都基于语义相同的原子命题集合。本文所提出的隐私活动元模型,系统归纳并精化了目前被采纳的隐私保护规范中的核心概念,并进一步分析了这些概念元素之间的关系,给出了其精确的形式语义。在此基础上,讨论了基于隐私活动元模型的隐私需求建模和系统隐私建模的框架。本研究后续工作都围绕此元模型及相关框架展开。(2)在隐私需求的建模方面。提出了一种声明式隐私需求描述语言(Declarative Privacy Policy Language,DPPL),该语言不仅考虑了数据、角色和目的的层次结构,而且通过定义可扩展的声明式约束模板提供了时序约束的表达能力。在此基础上,分析了隐私活动包含关系对最终建模结果的影响,给出了针对该语言定义的隐私需求的形式化建模算法。考虑到传统形式化验证由于空间爆炸而带来的实用性限制,进一步结合隐私活动的特征提出了隐私需求模型的约简方法。最后,通过实例分析和仿真检验了本研究所提出方法的可行性。(3)在云计算静态服务的隐私建模方面。针对SOAP/WS-*服务及其业务流程执行语言BPEL流程的隐私建模开展了研究。首先,对于服务组合流程中SOAP/WS-*原子活动中包含的隐私数据进行了建模分析。其次,提出了一种扩展内部变迁的迁移系统,用以将BPEL里所有可能牵涉隐私活动的变量访问,谓词表达式等都建模为独立的变迁。之后,针对此变迁系统中的每一个变迁进行转换,从数据、目的、参与方和谓词约束4个方面入手,将原有的变迁转换为可能的隐私活动,从而建立起面向隐私活动的BPEL模型。最后,通过案例分析和仿真实验对该方法所建立的模型和原有的BPEL建模结果在状态空间方面进行了比较,以确保该方法的建模结果不会加剧状态空间爆炸。(4)在云计算动态服务的隐私建模方面。针对云计算动态服务的典型代表——Restful服务的应用状态开展隐私建模研究。考虑到由于超媒体作为应用引擎特征而引发的服务内部变迁,提出了一种Restful服务应用状态的隐私模型并研究了从Restful服务描述向此模型的自动转换方法。在该模型中,不仅利用隐私活动的元模型确保了隐私操作的精确刻画,同时形式化定义了Restful服务资源操作、链接等基本概念以及之间的关联关系。最后通过案例分析和实验说明了方法的可用性。(5)根据隐私需求建模和系统隐私建模的理论研究,设计并实现了云计算隐私策略描述和建模,云计算静态服务和动态服务隐私建模的相关原型工具。采用此原型工具,对一个电子商务场景的总额综合案例进行的分析,说明了所提出建模方法的实用性与可用性。