A CROSS TENANT ACCESS CONTROL (CTAC) MODEL FOR CLOUD COMPUTING: FORMAL SPECIFICATION AND VERIFICATION

 

ABSTRACT

Sharing of resources on the cloud can be achievedon a large scale since it is cost effective and location independent.Despite the hype surrounding cloud computing, organizations arestill reluctant to deploy their businesses in the cloud computingenvironment due to concerns in secure resource sharing. In thispaper, we propose a cloud resource mediation service offered bycloud service providers, which plays the role of trusted thirdparty a its different tenants. This paper formally specifiesthe resource sharing mechanism between two different tenants inthe presence of our proposed cloud resource mediation service.The correctness of permission activation and delegation mechanisma different tenants using four distinct algorithms(Activation, Delegation,Forward Revocation and Backward Revocation)is also demonstrated using formal verification. Theperformance analysis suggest that sharing of resources can beperformed securely and efficiently across different tenants of thecloud.

EXISTING SYSTEM:

Role based access control (RBAC) enables fine-grainedaccess control (and generally in a single domain). Differentextensions of RBAC have been proposed in the literature tosupport multi-domain access control. These approaches relyon a single body responsible for maintaining cross-domainpolicies. However, in a cloud environment, each user (individualor organization) may have one or more tenants and havea separate management infrastructure. Therefore, it is likelythat users are not able to agree on a single organization tomanage access control on their behalf.With the increased trendof cloud services due to its various benefits (e.g. on-demandself-service model and resources sharing a tenants), itis essential for CSPs to provide mechanisms to segregate thedata of the tenants.An advanced Hierarchical Open Stack Access Controlmodel was proposed in , which is designed to facilitatesecure and effective management of information sharing in acommunity cloud for both routine and cyber incident responseneeds. A cross-tenant trust model and its RBAC extension wasproposed in for enabling secure cross-tenant communication.A multi-tenant authorization as a Service (MTAaaS)platform to enforce such cross-tenant trust model is also presentedin the paper. In a separate work, an autonomous multitenantnetwork security framework “Jobber” was proposed[18]. However, the security of the approaches in these threestudies was not demonstrated.

PROPOSED SYSTEM:

Y We present a CTAC model for collaboration, and theCRMS to facilitate resource sharing ast varioustenants and their users.Y We also present four different algorithms in the CTACmodel, namely: activation, delegation, forward revocationand backward revocation.Y We then provide a detailed presentation of modeling,analysis and automated verification of the CTAC modelusing the Bounded Model Checking technique with SMTLIBand Z3 solver, in order to demonstrate the correctnessand security of the CTAC model.CONCLUSIONIn this paper, we proposed a cross-tenant cloud resourcemediation service (CRMS), which can act as a trusted-thirdparty for fine-grained access control in a cross-tenant environment.For example, users who belong to an intra-tenant cloudcan allow other cross-tenant users to activate a permission intheir tenant via the CRMS. We also presented a formal modelCTAC with four algorithms designed to handle the requests forpermission activation. We then modeled the algorithms usingHLPN, formally analyzed these algorithms in Z language,and verified them using Z3 Theorem Proving Solver. Theresults obtained after executing the solver demonstrated thatthe asserted algorithm specific access control properties weresatisfied and allows secure execution of permission activationon the cloud via the CRMS.Future work will include a comparative analysis of theproposed CTAC model with other state-of-the-art cross domainaccess control protocols using real-world evaluations. For example,one could implement the protocols in a closed or smallscale environment, such as a department within a university.This would allow the researchers to evaluate the performance,and potentially (in)security, of the various approaches underdifferent real-world settings.

REFERENCES

[1] Akhunzada, A., Gani, A., Anuar, N. B., Abdelaziz, A., Khan, M. K.,Hayat, A., & Khan, S. U. (2016). Secure and dependable software definednetworks. Journal of Network and Computer Applications, 61, 199-221.

[2] Alam, Q., Tabbasum, S., Malik, S., Alam, M., Tanveer, T., Akhunzada,A., Khan, S., Vasilakos, A. and Buyya, R., (2016). Formal Verification ofthe xDAuth Protocol. IEEE Transactions on Information Forensics andSecurity, 11(9), pp. 1956-1969.

[3] Ali, M., Malik, S. and Khan, S., DaSCE: Data Security for CloudEnvironment with Semi-Trusted Third Party.

[4] Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi, D., King,T., Reynolds, A. and Tinelli, C., 2011, July. Cvc4. In InternationalConference on Computer Aided Verification (pp. 171-177). SpringerBerlin Heidelberg.

[5] Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodrguez-Carbonell, E. andRubio, A., 2008, July. The barcelogic SMT solver. In InternationalConference on Computer Aided Verification (pp. 294-298). SpringerBerlin Heidelberg.

[6] Bruttomesso, R., Cimatti, A., Franzn, A., Griggio, A. and Sebastiani, R.,2008, July. The mathsat 4 smt solver. In International Conference onComputer Aided Verification (pp. 299-303). Springer Berlin Heidelberg.

[7] Choo, K.K., 2006. Refuting security proofs for tripartite key exchangewith model checker in planning problem setting. In 19th IEEE ComputerSecurity Foundations Workshop (CSFW’06) (pp. 12-pp). IEEE.

[8] Choo, K.-K. R., Domingo-Ferrer, J. and Zhang, L., 2016. Cloud Cryptography:Theory, Practice and Future Research Directions. Future GenerationComputer Systems, 62, pp. 51-53.

[9] De Moura, L. and Bjørner, N., 2011. Satisfiability modulo theories:introduction and applications. Communications of the ACM, 54(9), pp.69-77.

[10] Dutertre, B. and De Moura, L., 2006. The yices smt solver. Tool paperat http://yices. csl. sri. com/tool-paper. pdf, 2(2).