About cloudsec

cloudsec is a library and toolkit for formally analyzing security policies in cloud/API systems using Python. It has a modular and extensible architecture allowing it to support multiple backends; initially, z3 and cvc5 will be supported. The cloudsec project takes influence from a number of related projects, such as the Z3 Firewall Checker.

Background

Cloud/API systems are commonly secured through the use of security policies -- rules governing the set of actions that agents (users, services, etc) are authorized to take within the system. For example, AWS uses IAM Policies; Kubernetes provides pod security policies, network policies, RBAC, etc.

Within this context, a common question arises: given two sets of security policies, P and Q, are the rules generated by P and Q equivalent, or is one set strictly more permissive than the other? A particular common case is to let P be some existing policy set and let Q be a policy set that includes a security vulnerability. In this case, determining that P is equivalent to Q (or even just that P=>Q) establishes that the existing policy set contains a vulnerability. These are the types of questions cloudsec tries to help answer.

Quick Start

To get a quick sense of what CloudSec is about, let's assume we have a web API with an authorization model that grants users access to different endpoints in the API. For simplicity, an "endpoint" will be a URL path (e.g., /apps, /jobs, etc) and an HTTP verb (e.g., GET, POST, DELETE, etc.). We can use CloudSec to define a new policy type for our web API with just a few lines of code:

from cloudsec.core import StringComponent, StringEnumComponent, Policy, PolicyType, OneWildcardMatching

username = StringComponent(name="username", 
                           char_set=ALPHANUM_SET, 
                           max_len=25,             
                           matching_type=OneWildcardMatching())
path = StringComponent(name="path", 
                       char_set=PATH_CHAR_SET, 
                       max_len=250, 
                       matching_type=OneWildcardMatching())
verb = StringEnumComponent(name="verb", 
                             values=["GET", "POST", "PUT", "DELETE"], 
                             matching_type=OneWildcardMatching())
WebAPIPolicyType = PolicyType(components=[username, path, verb])

In the code above, we create a new security policy type (WebAPIPolicyType) defined by three parts: the username, presenting the identity to be authorized, and the path and verb, together representing an endpoint in our Web API. Note that this small amount of code is all that is needed to define a new policy type -- it would be similarly easy to define a policy type for other kinds of systems.

But once we have a policy type defined, we can create and analyze policies. Creating policies amounts to providing values for each of the components (username, path and verb, in the case above) as well as a specical decision field which all policy types inherit. The decision field takes one of two values: allow or deny, indicating whether the policy authorizes or does not authorize the action.

Here we create two policies:

p = Policy(policy_type=WebAPIPolicyType, 
           username="jstubbs", 
           path="/apps",
           verb="GET",
           decision="allow")

q = Policy(policy_type=WebAPIPolicyType, 
           username="jstubbs", 
           path="/apps",
           verb="*",
           decision="allow")

In the first policy, p, we authorize the user "jstubbs" for the GET /apps endpoint. In the second, q, we authorize the same user for all verbs on the /apps path. The * is a wildcard which indicates any value. We can use wildcard characters when defining any of the values in our policies.

We can now analyze these two policies using a cloudSec PolicyEquivalenceChecker.

checker = PolicyEquivalenceChecker(policy_type=WebAPIPolicyType, 
                                   policy_set_p=[p],
                                   policy_set_q=[q])

The checker object has methods that allow us to analyze the equivalence of the two policy sets, [p] and [q]:

result = checker.p_implies_q()
result.proved
  --> True

result = checker.q_implies_p()
result.proved
  --> False
result.found_counter_ex
  --> True
result.model
  --> [verb = "PUT", path = "/apps", username = "jstubbs"]

First we check if p => q, and cloudSec finds the result is proved. That's because every action authorized by our p policy is indeed authorized by q. Next, we check if q => p. Here, cloudSec shows the result is not proved and in fact it found a counter example. Indeed, p is strictly less permissive than q, and the result.model provides an example of an action that is authorized by q but not p. Note that in the case above cloudSec is leveraging the z3 theorem prover, but we could have used cvc5 instead -- all we would need to do is specify backend="c5c5" when constructing the PolicyEquivalenceChecker instance.

Installation

Building the Images and Trying the Examples

Docker images can be built to try out the cloudsec software. The Makefile can be used to generate the images:

# generate the images --
$ make build

With the images generated, start a container with the cloudsec software and examples using docker:. Have a look at the examples_z3.py file, contained within the examples directory, for all the definitions of the objects used below.

$ docker run -it --rm --entrypoint=bash --name=sec  jstubbs/cloudsec-exs

Start a Python shell and import the examples:

# from within the container started above,

>>> from examples_z3 import *

>>> result = checker.p_implies_q()

# p => q is True, meaning that the p policy set is less permissive than the q policy set
# i.e., any activity allowed by p is also allowed by q.
>>>  result.proved
True

>>> result = checker.q_implies_p()

# q => p is False, however, because q is NOT less permissive than p; that is, q allows some activities
# that p does not allow.
>>> result.proved
False

# In fact, cloudsec was able to find a counter example to the statement q => p; i.e., it was able to find
# an activity allowed by q but not by p.
>>> result.found_counter_ex
True

# the result.model contains a counter example to the q => p statement; i.e., it contains an example of
# an activity that is allowed by the q policy set but not by the q policy set. 
>>> result.model
[action = "PUT",
 resource_path = "s2/home/jstubbs",
 resource_service = "files",
 resource_tenant = "a2cps",
 principal_username = "jstubbs",
 principal_tenant = "a2cps"]

Development

cloudsec includes a test suite based on pytest. The Makefile can be used to build the tests container image and run the tests:

# Build the tests image 
$ make build-tests

# Run the tests
$ make test