CloudSec: An Extensible Automated Reasoning Framework for Cloud Security Policies

TL;DR

CloudSec is an extensible framework that simplifies reasoning about cloud security policies using SMT solvers, enabling easier analysis and switching between different solvers without requiring specialized knowledge.

Contribution

It introduces a high-level API for encoding cloud security policies and supports multiple SMT libraries, facilitating broader adoption and flexibility in policy analysis.

Findings

Successfully analyzed policies in Tapis cloud platform

Enabled switching between SMT solvers like Z3 and CVC5

Demonstrated practical applicability in real-world cloud systems

Abstract

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 \textit{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 that 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 such as Z3 and CVC5. We demonstrate the use of CloudSec to analyze security policies in Tapis, a cloud-based API for distributed computational research used by tens of thousands of researchers.