About cloudz3sec

cloudz3sec is a library and toolkit for formally analyzing security policies in cloud/API systems using Python. It is based on z3 and 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 cloudz3sec tries to help answer.

Using cloudz3sec

There are multiple ways to use cloudz3sec. The easiest way to get started is to use the BasicCloudPolicy and associated BasicCloudPolicyManager from the cloud module. This is a good approach for getting a quick sense for what cloudz3sec is about. But keep in mind that the BasicCloudPolicy type is just one example of the kind of policy you can define.

Using BasicCloudPolicy

The cloudz3sec library includes a BasicCloudPolicy type that can be used directly for analyzing policy sets. A BasicCloudPolicy consists of the following components:

• Principal - an identity in the cloud system to which the policy applies.
• Resource - an object in the cloud system governed by the policy; for BasicCloudPolicy, a resource is a URL path on a service within a tenant at some site. (The BasicCloudPolicy is modeled after RESTful microservices running in different geographical locations and includes a concept of tenancy where tenants belong to sites; i.e., institutions and/or physical datacenters where services run).
• Action - an action being performed on a resource, in this case, an HTTP verb.
• Decision - either "allow" or "deny".

Thus, policies allow or deny principals to take actions on specific resources.

We can construct policies by constructing their individual components; i.e., by creating Principal, Resource, Action and Decision objects and passing them to the BasicCloudPolicy constructor. When creating any of the components, we use a two step process: first, we construct an instance of the object, passing in data that determines all possible values for the object. Then we call the instance's set_data() method to set the specific value for the policy.

For example, suppose our cloud system is deployed at two sites, site_1 and site_2, and suppose it supports three tenants: foo, bar and baz. Suppose we have three services in our system: the apps, files and jobs services. Then the following policy grants user jsmith in the foo tenant at site_1 authorization to make GET requests to the path /apps/opensees within the apps service:

from cloudz3sec.core import *
from cloudz3sec.cloud import *

# define the list of all sites, tenants and services in our system --
sites = ['site_1', 'site_2']
tenants = ['foo', 'bar', 'baz']
services = ['apps', 'files', 'jobs']

# create the jsmith principal object --
# first, define the "universe"
jsmith = Principal(sites=sites, tenants=tenants)
# then call set_data to give the specific value
jsmith.set_data(site='site_1', tenant='foo', username='jsmith')

# similarly, define the apps Resource, the get Action, and the allow Decision --
apps = Resource(sites=sites, tenants=tenants, services=services)
apps.set_data(site='site_1', tenant='foo', service='apps', path='/apps/opensees')
get = Action()
get.set_data('GET')
allow = Decision('allow')

# finally, create the policy by putting all the components together --
policy = BasicCloudPolicy(principal=jsmith, resource=apps, action=get, decision=allow)

In addition to exact values for the components above, policies can include wild cards using the * character. For example, we could authorize jsmith for all HTTP methods instead of just GET with the following change:

# construction of Principal, Resource, and Action same as before...
all_actions = Action()
all_actions.set_data('*')

policy = BasicCloudPolicy(principal=jsmith, resource=apps, action=all_actions, decision=allow)

The above approach of defining individual components one by one is verbose and tedious. The BasicCloudPolicyManager simplifies creating and working with BasicCloudPolicy's, allowing strings to be passed in. For example, we can create the same policy above using the policy_from_strs, as follows:

from cloudz3sec.cloud import BasicCloudPolicyManager

m = BasicCloudPolicyManager(sites=['site_1', 'site_2'], tenants=['foo', 'bar', 'baz'], services=['apps', 'files', 'jobs'])

policy = m.policy_from_strs('site_1.foo.jsmith', 'site_1.foo.apps./apps/opensees', 'GET', 'allow')

In the above approach, we pass in the initial data defining the universe of all possible values for our components once to the BasicCloudPolicyManager constructor. This data includes the list of sites, tenants and services.

Then, we pass the values for the indivdual components for our policy as single strings. For example, for the principal, we pass the string "site_1.foo.jsmith". The period (.) character separates the individual parts of the principal component (the site, the tenant and the username).

Analyzing the Equivalence of Policies

The main utility of cloudz3sec is the ability to evaluate the equivalence of two policy sets. The PolicyEquivalenceChecker class from the core module provides this functionality.

Continuing with the example above, note that because the Action class from the cloud module defines the allowable HTTP verbs to be GET, POST, PUT and DELETE, we can authorize a user for all HTTP methods for a single endpoint in two equivalent ways: either through 4 policies that individually grant authorization for each HTTP method, or via a single policy that uses a wildcard (*) to grant authorization to all HTTP methods at once.

Here is how we might check that those two policy sets are equivalent using cloudz3sec:

from cloudz3sec.core import PolicyEquivalenceChecker
from cloudz3sec.cloud import BasicCloudPolicy, BasicCloudPolicyManager

m = BasicCloudPolicyManager(sites=['site_1', 'site_2'], tenants=['foo', 'bar', 'baz'], services=['apps', 'files', 'jobs'])

p_1 = m.policy_from_strs('site_1.foo.jsmith', 'site_1.foo.apps./apps/opensees', 'GET', 'allow')
p_2 = m.policy_from_strs('site_1.foo.jsmith', 'site_1.foo.apps./apps/opensees', 'POST', 'allow')
p_3 = m.policy_from_strs('site_1.foo.jsmith', 'site_1.foo.apps./apps/opensees', 'PUT', 'allow')
p_4 = m.policy_from_strs('site_1.foo.jsmith', 'site_1.foo.apps./apps/opensees', 'DELETE', 'allow')
# first policy set, p
p = [p_1, p_2, p_3, p_4]

q_1 = m.policy_from_strs('site_1.foo.jsmith', 'site_1.foo.apps./apps/opensees', '*', 'allow')
# second, equivalent policy set, q
q = [q_1]

# a policy checker
ch = PolicyEquivalenceChecker(policy_type=BasicCloudPolicy, policy_set_p=p, policy_set_q=q)

ch.p_implies_q()
# output: "proved"

ch.q_implies_p()
# output: "proved"

The calls to ch.p_implies_q() and ch.q_implies_p() are wrappers around the z3.prove() function and print "proved" if z3 can prove the statement is true, and will print a counter example if one is found.

For example, if we leave out one of the policies (policy p_4, say) from the p set, the call to ch.q_implies_p() will find a counter example:

# ...
# above definitions of p_1 through ,p_4 and q the same...

# leave out the p_4 policy:
p = [p_1, p_2, p_3]

ch = PolicyEquivalenceChecker(policy_type=BasicCloudPolicy, policy_set_p=p, policy_set_q=q)

# this is still true, as p is strictly less permissive than q
ch.p_implies_q()
# output: "proved"

ch.q_implies_p()
# output: 
  # counterexample
  # [action = "DELETE",
  #  resource = "site_1.foo.apps./apps/opensees",
  #  principal = "site_1.foo.jsmith"]

Of course, in the above simple cases it is obvious whether the policies sets are equivalent, but the power of cloudz3sec comes from the ability to analyze policy sets where equivalence is not easy to determine manually.

Creating Custom Policy Types

"But my cloud API includes the PATCH method!" you exclaim. No problem! cloudz3sec is designed to provide reusable components you can use to build your own security policy types representing the policies of your application. There are two types of building blocks provided by cloudz3sec that can be used for defining your own policy types: types where the underlying data are strings, and types where the underlying data are bit vectors.

String Types

cloudz3sec currently provides 3 different base types for working with string data in security policies: StringRe, StringEnumRe, and StringTupleRe. All three descend from the base class BaseRe and allow for policies with wildcard (*) characters by utilizing regular expression constraints over the theory of strings.

The StringEnumRe Type

The core.StringEnumRe type can be used for strings that can take a fixed, finite set of values. The cloud.Action type, representing an HTTP verb is a good example of a StringEnumRe because instances of the type can only take on one of the following values: GET, POST, PUT, DELETE or *. In general, StringEnumRe values cannot contain a wildcard with other characters; e.g., P* is not a valid Action value.

To create a new type based on StringEnumRe, simply descend from it and specify the allowable values for the new type:

class ExampleStringEnum(core.StringEnumRe):
    def __init__(self):
        # your values here...
        values = ['value_1', 'value_2', 'value_3']
        super().__init__(values)

The StringRe Type

The core.StringRe type can be used for strings that can take arbitrary values from a specified character set. A username in a cloud system is an example of something we might model with a StringRe type, if we do not consider the list of usernames in our system to be a fixed, finite list (otherwise, StringEnumRe would be a better choice). Unlike StringEnumRe, a StringRe value can contain wildcard characters with other characters.

To create a type based on StringRe, one only needs to specify the character set:

class ExampleIdentifierType(core.StringRe):
    def __init__(self):
        # your charset here ...
        super().__init__(charset=set('abcd0123456789'))

The cloud module makes use of StringRe for usernames as well as (POSIX) paths on a file system.

The StringTupleRe Type

The core.StringTupleRe type is useful for types that are really the composition of multiple StringRe and/or StringEnumRe types that should be thought of individually for the purposes of wildcard matching, but should be thought of as a single value in the overall policy.

We illustrate the concept using the example of a principal (a user identity) in a multi-tenant cloud system. In such a system, every user belongs to some tenant, and it is typical to represent an end-user identity as a username together with a tenant id. For example, for the jsmith user in the foo tenant, we might write the principal as jsmith.foo (or jsmith@foo, etc). For security policies in such a system that authorize principal(s) for one or more resources/actions, it is important to match the entire principal (user and tenant). For example, a security policy that authorizes jsmith.bar (jsmith in the bar tenant) for some resources has no bearing on the jsmith.foo user. However, with wildcard characters, we want the wildcard to apply to only one component of the principal. For example, *.foo would be all users in the foo tenant, while jsmith*.foo would be all users in the foo tenant whose username starts with jsmith.

We can create new types based on the StringTupleRe class by specifying a fields attribute to the construct. The fields attribute is a list of dictionaries, where each dictionary provides the following keys:

• name: str - the name of the field.
• type: type - the type of the field (e.g., StringRe, StringEnumRe).
• kwargs: dict - dictionary of keyword arguments to provide to the constructor of the field. For example, for StringRe fields, we should provide the charset argument and for StringEnumRe fields, we should provide the values argument.

As an example, here is how we might define our Principal type described above:

from cloudz3sec import core

class Principal(core.StringTupleRe):

    def __init__(self) -> None:
        self.tenants = ['foo', 'bar', 'baz']
        fields = [
            {'name': 'tenant', 'type': core.StringEnumRe, 'kwargs': {'values': tenants}},
            {'name': 'username', 'type': core.StringRe, 'kwargs': {'charset': ALPHANUM_SET }}
        ]
        super().__init__(fields)

Bit Vectors

Coming soon...

Implementation and Contributing New Types

This section describes the implementation of the main classes in the core module, including the BaseRe class and its children classes that support the string types, as well as the BasePolicy and PolicyEquivalenceChecker classes. The goal of this section is to explain the ways in which cloudz3sec depends on z3 and what is required to implement new (base) types in the core module.

To be completed...