ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2015, Vol. 52 ›› Issue (10): 2395-2410.doi: 10.7544/issn1000-1239.2015.20150513

所属专题: 2015网络安全与隐私保护研究进展

• 信息安全 • 上一篇    下一篇



  1. (南京航空航天大学计算机科学与技术学院 南京 210016) (
  • 出版日期: 2015-10-01
  • 基金资助: 

Privacy Requirement Modeling and Consistency Checking in Cloud Computing

Wang Jin, Huang Zhiqiu   

  1. (College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016)
  • Online: 2015-10-01

摘要: 云计算中应用分层、服务外包以及数据的分布存储等特性引发了隐私保护的新挑战.如何刻画不同服务提供者的隐私需求,并保证不同参与方隐私需求在全局应用上一致无冲突是云计算隐私保护的一个核心问题.在对隐私需求的分类和建模目标系统分析后,提出了一种综合考虑了数据、角色和目的的层次结构,并支持时序约束表达的声明式隐私需求描述语言DPPL.为验证不同隐私需求间的一致性,给出了该语言的形式化语义及对应的形式化建模算法.考虑到传统形式化验证由于空间爆炸而带来的实用性限制,进一步结合隐私活动的特征提出了隐私需求模型的约简方法.最后,通过实例分析和原型工具检验了所提出方法的可行性,并对于该方法目前尚存在的限制和未来工作进行了讨论.

关键词: 云计算, 隐私需求, 形式化模型, 需求约简, 声明式语言

Abstract: As a scalable and hierarchical distributed collaboration paradigm, cloud computing is envisioned as a XaaS (X as a service) architecture, combined with the advantage of reducing cost by sharing computing and storage resources. Although there is a large push towards cloud computing, privacy issues are the major challenges which inhibit the cloud computing wide acceptance in practice. How to precisely describe the privacy requirement and guarantee the privacy requirement among different participants consistent with each other are two key issues in cloud computing privacy protection. Based on systematical analysis of the privacy requirement classification and design goals, a declarative privacy policy language, DPPL, is proposed with its formal semantics. This language not only considers the hierarchical structure of the privacy datum, role and purpose, but also presents a series of declarative event templates to support the temporal constraints. To verify the consistency of different privacy requirements, the single-event finite automaton model for DPPL and its generation algorithm are given. Furthermore, to mediate the space explosion dilemma in traditional formal verification, the requirement model reduction rules based on the relationship among privacy actions are stated. Finally, we evaluate our approach with the case study and prototype implementation, and certify the correctness and feasibility of our method.

Key words: cloud computing, privacy requirement, formal model, requirement reduction, declarative language