%0 Conference Proceedings %T A Formal Approach for the Verification of AWS IAM Access Control Policies %+ National University of Computer and Emerging Sciences [Islamabad] (NUCES) %+ Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) %+ Web Scale Trustworthy Collaborative Service Systems (COAST) %A Zahoor, Ehtesham %A Asma, Zubaria %A Perrin, Olivier %Z Part 3: Security %< avec comité de lecture %( Lecture Notes in Computer Science %B 6th European Conference on Service-Oriented and Cloud Computing (ESOCC) %C Oslo, Norway %Y Flavio De Paoli %Y Stefan Schulte %Y Einar Broch Johnsen %I Springer International Publishing %3 Service-Oriented and Cloud Computing %V LNCS-10465 %P 59-74 %8 2017-09-27 %D 2017 %R 10.1007/978-3-319-67262-5_5 %K AWS cloud %K IAM %K Access control %K Verification %K Event-Calculus %Z Computer Science [cs]Conference papers %X Cloud computing offers elastic, scalable and on-demand network access to a shared pool of computing resources, such as storage, computation and others. Resources can be rapidly and elastically provisioned and the users pay for what they use. One of the major challenges in Cloud computing adoption is security and in this paper we address one important security aspect, the Cloud authorization. We have provided a formal Attribute Based Access Control (ABAC) model, that is based on Event-Calculus and is able to model and verify Amazon Web Services (AWS) Identity and Access Management (IAM) policies. The proposed approach is expressive and extensible. We have provided generic Event-Calculus modes and provided tool support to automatically convert JSON based IAM policies in Event-Calculus. We have also presented performance evaluation results on actual IAM policies to justify the scalability and practicality of the approach. %G English %Z TC 2 %Z WG 2.14 %2 https://inria.hal.science/hal-01677620/document %2 https://inria.hal.science/hal-01677620/file/449571_1_En_5_Chapter.pdf %L hal-01677620 %U https://inria.hal.science/hal-01677620 %~ CNRS %~ INRIA %~ INRIA_TEST %~ INRIA-LORRAINE %~ LORIA2 %~ INRIA-NANCY-GRAND-EST %~ TESTALAIN1 %~ IFIP-LNCS %~ IFIP %~ UNIV-LORRAINE %~ INRIA2 %~ IFIP-TC %~ IFIP-WG %~ IFIP-ESOCC %~ IFIP-TC2 %~ LORIA %~ LORIA-NSS %~ INRIA2017 %~ IFIP-WG2-14 %~ IFIP-LNCS-10465