Privacy Requirement Modeling and Consistency Checking in Cloud Computing

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.