CloudSec: An Extensible Automated Reasoning Framework for Cloud Security Policies

Users increasingly create, manage and share digital resources, including sensitive data, via cloud platforms and APIs. Platforms encode the rules governing access to these resources, referred to as security policies, using different systems and semantics. As the number of resources and rules grows, the challenge of reasoning about them collectively increases. Formal methods tools, such as Satisfiability Modulo Theories (SMT) libraries, can be used to automate the analysis of security policies, but several challenges, including the highly specialized, technical nature of the libraries as well as their variable performance, prevent their broad adoption in cloud systems. In this paper, we present CloudSec, an extensible framework for reasoning about cloud security policies using SMT. CloudSec provides a high-level API which can be used to encode different types of cloud security policies without knowledge of SMT. Further, it is trivial for applications written with CloudSec to utilize and switch between different SMT libraries. We use CloudSec to analyze security policies in Tapis, a cloud-based API for distributed computational research used by tens of thousands of researchers, and we present a performance case study of using CloudSec with Z3 and cvc5, two popular SMT solvers.