Research On Model Checking Supportive Privacy Modeling Method In Cloud Computing

Scalability,pay-as-you-go and network-based message delivery is three core characteristics of 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,security and privacy are the major challenges which inhibit the cloud computing wide acceptance in practice.Different from the traditional architecture in which users have full control of their privacy data,the internal operations of cloud computing software systems are usually transparent to the user and once the privacy data of the users are collected,they will lose control over it.Unlike the SOA(Service-Oriented Architecture)and component based software in which the information exchanging mechanisms among services or components are clear and definite,the cloud computing system usually combines hierarchical and heterogeneous services provided by multiple organizations.On the one hand,the services in different layers(IaaS,PaaS and SaaS-Infrastructure,Platform and Software as a Service respectively),may rely on different protocols and message formats.For example,the majority of the services in the infrastructure and platform layer are stateless Restful services based on HTTP protocol.The services in the software layer,however,mostly adopt SOAP/WS-* web services which can represent business flow more clearly.On the other hand,the cloud system is generally the collaboration of services which consists not only the composition of services in same layer but also the assembling with multiple participants from the different layers.The characteristic of cloud computing makes the traditional promising technologies such as access control,Chinese wall and homomorphic encryption are unable to properly resolve the security and privacy challenges.Providing verifiable mechanism to ensure the practice of software compliant with the privacy requirement is one of the most important principles in privacy related standards and regulations such as OECD and ISO29100.To solve the above-mentioned issue,this dissertation proposes the methods to establish the formal model of privacy requirement and system implementation in cloud computing,which can support further verification process.The specific research works can be listed as follows.(1)The start point of our solution is to precisely describe privacy actions and constraints.Based on refinement of current privacy protection standards and regulations,we systematically analyze the partial order relation among privacy datum,roles and purposes and define the meta-model of privacy action as a basis for the privacy related model checking.A Privacy requirement modeling and privacy-oriented system modeling architecture are then proposed based on that meta-model.(2)In privacy requirement modeling aspect,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 were given.Furthermore,to mediate the space explosion dilemma in traditional formal verification,the requirement model reduction rules based on 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.(3)In static service privacy modeling aspect,we focus on the most adopted process definition language,BPEL.We present a privacy action-oriented BPEL process modeling method.This approach not only considers the privacy actions caused by basic and structural activities in BPEL,but also analyzes the different roles and participants.We define a formal transition system that considers roles and internal transitions and propose a privacy action model generation method based on the formal transition system and privacy action meta-model.(4)In dynamic service privacy modeling aspect,we foucs on Restful service.Acknowledging the hypermedia nature of RESTful service,we present a Restful application state privacy model based on single-event finite automaton and discuss the automatical transformation method from Restful service description to that formal model.We formally define some kernel elements of Restful service and discuss how to transform the Restful service resources to the corresponding privacy actions.In addition,we propose a new data structure called resource link mapping tree to represent the relationship between the Restful service resources and links.A transformation method based on the resource link mapping tree is introduced to generate the corresponding privacy actions from the Restful service definition and further generate the formal single-event automata.We finally use a case-study based on our prototype tools to show the feasibility of our approach.(5)Based on the theoretical analyzing result,we further design and implement the prototype system and illustrate the feasibility and practicality with simulation experiments.