On the modelling and analysis of Amazon Web Services access policies

Abstract

Cloud computing is a conceptual paradigm that is receiving a great deal of interest from a variety of major commercial organisations. By building systems which run within cloud computing infrastructures, problems related to scalability and availability can be reduced, and, from the point of view of consumers of such infrastructures, abstracted away from. As such infrastructures tend to be shared, it is important that access to the sub-components of each system is controlled. One of the first languages for controlling access to services within a cloud is the Amazon Web Services access policy language. In this paper we present two formal models of this language|one in Z and one in Alloy|and show how the Alloy model might be used to test properties of multiple policies and to generate and test candidate policies.