Cloud computing providers employ sophisticated authorization engines to decide when a request to access a resource should be allowed or denied. Several approaches have formalized the behavior of individual authorization policies, but authorization engines employ multiple types of policies that can interact in different ways. This paper presents a modular formalization of the Amazon Web Services (AWS) authorization engine and a corresponding analysis tool, called IAM-MultiPolicyAnalyzer, for verifying properties pertaining to multiple policies of different types. IAM-MultiPolicyAnalyzer adopts Zelkova [18]—i.e., the formalization of individual IAM policies—as a basic building block, and uses a new domain-specific language for modularly describing how the authorization engine composes individual uses of Zelkova. As a result, IAM-MultiPolicyAnalyzer provides a trusted, reusable, human-readable, and performant SMT-backed model of AWS’s authorization logic that is now used within multiple AWS applications. We have run conformance testing of our model against the engine implementation and its documentation; the corner cases identified by our testing have led to improvements and modifications to the official AWS documentation.
Research areas
