Peng Zhao,Lifa Wu,Zheng Hong,He Sun

1 Command & Control Engineering College,Army Engineering University of PLA,Nanjing 210007,China

2 School of Computer Science,Nanjing University of Posts and Telecommunications,Nanjing 210023,China

3 PANDA Electronics Group Co.,Ltd.,Nanjing 210014,China

Abstract: Multicloud access control is important for resource sharing and security interoperability across different clouds,and heterogeneity of access control policy is an important challenge for cloud mashups.XACML is widely used in distributed environment as a declaratively fine-grained,attribute-based access control policy language,but the policy integration of XACML lacks formal description and theory foundation.Multicloud Access Control Policy Integration Framework(MACPIF) is proposed in the paper,which consists of Attribute-based Policy Evaluation Model (ABPEM),Four-value Logic with Completeness (FLC) and Four-value Logic based Policy Integration Operators (FLPIOs).ABPEM evaluates access control policy and extends XACML decision to four-value.According to policy decision set and policy integration characteristics,we construct FLC and define FLPIOs including Intersection,Union,Difference,Implication and Equivalence.We prove that MACPIF can achieve policy monotonicity,functional completeness,canonical suitability and canonical completeness.Analysis results show that this framework can meet the requirements of policy integration in Multicloud.

Keywords: Multicloud; access control; policy integration; four-value logic

I.INTRODUCTION

With the rapid development of cloud computing,issues regarding resource sharing,Quality of Service (QoS) and Vendor Lockin [1,2]have prompted the emergence of new concepts and models in Cloud Computing,such as Inter-Cloud,Cloud Federation,Hybrid Cloud and Multicloud.As a promising cloudbased service paradigm,Multicloud [3,4]has become a kind of Inter-Cloud model with high recognition and wide popularity.In Multicloud the participants don’t need to make any change to the original technology solution and operation mode.Multicloud can reduce Vendor Lock-in,improve resiliency during outages and geo-presence,boost performance and lower costs [5].However,Multicloud still faces many security challenges[6],such as security perimeter extension,new trust system,secure & efficient interoperability,information flow control,data security & privacy protection.Consequently,it is of vital importance to research on Multicloud access control technology.

Multicloud access control technology is a security mechanism that ensures resource sharing and secure interoperability in Multicloud.It manages the access permission to prevent intrusion of illegal users and legitimate user’s misuse.The major objectives of Multicloud access control technology are: (1)to achieve resource sharing and interoperability among multiple clouds; (2) to prevent illegal users from accessing protected resource in Multicloud; (3) to prevent legitimate users from accessing unauthorized resource in Multicloud.There are not any policy conflicts in a single cloud environment,because access control policy is homogeneous and managed uniformly.However,the heterogeneity of Multicloud influences resource sharing and secure interoperability prominently.Therefore,it is very important to solve the problem of Multicloud access control policy integration.

Access control policy integration based on the policy formalization can ensure security interoperability among multiple clouds,avoid policy conf l icts and guarantee CSPs’ freedom of entry and exit.However,there are policy conflicts in the integration of Multicloud access control policies.When multiple CSPs collaborate,heterogeneous security policies can be the source of policy conf l icts that result in security breaches.So,policy integration for Multicloud access control must address challenges such as semantic heterogeneity,secure interoperability,and policy evolution management.Policy integration aims to synthesize access control policy,solve potential conf l icts and ensure secure interoperation cross clouds.Possible policy anomalies must be detected and resolved,including policy inconsistencies and inefficiencies.Policy inconsistencies can result in Contradiction,Exception,and Correlation.Inefficiencies in composite policies include redundancy and verbosity.This paper focuses on the problem of policy integration,policy conf l ict detection and resolution will be studied later.

This paper focused on the formalization and integration of access control policy in Multicloud,and defined the method of the rules,policies,and policy sets evaluation.

In this paper,Multicloud Access Control Policy Integration Framework (MACPIF) is proposed to solve the above problems.The main contributions of this work are as follows:First,Attribute-based Policy Evaluation Model(ABPEM) was constructed for the formalization and evaluation of access control policy.Second,Four-value Logic with Completeness(FLC) was proposed for the logical expression of policy integration and applied to the access decision generation in Four-value Logic based Policy Integration Operators (FLPIOs),includingIntersection,Union,Difference,ImplicationandEquivalence.Third,we prove that FLC can achieve policy monotonicity,functional completeness,canonical suitability and canonical completeness.

The original contribution of this work is to construct FLC which can intuitively reflect the operators and results of policy integration,including “Conflict”.MACPIF is designed according to FLC and has strict syntax and semantic,such as policy monotonicity,functional completeness and canonical completeness.The framework can be well adapted to Multicloud access control policy integration,and describe security interoperability and policy conf l icts among multiple clouds.

The rest of his paper is structured as follows.Related work on Multicloud access control policy integration is analyzed in section 2.Section 3 introduces ABPEM,FLC,and FLPIO,such asIntersection,Union,Difference,ImplicationandEquivalence.The characteristics of MACPIF,such as policy monotonicity,functional completeness,canonical suitability and canonical completeness,are proven in Section 4.MACPIF is compared with related work in section 5.Section 6 summarizes the paper and gives future prospects.

II.RELATED WORK

2.1 Cloud computing and XACML

Cloud service providers and Open Source community have designed the system architecture and technical scheme of access control to ensure the security of cloud services.Amazon Web Services[7]supports access policy mechanisms,including IAM,Resource-based ACLs,User-based ACLs,LDAP,pre-Signed URLs.Access policy mechanisms are broadly categorized into resource-based policies and user policies.Microsoft Azure[8]manages Microsoft accounts using Azure Active Directory,LDAP,SASs,and ACLs.Google Cloud[9,10]have two major options available for accessing objects and containers,and the options Access Control Lists(ACLs) and Signed URLs.OpenStack[11]has an independent component (Keystone) for authentication and authorization,which provides access control mechanisms,such as Temporary URLs,RBAC,and LDAP.Both CloudStack and Eucalyptus do not have independent component for access control,but implement access control by setting entry rules and outf l ow rules for VMs.Resource domain (zone) manages user,security group,virtual machine and network access in CloudStack.Cloud controller (CLC)is in charge of identity authentication and user management in Eucalyptus.Access control technology in Cloud Computing is shown in Table I

XACML is a policy description language proposed by OASIS[12],but it isn’t applied widely on Cloud platforms,except for Jboss,Axiomaics and OpenAZ.Public Cloud Service Providers prefer self-designed policy description languages,such as Amazon Web Services,Microsoft Azure,and Google Cloud,but XACML is studied to solve the specification,expansibility and flexibility of access control in the academic world.Ravi Sandhu etal[13]verified the feasibility of MTAS model using RBAC policy specification of XACML 2.0.Aliaksandr et al [14,15]presented an advanced authorization framework based on the Usage Control (UCON) model and the OASIS XACML standard to regulate the usage of cloud resources.The framework addresses the issue of long lasting accesses and it is able to interrupt accesses that are in progress when the corresponding access rights do not hold any more.Dinh et al [16]extended XACML 2.0 model to achieve security and flexibility for access control in Cloud.Daniel et al [17]proposed a framework for risk-based access control,and it is based on an extension of XACML and uses risk policies,which adds flexibility for resource sharing in a dynamic and collaborative environment.Yin et al [18]proposed a Multicloud access control model based on XACML,named MCACM,to implement Cross-Cloud access control.

Table I.Access control technology in cloud computing.

2.2 Multicloud policy integration

Multicloud access control policy integration needs to solve policy heterogeneity and security interoperability,and the relevant methods and processes are complicated.Current research on Multicloud access control policy integration mainly includes trust-based method [19-21],ABE-based method [22,23],and semantic-based method [24,25].

Trust-based access control policy integration achieves security interoperability according to the trust or reputation level between multiple clouds and consumers.Banyal et al.[26]proposed an efficient and flexible access control framework to address the security and privacy issues for Multicloud.This framework used static and dynamic trust evidence to generate trust value and reduce the probability of unauthorized operation,and it ensured that authorized users could access cloud resources.Fan et al.[27]addressed the problem of trust management in Multicloud environments based on a set of TSPs (Trust Service Providers).The TSPs were distributed over multiple clouds,and elicited raw trust evidence from different sources and in differ-integration inconsistency and inaccurate evaluation results,Ni et al.[31]proposed D logic to integrate access decisions using unary operators ?,binary operators ⊕ and ?,and to achieve functional completeness and computational validity.Rao et al.[32]proposed a Fine-grained policy Integration Algebra (FIA)using three-valued logic {Y N NA,,} to defineAND,OR,andNOToperators,and proved that FIA was functionally complete.Liu et al.[33]constructed binary operator to integrate XACML,but the formalization of XACML is not intuitive and the evaluation result is inconsistent.Li et al.[34,35]proposed a Policy Combining Language (PCL),which modeled XACML policy integration algorithms[36],combined evaluation results and extended decision set to {Permit,Deny,NA,IN}.Bruns et ent formats.Based on the adherence of CSP to Service Level Agreement (SLA) for a Cloudbased service and the feedback sent by CSUs,independent third-party evaluated an objective trust and a subjective trust of CSPs.Pustchi et al.[20,21]presented a fine-grained Cross-Cloud domain trust model which enables resource sharing among domains across distinct homogeneous Clouds,and a formalized description of core MC-OSAC (Multicloud OpenStack Access Control) with proposed domain trust extension by extending OpenStack identity and federation services to support Cross-Cloud domain trust.However,trustbased access control policy integration can easily lead to trust deception.It is necessary to combine other methods to ensure data security.

ABE-based access control policy integration achieves Cross-Cloud interoperability according to Multicloud access structures,attribute set and their secret key.Komninos et al.[28]proposed an encryption scheme to preserve privacy by employing data access policy over sets of attributes in the collaborative environment for multiple clouds,but the authorization center is highly vulnerable.Li et al.[22]constructed an attribute-based access control system for proxy-based Multicloud environment [2]to achieve distributed access control without any trusted center,manager,or additional secret keys,and proposed a MACPABE scheme to achieve resource security and resource sharing in Multicloud.However,collusion attack arises in the model.

Semantic-based access control policy integration achieves semantic description and logic reasoning of heterogeneous access control policy,but the semantic conf l ict cannot be avoided.Bonatti et al.[29]proposed a set of policy integration algebra,which formalized access control policy into triplet,including subjects,objects and actions,and policy integration operators such asAddition,Conjunction,andSubtraction.Lin et al.[30]extended the policy integration algebra to Attribute-based access control Policy Composition Algebra (APoCA).In order to solve policy non-formalization,al.[37]proposed a policy integration algebra PBel according to Belnap,the decision set is{Grant,Deny,Unspecified,Conflict} .P B e l[38]had the ability of integration operation according to Belnap Bilattice,but didn’t consider monotonicity and completeness.PTaCL[39]is a formal authorization policy language that provides accurate policy decision and precise policy evaluation,but the policy conf l icts and completeness are not considered.Crampton et al.[40-42]constructed a policy description language based on Four-valued Logic for policy integration.In addition,6-ary logic [43]and 8-ary logic [31]were studied to describe the decision set of access control from different points of view,but the characteristics of the logics were not analyzed.

This paper constructs MACPIF with strict syntax and semantics to solve the problems regarding Multicloud access control policy integration,realizes the formalization of Multicloud access control policy,and ensures the correctness of policy integration.

III.MACPIF

MACPIF consists of ABPEM,FLC and FLPIO.ABPEM implements the evaluation of attribute,rule,and policy by formalizing cloud entity and matching request with policy,expands the decision set from three values to four values and renders it suitable for Multicloud policy integration.FLC defines the decision set 4t={0,⊥,?,1} and describes policy integration usingIntersection,Union,Difference,ImplicationandEquivalenceoperators.FLPIO evaluates these operators on the basis of ABPEM and FLC.The execution process of MACPIF is shown in figure 1.

3.1 ABPEM

XACML’s policy consists of target,rules,rule-combining algorithm,obligation and advice.The target defines the set of requests to which the policy is intended to apply in the form of a logical expression on attributes in the request.Main components of rule includes target,effect,condition,obligation and advice.Condition represents a Boolean expression that refines the applicability of the rule beyond the predicates implied by its target.The effect of the rule can be “Permit”,“ Deny”,“ Intermediate”,or “ NotApplicable”.The restrictions specified by the target and condition elements support the notion of attribute-based access control under which access control policies are expressed as conditions against the properties of subjects and protected objects.Rule evaluation needs to evaluate the target and condition of the rule,whose process is complex and lacks theoretical support.ABPEM is proposed in the section,which improve XACML’s rule evaluation approach using the attribute expressions [42]to get the rule evaluation results,including “Permit”,“Deny”,or “NotApplicable”,and achieve policy evaluation.

Fig.1. The execution process of MACPIF.

Definition 1.Attributeais composed of data type and value range,and abstractly described as tripletwherenis attribute name,vis the range of value,and ～ is the relation between name and value.All entity attributes in ABAC were referred to asa.

Attributeais the smallest unit of constraint and rule in ABAC.The attribute value range includes series type and discrete type.The series type is the relation of numerical comparison,which indicatesT h e discrete type is an independent value or partial ordering relation,which indicateswhere operator ? is the relation of partial ordering,such as “prior to” or “inheritance”,and operator ?is the opposite of ?.

Definition 2.Requestqconsists ofnname-value pair and is described aswherenvpiindicates theith name-value pairin a two-tuple form.The name-value pair of all entity attributes in the request are uniformly described as

Definition 3.Attribute operation is represented as tripletwhereis the symbol of attribute operation which is used to restrict value range and is described asnv∝.The attribute operation of all entities can be expressed as

Definition 4.For name-value pairnvpand attributea,the result that attributeaevaluatesnvpis represented as ?a?(nvp) and formalized a sThe evaluation result are as follows:

The results of attribute evaluation include“Permit”,“Deny”,and “NotApplicable” in ABPEM,and are expressed as {1,0,⊥}.When Policy Decision Point (PDP) matches request with the attribute,it can be regarded as matching the attribute set with the name-value pair of the request.

Definition 5.?R?(q) indicates the result which the ruleRevaluates requestq,whereis the rule set,is the request,⊕ is the binary operator.The attribute evaluationis composed ofThe rule evaluation is composed ofwhereThe formalization is as follows:

In brief,the formalization that the ruleRevaluates the requestqis as follows:

D={0,?,⊥,1} is the result set of attribute evaluation,and ⊕ is a binary operator between the evaluation results.The attributeaiandajevaluate requestqrespectively.Ifandthe evaluation results conflict,and indicates ?R?(q)=?.

Policy Administration Point (PAP) produces and maintains access control policies,and PDP evaluates these policies.The policy evaluation is de fined as follow:

Definition 6.The formalization of the policy evaluation iswhereP={RS,⊕} is the formalization of access control policy,RS={R1,…,Rk} is the rule set,and⊕ is rule-combining algorithms.

The mapping function fromkrule to decisionDis described as ?P?(q)=which can be simplified aswhereDi∈{0,⊥,?,1} is the decision set of policy evaluation.

3.2 FLC

Belnap [44]is a well-known Bilattice Logic whose truth values are “0”,“1”,“⊥” and “?”,representing “False”,“True”,“NotApplicable”and “Conflict” respectively.Belnap can indicate the inconsistency and incompleteness of policy integration and is the foundation of formalized authorization languages,such as PBel[38],Rumpole [45]and BelLog [46].The bilattice is a space of generalized truth values with bilattice orderings.One ordering,≤t,records the degree of truth,“1” is the maximal element,and “0” is the minimal element,“⊥”and “?” are incomparable intermediate elements.The other ordering,≤k,records the degree of information or knowledge.“?” is the maximal element,“⊥” is the minimal element,“0” and “1” are incomparable intermediate elements.Bilattice Logic is shown in figure 2.

Definition 7.Four-value Logic is defined asFOUR({0,⊥,?,1},≤t,≤k),and the truth value indicates a two-tuple{(t,f),f≤t}.Let 1=(t,f),0=(f,t),?=(t,t),⊥=(f,f),and (a,b)≤t(c,d)?a≤c∧d≤b,(a,b)≤k(c,d)?a≤c∧b≤d.

The results of policy integration aren’t described clearly and explicitly using “True”,“False”,“Con flict” and “NotApplicable”,but is expressed in two-tuple intuitively.Table II is the truth value table for propositionA.

Fig.2.Bilattice logic.

So the essential difference between Four-valued Logic and classical two-value logic is whether “there is information which supportsA” is equivalent to “there is no information which opposesA”.This definition can intuitively represent the two states of information and the four states of policy integration.

The partial order relationship among“0”,“1”,“⊥” and “?” is represented as 0≤t⊥,?≤t1,where “0” is “False”,“⊥” is“NotApplicable”,“?” is “Conflict”,“1” is“True”.Four-valued Logic can intuitively describe the evaluation results of access controland the integration results between the evaluation results.

Table II.The truth value table for proposition A.

Fig.3.Fouler-value Logic operators.

Fig.4.The extended Four-value Logic operators.

FLC is constructed according to Four-valued Logic.

Definition 8.Four-valued Logic with CompletenessFLC(4t,{ ?,?,∧}) is a Four-valued Logic based on “True” and “False” partial order.We define two unary operators ? and? whose truth tables are shown in figure 3(a),the operator ? swaps the values of “0” and “1”,and the operator ? permutes the values “0”,“⊥”,“?” and “1”.In addition,we define the operator ∧ which acts asIntersectionoperator,whose truth table is shown in figure 3(b).

Definition 9.The extended operators of FLC includeImplication,EquivalenceandConjunction.?x,y∈{0,⊥,?,1}.The operator → indicatesImplication,and is expressed asx→y=?x∨y.The operator ?indicatesequivalence,and is expressed asx?y=(x→y)∧(y→x).The operator∨ indicatesconjunction,and is expressed asx∨y=?(?x∧ ?y).The truth table is shown in figure 4.

The operators of FLC apply to the integration of access control rule,policy and policy sets,which lay a theoretical foundation for the policy integration.

3.3 FLPIO

In the access control policy integration field,the work of Bonatti et al.[29]and Lin et al.[30]are most representative and typical.An algebra for composing access control policies was proposed by Bonatti et al.[29],whose main entities are Subject,Object and Action,and the operators such asUnion,IntersectionandDifferenceare used to resolve policy integration.FLPIO is proposed in this paper.FLPIO formalizes and evaluates the integration operators such asUnion,Intersection,Difference,ImplicationandEquivalenceoperators.

ForIntersection,Union,Difference,Implication,andEquivalenceoperators,these operators betweenP1andP2indicateP1∧P2,P1∨P2,P1-P2,P1→P2andP1?P2,whose policy evaluation to requestqindicates ?P1∧P2?(q),?P1∨P2?(q),?P1-P2?(q),?P1→P2?(q) and?P1?P2?(q).

The operator ∧ generates new access control policyP1∧P2.IfP1allows access authorization andP2also allows access authorization,P1∧P2also allows access authorization.

Definition 10.There existP1,P2andq,?P1?(q) and ?P2?(q) indicate the evaluation policyP1andP2to requestqrespectively,?P1∧P2?(q)=?P1?(q)∧ ?P2?(q) indicate the evaluation of operator ∧ integration policy to requestq.If the policy evaluation ?P1?(q) is“True”,and the policy evaluation ?P2?(q) is also “True”,?P1?(q)∧?P2?(q) is “True”.

The operator ∨ generates new access control policyP1∨P2.If eitherP1orP2allows access authorization,P1∨P2allows access authorization.

Definition 11.There existP1,P2andq,?P1?(q) and ?P2?(q) indicate the evaluation of policyP1andP2toqrespectively,?P1∨P2?(q)=?P1?(q)∨ ?P2?(q) indicate the evaluation of operator ∨ integration policy to requestq.If either the policy evaluation?P1?(q) or ?P2?(q) is “True”,?P1?(q)∨?P2?(q)is “True”.

The operator - generates new access control policyP1-P2.IfP1allows access authorization andP2denies access authorization,P1-P2allows access authorization.

Definition 12.There existP1,P2andq,?P1?(q) and ?P2?(q) indicate the evaluation of policyP1andP2to requestqrespectively,?P1-P2?(q)=?P1?(q)∧ ??P2?(q) indicates the evaluation of operator - integration policy to requestq.If the policy evaluation ?P1?(q) is“True”,and ?P2?(q) is “False”,?P1-P2?(q) is“True”.

The operator → generates new access control policyP1→P2.IfP1denies access authorization,orP2allows access authorization,P1→P2allows access authorization.

Definition 13.There existP1,P2andq,?P1?(q) and ?P2?(q) indicate the evaluation of policyP1andP2to requestqrespectively,?P1→P2?(q)=??P1?(q)∨ ?P2?(q) indicate the evaluation of operator → integration policy to requestq.If the policy evaluation ?P1?(q) is“False”,or ?P2?(q) is “True”,?P1→P2?(q) is“True”.

The operator ? generates new access control policyP1?P2.IfP1→P2allows access authorization andP2→P1also allows access authorization,P1?P2allows access authorization.

De finition 14.There existP1,P2andq,?P1?(q)and ?P2?(q) indicate the evaluation of policyP1andP2to requestqrespectively,?P1?P2?(q)=(?P1?(q)→?P2?(q))→(?P2?(q)→?P1?(q))indicate the evaluation of operator ? integration policy to requestq.If the policy evaluation ?P1?(q)→?P2?(q) is “True”,and?P2?(q)→?P1?(q) is “True”,?P1?P2?(q) is also “True”.

IV.THE CHARACTERISTICS OF MACPIF

This section mainly analyzes the characteristics of MACPIF,such as policy monotonicity,functional completeness,canonical suitability,and canonical completeness.

4.1 Policy Monotonicity

The purpose of policy monotonicity is to prevent malicious users from changing decision and affecting the access results through withholding attributes.Li et al.[47]analyzed three cases of matching entity attributes with request attributes,and the conditions of matching success have been given.Crampton et al.[39]proposed policy monotonicity and analyzed the impact of the decision the malicious users can modify.This part analyzes policy monotonicity of MACPIF.

For policyP,P1andP2,there may existqandq′ such thatq′?q,?P1?(q′)=?P1?(q)=0 and ?P2?(q′)=0,?P2?(q)=1.If we have a policyP=(P1,P2),such that ?P1?(q)=0 and?P2?(q)=1,then ?P?(q)=0.However,if?P1?(q′)=0,?P2?(q′)=0,then ?P?(q)=⊥.In other words,it might be possible for a malicious user to change “0” decision to “⊥” decision by suppressing certain attributes.Consequently,the less information a request contains,the more uncertain the policy evaluation is.

Definition 15.For policyPand requestq,q′,ifq′?q,?P?(q′)≤?P?(q),policyPhas policy monotonicity.

There may exist requestsqandq′ such thatq′?qand for any attribute namensuch that(n,v)∈q′ and (n,v′)∈q,then (n,v′)∈q′.It is easy to see that any atomic operator is monotonic,and it follows that any policy built using the operatorsand,orandnotis monotonic.

Theorem 1.LetPbe a policy which consists of sub-policyP1,…,Pkand operators∧,∨,-,→,?.For requestsq′,q,if there existsq′?q,such that ?P?(q′)≤?P?(q),thenPachieves policy monotonicity.

PROOF: We prove policy monotonicity using mathematical induction;

Step 1: For policyPiand requestsq′,q,ifq′=q,then ?Pi?(q)=?Pi?(q′).Ifq′?q,thenvpnumber ofq′ is less than thenvpnumber ofq,the probability ofq′ matching policyPisuccessfully is less than the probability ofq,then ?Pi?(q)＜?Pi?(q′).Therefore,the policyPiis monotonic;

Step 2: For policiesPi,Pjand requestsq′,q,ifPi= ?Pj,then ?Pi?(q)=??Pi?(q)a n d ?Pi?(q′)=???Pj??(q′).B e c a u s eTherefore,the policy ?Piis monotonic;

Step 3: For policiesP,Pi,Pjand requestsq′,q,whereP=Pi∩Pj,if there areaccording to Step 1,then ?P?(q)??P?(q′),the policyPwhich is integrated using operator∧ is monotonic;

Step 4: According to Definition 9,the operators of the extended Four-value Logic,∨,-,→ and ?,can be represented using ?and ∧ operators.Consequently,the policyPwhich is integrated using operator ∨,-,→ and? is monotonic;

In summary,the policyPis monotonic,which consists of sub-policyP1,…,Pkand operators ∧,∨,-,→ and ?.

Theorem 1 shows that if the subset of the requestqsatis fies the policyP,requestqalso satisfies the policyP.Therefore,an attacker cannot get access permissions through hiding attributes.

4.2 Functional completeness

Functional completeness is the ability to represent the result of evaluation in the process of policy integration.For example,Three-valued Logic cannot express the contradictions of policy integration,functional completeness of which is de fined in [48].Now,functional completeness of MACPIF is proven in this part.

L=(D,Ops) is logic,whereDis the truth value set,Opsis the operator set,Φ(L) is the function set.A functionF:Dn→Dis completely speci fied by a truth table containingncolumns andmnrows.Functional completeness is de fined as follows:

Definition 16.For every functionF:Dn→D,if there is a formulaφ=Φ(L) of aritynwhose evaluation corresponds to the truth table,thenLis functionally complete.

FunctionF:Dn→Dis completely specified by a truth table containingncolumns andmnrows.However,not every truth table can be represented by a given logicL=(D,Ops).Lis said to be functionally complete if for every functionF:Dn→D,there is a formulaφ=Φ(L) of aritynwhose evaluation corre-sponds to the truth table.

Theorem 2.FLC(4t,{?,?,∧}) is functionally complete

PROOF:FLC(4t,{?,?,∧}) is proposed in this paper,where 4t={0,⊥,?,1} is the decision set,{?,?,∧} is the basic operator set,{∨,-,→,?} is the extended operator set.Figure 5 is the truth table of functionFand the table shows logicFLC(4t,{?,?,∧}) is functionally complete.

According to Definition 16 and Theorem 2,XACML [12]is not functionally complete,but PTaCL [39]and PBel [38]are functionally complete.

4.3 Canonical completeness

Canonical completeness indicates the ability of access control policy to describe selection operation.When canonical completeness of MACPIF is analyzed,canonical suitability and selection operator are introduced to clearly describe the canonical completeness of MACPIF.

HypothesisL=(D,Ops) is logic,whereDis the truth value set,Opsis the operator set,Φ(L) is the function set.

De finition 17.If and only if there exist formulaφmaxandφminof arity 2 in Φ (L) such thatφmax(x,y) returnssup{x,y} andφmin(x,y)returnsinf{x,y},Lis canonically suitable.If logicLis canonically suitable,we will writeφmax(x,y) andφmin(x,y) using infix binary operators asx?yandx?y,respectively.

FLC(4t,{?,?,∧}) is canonically suitable b e c a u s eφmin(x,y)=x∧y,φmax(x,y)=?(?x∧?y),4t={0,⊥,?,1},and the truth table of FLC operators.Select operator is introduced to prove canonical completeness of logic FLC.Figure 6 shows the normal forms of the unary single selection operators.

Theorem 3.IfFLC(4t,{?,?,∧}) is canonically suitable and every unary selection operator can be expressed in normal form,thenFLC(4t,{?,?,∧}) is canonically complete.

PROOF: According to Definition 17,FLC is canonically suitable; According to Definition 18 and figure 7,all unary selection operator of FLC can be expressed in normal form; Moreover,Functionfis expressed as thedisjunction(?) andconjunction(?) of unary selection operators.In conclusion,FLCsatisfies canonical completeness.

V.COMPARISON AND ANALYSIS

Fig.5. The truth table of FLC operators.

Fig.6. The normal forms for the unary selection operators.

In this paper MACPIF has been proposed and it has strict syntax and semantic,such as policy monotonicity,functional completeness and canonical completeness.The characteristics have been proven in section IV.The theoretical analysis can intuitively reflect the advantage of MACPIF.This section analyses the characteristics,the operators set and the decision set of MACPIF,and compares MACPIF with related work,such as XACML [12],PTaCL[39],PTaCL(E) [41],PBel [38].

Table III compares MACPIF with related works about the characteristics of policy integration.The results show that the security of policy integration is not considered in XACML [36].Policy Integration of PTaCL[39]does not achieve normal forms.There is a risk that the malicious user tampers with the results of policy integration in PTaCL(E)[28].Functional completeness is only considered in PBel[25].MACPIF satisfies policy monotonicity,functional completeness,canonical suitability and canonical completeness simultaneously.In Section 4,we have proven the operators of MACPIF satisfy FLC and have a strict theoretical basis.Therefore,MACPIF can provide theoretical support for achieving Multicloud interoperability and preventing unauthorized access.

Table IV compares MACPIF with related work.The results show that the decision setsof XACML [12],PTaCL [39],and PTaCL(E)[41]exist in three states:Permit,Deny,NotApplicable,and cannot indicate policy conflicts.The operator set of PBel [25]cannot describe canonical completeness.The decision set of MACPIF can intuitively reflect the results of policy integration.The operator set of MACPIF can describe policy monotonicity,functional completeness,canonical suitability,and canonical completeness.MACPIF can describe complex policy integration through composing decision results and achieve the requirements of resource sharing and secure interoperability in Multicloud environment.

Table III.The characteristics comparison of policy integration.

Table IV.The comparison of operators and decision set.

VI.CONCLUSION AND FUTURE WORK

This paper focused on the formalization and integration of access control policy in Multicloud,and defined the method of the rules,policies,and policy sets evaluation.According to the constructed Four-valued Logic,the integration operators were defined,includingIntersection,Union,Difference,ImplicationandEquivalence.Compared with related work,the results show that the framework was policy monotonic,canonical suitable,functionally complete and canonically complete.In the future,we will further study the policy mining and logic reasoning in Multicloud environment,which provide theoretical principle for resource sharing and security interoperability.

ACKNOWLEDGEMENTS

This work was supported by National Key R&D Program of China (2017YFB0802900)and NUPTSF (No.NY219004).