云计算中隐私需求的建模与一致性检测  

Privacy Requirement Modeling and Consistency Checking in Cloud Computing

作　　者：王进[1] 黄志球[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京210016

出　　处：《计算机研究与发展》2015年第10期2395-2410,共16页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(61272083;61262002);江苏省普通高校研究生科研创新计划项目(CXZZ11_0218);南京航空航天大学基本科研业务费专项青年科技创新基金项目(NS2012129)

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

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]