=Paper=
{{Paper
|id=Vol-1531/paper3
|storemode=property
|title=Privacy Requirement Modeling and Verification in Cloud Computing
|pdfUrl=https://ceur-ws.org/Vol-1531/paper3.pdf
|volume=Vol-1531
|dblpUrl=https://dblp.org/rec/conf/models/Wang15
}}
==Privacy Requirement Modeling and Verification in Cloud Computing==
https://ceur-ws.org/Vol-1531/paper3.pdf
Privacy Requirement Modeling and Verification in
Cloud Computing
Jin, Wang
College of Computer Science and Technology
Nanjing University of Aeronautics and Astronautics
Nanjing, China
woodenwang55@hotmail.com
Abstract—Cloud computing, the architecture which shares regulations such as OECD [6] and ISO29100 [7]. The issues
dynamic heterogeneous characteristics in the cross-layer service appearing in this principle are manifold.
composition, has affected traditional security, trust and privacy Firstly, we need an approach to precisely describe the
mechanisms which are mainly based on data encryption and privacy requirement. On the one hand, due to the ambiguous
access control. Approaches that can support accurate privacy
requirement description and verifiable compliance between the
and inconsistent essence, natural language is essentially
privacy requirement and system practice need to be developed to unusable to depict a user concerned privacy requirement. On
fit this new paradigm. To tackle the issues of privacy the other hand, directly using a specification language, such as
requirement modeling and verification in cloud computing, a Linear Temporal Logic (LTL) and Description Logics (DL), is
framework that supports model checking consistency, entailment too complicated to be implemented by the requirements
and compliance with the formal definition of privacy analysts and system designers. Therefore, we must establish
requirements and privacy model of cloud application is proposed. one privacy requirement description method that can make a
This paper provides an overview of the scientific research balance between the expressiveness and the applicability.
problem, approaches to solve the problem and ways to evaluate
the solution found by the research related PhD thesis.
Secondly, considering the multi-participant and outsource
Keywords—Cloud computing, privacy requirement, model nature of cloud computing, we must guarantee there is no
checking, formal model conflict among different participants which means the privacy
requirement among different participants should be
I. PROBLEM consistent with each other.
Thirdly, some laws and regulations in different
Scalability, on-demand access and network-based message application contexts, such as the Children Online Privacy
delivery are three core characteristics of cloud computing [1]. Protection Act (COPPA), the Health Information Portability
As a scalable and hierarchical distributed collaboration and Accountability Act (HIPAA) and the Gramm–Leach–
paradigm, cloud computing is envisioned as an XaaS (X As a Bliley Act (GLBA), are proposed to enforce the privacy
Service) architecture, combined with the advantage of reducing requirements of each participant and we must make sure the
cost by sharing computing and storage resources [2]. Although privacy requirements entail certain privacy regulations and
there is a large push towards cloud computing, security and laws.
privacy are the major challenges which inhibit the cloud Finally, we need to verify the compliance between the
computing’s wide acceptance in practice. A survey conducted cloud computing system practice and requirements. To
by the US Government Accountability Office (GAO) states support the verification, a formal model of privacy
that “22 of 24 major federal agencies reported that they were requirements and the specified cloud computing privacy model
either concerned or very concerned about the potential are needed. Moreover, to overcome the space explosion
information security and privacy risks associated with cloud dilemma in traditional model checking, there should be some
computing” [3]. Different from the traditional architecture in reduction method to make our verification represent real-life
which users have full control of their privacy data, the internal systems and not just toy examples.
operations of cloud computing software systems are usually
transparent to the users and once the privacy data of the users II. RELATED WORK
are collected, they will lose control over it.
The essence of privacy protection in cloud computing is the A. Privacy Requirement Description
rights and obligations of individuals and service providers with Current privacy policy definition methods can be classified
respect to the collection, use, disclosure, and retention of PII into four categories, access control model based on
(Personally Identifiable Information) [4,5]. Providing verifiable RBAC(Role-Based Access Control), access control models
mechanism in design phase to ensure that the practice of using Markup Language, Semantic-web policy frameworks
software is compliant with the privacy requirement is one of using description logic and declarative language with formal
the most important principles in privacy related standards and semantics.
For the first category, RBAC is an access control model in a very limited scale. Barth et al. [17] propose a Linear
which access rights are specified in terms of roles. As an access Temporal Logic (LTL) based framework CI (Contextual
control model, RBAC lacks the notion of privacy data and Integrity) for expressing and reasoning about norms of
purpose and is insufficient for directly modeling privacy policy. transmission of personal information. This method describes
Privacy-Aware Role-Based Access Control (PARBAC) model requirements with the logic formula directly which are proven
[8] notices the partial relations in roles, purpose and data too awkward to implement by the requirement analyzer and do
subject and combined RBAC with Chandramouli’s DAFMAT not have the feasibility of reality. S4P, a declarative language
framework. There is no formal semantics about the relations to express privacy preferences and policies are proposed in [18].
and interactions in the model, therefore consistency and The method provides a formal semantics and proof rules for
compliance checking is not feasible with it. P-RBAC [9], is the their language. S4P is at a higher abstraction level than our
first privacy data centric RBAC expansion. However, the work. The purpose of S4P is to check the consistency between
authors did not present any formal model for the condition and user preference and privacy policy.
obligation except the policy in natural language which makes
B. Privacy Requirement Verification
that policy unusable for verifying compliance and can only
check the consistency in a limited context. Y. Li et al. [19] establish the mapping between business
For access control models using Markup Language, process execution language (BPEL) and P3P policy and verify
XACML defines a general-purpose access control system and the privacy requirements in P3P. A state machine based
provides a privacy profile in [10]. XACML leaves obligation model is proposed and extended to monitor the compliance of
interpretation and rule conflict detection to the application. privacy agreements and verify the time properties in privacy
Therefore, the semantics of an XACML policy cannot be fully requirements at the runtime [20,21]. Barth et. al [22] use LTL
specified by the policy itself which makes the formal semantics formula to depict and verify privacy properties in service
rely on specified application and cannot do the consistency and composition. Our team also does research on privacy modeling
compliance checking with the model itself. IBM proposed a and verification with interface automaton and hyper-graph.
language called EPAL [11] to encode privacy policies. Similar These works, however, mostly focus on the SOAP web service
to XACML, the language is based on XML and uses a set of and do not consider the hierarchical and the heterogeneous
attributes called vocabularies. The main issue about EPAL is feature of cloud computing.
that the obligation definition is natural language based and hard C. Cloud Computing Modeling and Verification
to expand to support formal semantics. The Platform for
Privacy Preferences (P3P) is a privacy language intended for In Cloud computing environments, different types of
use by web site operators in informing their visitors of their services co-exist and collaborate with each other to offer a final
data practices [12]. P3P policies were not originally intended to system. Numerous studies have already been carried out on
describe the exchange of privacy data among multi participants modeling the most common cloud computing service, Restful
context. In describing data collection requirements, all and SOAP services, and their combination. In Restful Service
requirements in P3P are categorical with fixed options which modeling, some semi-formal and formal models, such as UML
makes it impossible to expand to adapt different domains and state diagram, Petri Net and finite state machine, are proposed
application contexts. P3P also lacks a formal semantics, which to depict the Restful service from different aspects. In SOAP
may have led to language misuse. service modeling, some standards, such as BPEL and WS-
CDL, have been proposed to reduce the complexity required to
For Semantic-web policy frameworks, naturally, the Web
Ontology Language (OWL) and its predecessors can depict compose web services, hence reducing time and costs, and
classification hierarchies with data type constraints. The increase overall efficiency in businesses. To verify functional
and non-functional properties, these standards are further
Description logic behind those languages is a subset of first-
extended and formalized by transition system [29], process
order logic for expressing knowledge. Some frameworks such
algebra [30] and Petri Net [31]. Some research realize the
as KAoS [13] and Rei [14] that contains an OWL policy
ontology are proposed for expressing rights, prohibitions, and cross-layer service composition nature of cloud computing and
obligations. Eddy [15] further extends previous work with the propose some approaches to analyze different aspects ranging
from resource management model [32] to information store
formal model and consistency checking method. Bearing on the
model [33]. None of the aforementioned approaches focus on
limitation of Description logic, these methods cannot describe
privacy analysis which makes modeling privacy properties in
temporal constraints and can hardly work with the data
cloud computing still an open challenge.
implementation model of a specified system to check the
compliance. III. PROPOSED SOLUTION
For declarative language with formal semantics, May et al.
[16] introduce privacy APIs, which is a logical framework that To mitigate the aforementioned challenges in Section I, an
includes a language to express permissions using commands. approach considering four aspects, i.e., definition,
The policies are further formalized in the Promela model- formalization, reduction and verification, respectively, is
checking language and can be checked using the model checker proposed.
SPIN. However, the only temporal constraints in this method On the privacy requirement side, the start point of our
are “Opt-In” and “Opt-Out” that restricts the expressiveness to 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 TABLE1 EVENT TEMPLATE EXAMPLES
relation among privacy datum, roles and purposes and define Template Description LTL Mapping
Least(n, a) a will occur at least n ◇(a∧○( Least(n-1,a) )
the meta-model of privacy action(Fig 1) as a basis for the times.
privacy model checking. Response(a, b) Every a is eventually (a ◇(b))
followed by at least
one b.
MultiOptionResp If a occurs, there must (a ◇(b1 b2 ... bn))
(a, B) be at least one privacy
action in B occurs
after a.
formal model that can map privacy action and atomic service
request/response are stated. For SOAP service, this mapping is
apparent and directly based on WSDL description. For Restful
service, on the other hand, the HATEOAS (Hypermedia As
The Engine Of Application State) constraint makes the internal
transition more complex. To correctly represent those
transitions caused by the iteration relation between resources
and links, our approach defines a resource link mapping tree
and then transforms that tree to the automaton. Furthermore, a
cross-layer interaction model will be created based on the
Fig 1 Privacy Action meta model. atomic service model and control flow.
To express the occurrence condition and obligations of One of the most severe challenges for verifying the cross-
privacy action, we further design three categories of event layer model is the state space explosion. The state space for 30
templates, EXISTENCE, BINARY RELATION and PLURAL services composition can reach 106 or more which makes
RELATION, respectively. The declarative nature of our event verifying real-life cases impossible before reduction. In our
templates makes them easy to use by privacy analyzers. To approach, both the privacy requirement and the privacy
support the formal verification, we map each event to the operations of the cloud computing system can be formalized as
corresponding LTL formula. Table 1 are some typical events a transition system where the privacy actions are used as the
and their corresponding LTL mapping. Considering the transition guards. A lot of elements in privacy actions are
influence of partial order relations, we also give the formal disjoint with each other, privacy datum and participant for
definition and detection algorithm of privacy action inclusion example. Taking advantage of these disjoint elements, we can
relationship. Different from traditional LTL formulas which achieve the partial model from the original formal model. For
can monitor two or more properties simultaneously, our model example, the privacy datum set we want to verify is { name,
is safely assumed to be a single event system. Using generated address, email }, we can obtain the sub-models for name ,
LTL formula and inclusion relationship, we can finally achieve address and email respectively and just check each sub-model
the single event finite automaton to do the consistency and instead of checking the whole formal model. To generate the
entailment checking. sub-model of one specified privacy datum, we firstly get all the
Let us take one key constraint , “Online Service does not privacy actions containing that privacy datum. Then we
collect personal information from any visitor prior to collecting analyze the transitions that will affect or be affected by these
age information”, in §312. 2 of COPPA as an example. With privacy actions and finally remove those transitions which have
our language, this term can be represented by two privacy no relation to the specified privacy datum from the original
actions and one event constraint as follow ( we use T to formal model.
represent universal set and \ for relative complement , OS and IV. PRELIMINARY WORK
SP are the abbreviation of Online Service and Service
Provider): We started our work by examining the minimum privacy
p1 = <{(User, age) },(Collect, T), (Operator, User), disclosure in SOA architecture [23]. When analyzing the state
( OS,SP),Φ> of art privacy regulations and standards, we realized most
current privacy requirement definition methods lack a
p2 = <{(User, PII \ age)},(Collect, T), (Operator, User),
theoretical foundation and therefore is not amenable to
(OS, SP),Φ>
verification or reasoning. Futhermore, developed from SOA,
e1= Prior( p1, p2) cloud computing introduces multi-layer and heterogeneous
On the cloud computing system side, when services in SaaS service collaboration which makes privacy protection a more
usually use SOAP/WS-*, most products in IaaS and PaaS, such complex challenge. We list most relevant up-to-date work and
as OCCI, OpenStack, mOSAIC, Google Map, Yahoo!Local, achieved results as below:
are Restful service based. To verify the privacy requirement in - We have introduced an XML based privacy requirement
cloud computing system, we need to formally define these two language which preliminarily approaches the problem of
kinds of service and present a model can depict the multi-layer expressing temporal constraints [24]. To give the privacy
collaboration between these heterogeneous services. Firstly, a requirement more precise and formal semantics, we
further defined a declarative privacy policy language with correctness, we plan to conduct an experiment using the same
its formal model [25]; data in [15] and compare our conflict detection result with
- We have focused on the privacy data in SOAP and theirs.
Restful service and established the formal privacy model At the feasibility side, we intend to conduct a set of real
for these two types of services [26,27] which are the basis case study to model COPPA, HIPAA and the policies from the
of cloud computing; related service providers to check the limitation of our privacy
- We have analyzed the privacy data with the predicate requirements modeling method and determine which kind of
constraints in SOAP service composition and get a policies can be or cannot be modeled with our approach.
feasible path generation method that can support our Furthermore, we aim to model some open-source cloud
future verification [28]. computing applications which include both Restful and SOAP
- We have conducted a study aimed at reducing the state service interactions to analyze the compliance of the privacy
space of privacy requirement and verifying the requirement.
consistency among different privacy requirements [25]. At the performance side, we intend to conduct several
experiments based on the benchmark from [34] and to
V. EXPECTED CONTRIBUTIONS investigate the following indicators:
We are currently working on several directions, that will − Number of specifications
address the following contributions. − Number of privacy datum items;
From the privacy requirement modeling aspect, a privacy − Number of constraints
action meta-model and declarative requirements definition − Number of privacy action inclusion constraints;
language are proposed. Constraints templates and their LTL − Number of application states in cloud system
mapping are stated to support formal specification generation.
A Formal semantics of that language based on an automaton VII. CURRENT STATUS
are established to support further model checking. The privacy Currently, we are proposing a declarative privacy policy
action inclusion relationships are introduced to reduce the state language with the formal semantics that is expected to be the
space in model checking. input of our further consistency and entailment verification.
From the cloud computing privacy modeling aspect, the The case study and performance evaluation will be performed
privacy model for most common service –Restful and SOAP - in parallel with our theoretical research. To finalize our work,
in cloud computing are proposed based on mapping between we identify the following tasks that will lead to a Ph.D.
system behavior and privacy action. A formal model dissertation. The planned timeline in terms of the expected
supporting multi-layer structure and heterogeneous service contributions and current status (dash line) is shown in Figure 2.
collaboration in cloud computing will be represented based on
Restful and SOAP privacy model.
From the privacy requirement verification aspect, an
automaton partition method will be presented to mediate the
state space explosion issue in model checking. A series of
prototype toolkits will be implemented to provide semi-
automated privacy data extraction, privacy requirement
definition and verification.
The main contribution can be summarized as follows.
- A declarative privacy requirement language with
formal semantics
- A formal privacy model for cloud computing Fig. 2: Planned timeline and current status
- A model checking Reduction method based on
transition relationship and privacy datum feature. • To model the privacy requirement with the formal
semantics (T1);
VI. PLAN FOR EVALUATION AND VALIDATION • To verify the consistency of privacy requirements
We plan to validate and evaluate our work from three based on reduction formal specification (T2);
aspects: correctness, feasibility and performance. • To provide a verification approach for the entailment
At the correctness side, to measure the expressive power of of privacy regulation and laws (T3);
our privacy requirements modeling approach, we will compare • To define mappings between cloud computing
our method with other related works using the following behavior and privacy action (T4);
criterias: Hierarchical data structure support, Role support, • To study the privacy model of cloud computing that
Purpose Specification support, Temporal constraints support, can reflect the hierarchical and heterogeneous
Privacy operation definition support, Compliance checking characteristics (T5);
support, Consistency checking support and User readable. • To implement a semi-automated privacy framework
Those criterias are retrived from the OECD, ISO 29100 and for supporting to extract privacy, data definition from
other related standards. To evaluate the verification the system (T6);
• To evaluate our work by case study and performance [17] A. Barth, A. Datta, J. Mitchell, and H. Nissenbaum. Privacy and
experiment (T7); contextual integrity: Framework and applications, In IEEE
Symposium on Security and Privacy, pages 184-198, 2006.
• To finish the Ph.D. thesis and dissertation (T8). [18] M. Y. Becker, A. Malkis, L. Bussard, S4P: A generic language
for specifying privacy preferences and policies, Technical
Report MSR-TR-2010-32, Microsoft Research, 2010.
ACKNOWLEDGMENT [19] Y. Li, S. Benbernou, H. Paik, and B. Benatallah. Formal
This research has been supported by This work is consistency verification between bpel process and privacy policy.
Proc of Privacy Security Trust PST’2006. New York, NY, USA :
supported in part by the National Science Foundation of China ACM 2006 : 212–224.
under grants (No.61272083, No.61373137, No.61373017) [20] Salima Benbernou, Hassina Meziane, Mohand-Said Hacid. Run-
Time Monitoring for Privacy-Agreement Compliance. LNCS
REFERENCES 4749 : Proc of ICSOC 2007, Berlin: Springer,2007: 353-364.
[1] Foster, Ian, et al. "Cloud computing and grid computing 360- [21] Karima Mokhtari, Salima Benbernou, Mohand-Said Hacid,
degree compared." Grid Computing Environments Workshop, Emmanuel Coquery, Frank Leymann. Verification of Privacy
Timed Properties in Web Service Protocols. Proc of IEEE SCC
2008. GCE'08. Ieee, 2008. 2008, Washington: IEEE 2008: 593-594.
[2] Fox, Armando, et al. Above the clouds: A Berkeley view of [22] Adam Barth, John Mitchell, Anupam Datta, and Sharada
cloud computing. Dept. Electrical Eng. and Comput. Sciences, Sundaram. Privacy and utility in business processes. Proc of
University of California, Berkeley, Rep. UCB/EECS 28 (2009). Computer Security Foundations Symposium, Washington: IEEE,
[3] GAO, “Information Security: Additional Guidance Needed to 2007:279–294.
AddressCloud Computing Concerns,” United States [23] Liu, Linyuan, Haibin Zhu, and Zhiqiu Huang. "Analysis of the
Government Accountability Office (GAO), October 6, 2011. minimal privacy disclosure for web services collaborations with
[4] Pearson, Siani. "Taking account of privacy when designing role mechanisms." Expert Systems with Applications 38.4
cloud computing services." Proceedings of the 2009 ICSE (2011): 4540-4549.
Workshop on Software Engineering Challenges of Cloud [24] Lu Jiajun, Huang Zhiqiu, Wang Jin, et al. Behavior-oriented
Computing. IEEE Computer Society, 2009. privacy policy description for Web services composition.
[5] Pearson, Siani, and Andrew Charlesworth. "Accountability as a Journal of Frontiers of Computer Science and
way forward for privacy protection in the cloud." Cloud Technology,2013,7(7)：592-601.
computing. Springer Berlin Heidelberg, 2009. 131-144.
[25] Wang Jin, Huang Zhiqiu. Privacy Requirement Modeling and
[6] Organisation for Economic Co-operation and Consistency Checking in Cloud Computing. Journal of
Development. OECD Guidelines on the Protection of Privacy Computer Research and Development. 2015, 52(10).
and Transborder Flows of Personal Data. OECD Publishing, [26] Cai Zheng-ping, Huang Zhi-Qiu, Wang Jin, et. al. Research of
2002. Web Services Composition Transaction Coordination
[7] ISO/IEC 29100. Information technology – Security techniques– Framework based on BPEL and WS-TX. Computer Science.
Privacy framework. ISO/IEC 29100 (1st edition), 2011. 39.6 (2012): 120-124.
[8] Q. He. Privacy enforcement with an extended role-based access [27] Tie Wei, Huang Zhi-Qiu, Wang Jin. BPEL based asynchronous
control model, NCSU Computer Science Technical Report TR- interaction and composition of RESTful Web Service. Computer
2003-09, 2003.
Engineering & Science. 35.4 (2013): 29-36.
[9] Q. Ni, E. Bertino & J. Lobo,“An Obligation Model Bridging
Access Control Policies and Privacy Policies,” in Proc. of ACM [28] Wang Jin, Huang Zhi-qiu ,Tang Jiajun, et. al. Predicate
SACMAT, pp.133-142, 2008. Constraint Oriented BPEL Modeling and Feasible Path Analysis.
Journal of Computer Research and Development. 2015, 51(4):
[10] OASIS. XACML’s Privacy profile. Available: 838-847.
http://www.oasisopen.org/committees/document.php?document
_id=37643&wg_abbrev=xacml [29] Foster H, Uchitel S, Magee J, et al . Model-based verification of
[11] P. Ashley et al.,“Enterprise Privacy Authorization Language web service compositions. Proc of 18th IEEE Int Conf on
(EPAL),” Research Report RZ 3485, IBM Research, 2003. Automated Software Engineering. Piscataway, NJ: IEEE, 2003:
[12] Cranor L et al, Platform for privacy preferences (P3P) 152-163
specification. W3C working group note,2006 [30] Ferrara A. Web services: A process algebra approach. Proc of
[13] Uszok A, Bradshaw JM, Lott J, Breedy M, Bunch L. New 2nd ACM Int Conf on Service Oriented Computing. Yew York :
developments in ontology-based policy management: increasing ACM,2003: 242-251
the practicality and comprehensiveness of KAoS, In: IEEE [31] Ouyang Chun, Verbeek Eric, Wil M.P, et al. Formal semantics
workshop on policies for distributed systems and networks,pp
145–152, 2008. and analysis of control flow in WS-BPEL . Science of Computer
Programming,2007,67(2/3), 162-198.
[14] Tonti G, Bradshaw JM, Jeffers R, Montanari R, Suri N, Uszok A.
Semantic web languages for policy representation and easoning: [32] De Boer, Frank S., et al. "Formal modeling of resource
a comparison of KAoS, Rei, and Ponder, LNCS 2870:419–437, management for cloud architectures: An industrial case
2003. study." Service-Oriented and Cloud Computing. Springer Berlin
[15] T. D. Breaux, H. Hibshi, and A. Rao. Eddy, a formal language Heidelberg, 2012. 91-106.
for specifying and analyzing data flow specifications for [33] Fitch, Daniel F., et. al. "A Petri Net Model for Secure and Fault-
conflicting privacy requirements, Requirements Engineering,
pages 1–27, 2013. Tolerant Cloud-Based Information Storage." SEKE. 2012.
[16] May MJ. Privacy APIs: formal models for analyzing legal and Westergaard, M.: Better Algorithms for Analyzing and Enacting
privacy requirements, Ph.D. Thesis, University of Declarative Workflow Languages Using LTL, In: Rinderle, S.,
Pennsylvania,2008. Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol. 6896, 2011.