Deciding Whether a Policy Set Grants More Than Intended

A policy document is a predicate over request tuples. Written in a small language with strings, wildcards, and conditions, it looks like configuration. Read as a formula, it is a decision procedure over an infinite domain, and the questions worth asking about it are questions a solver can answer: is this set of documents equivalent to that one, does any request satisfy all of them, and does any request satisfy them that the author would have rejected.

The question that matters is difference, not emptiness

Asking whether a policy set permits any request at all is almost always answered yes and is therefore useless. The useful question is a difference: which requests does this set permit that another set does not. That reframes review as a comparison between an intended set and an actual set, and it produces a witness rather than a verdict. A witness is a concrete request tuple, which a human can read and judge.

Formally, the analysis takes two predicates over the same request space and asks whether one implies the other. If actual implies intended, the policy set is at least as tight as the author’s model. If not, the solver returns a tuple in the difference, and that tuple is the finding: a specific principal, action, resource, and context that is permitted but was not intended.

This is the shape of every practical tool in the space. The hard work is not the solving; it is constructing the intended predicate, which nobody wrote down, and modelling the request space well enough that the solver’s answers correspond to what the service will actually do.

Encoding strings as a decidable theory

The difficulty in encoding policy documents is the wildcard. A resource pattern with a star denotes a set of strings, and comparing two such sets is a language-inclusion problem. Encoded naively as a string variable with constraints, the solver is asked to reason about unbounded strings, which is a hard theory and, in the general case, one that solvers handle poorly.

The practical encodings avoid general string reasoning by exploiting the restricted form of the patterns. A pattern of literal segments separated by stars denotes a regular language, and a regular language can be compiled to an automaton. Inclusion of one regular language in another is decidable in polynomial time in the product of the automaton sizes, and the automata here are small: the number of stars in a policy resource string is a handful, and the alphabet can be reduced to the distinct characters that appear in any pattern under comparison.

The alternative encoding translates the star into a bounded number of string operations and lets the solver reason about concatenation and substring constraints. That works for patterns with one or two stars and degrades quickly, because the solver’s string theory is expensive and the bounds it needs are not present in the policy. Tools in this space generally choose the automaton route for the resource field and reserve the solver for the boolean structure and the conditions.

Conditions add their own fragment. An equality condition on a tag is an equality between two terms in an uninterpreted or enumerated domain. A numeric condition on a date or a port is a linear arithmetic constraint. A condition on a source address range is a set-membership constraint over a prefix. Each of these is a theory that a modern solver handles, and the combination is the reason SMT is the natural tool: the formula mixes booleans, arithmetic, and equalities over a small finite domain, and the solver’s combination of theories is exactly designed for that mixture.

The translation is mechanical for the parts that are mechanical. A statement with an action set, a resource set, and a condition becomes a conjunction. A document becomes a disjunction of its statements, unless the document is a deny document, in which case the polarity flips. The whole set becomes the formula described in the evaluation order, which is a small amount of boolean structure over the translated statements. That the evaluation order is a fixed function of the documents, with no ordering and no state, is what makes the translation possible at all.

Asking about escalation rather than about a single identity

A more valuable question is transitive: given the policies in an account, which principals can obtain which permissions, including permissions obtained by assuming other roles, creating policies, or attaching policies to identities they control.

That question requires modelling the effect of each action on the policy state, which turns a satisfiability problem into a reachability problem over a transition system. The state is the set of policies and attachments; the transitions are the actions that modify them; the goal is a state in which the principal holds a target permission. The encoding is still an SMT query per step, with the step count bounded, and the bound is the interesting parameter: a bound of one finds direct grants, a bound of three finds chains through role assumption and policy attachment, and each additional step multiplies the search.

The findings this produces are the ones that matter in practice, because the escalation paths in these systems are rarely a single over-broad statement. They are a sequence: a principal that can create a role, a role that can be given a policy, a policy that grants a permission, and an assumption that ties them together. Each individual step looks defensible and the composition does not.

The classic composition is the one that makes a permission boundary necessary: iam:CreateRole plus iam:AttachRolePolicy plus iam:PassRole is equivalent to full administrative access, because the three together let a principal construct an identity with any permissions and then act as it. A boundary plus a condition requiring the boundary on creation, as described in permission boundaries and service control policies, breaks the chain at the second step. The solver’s job is to find the chain; the human’s job is to decide where to cut it.

Where the model and the service diverge

The analysis answers questions about the formula. The formula is a model of the service, and the model is where the analysis fails.

The first divergence is service-specific semantics. Whether a condition key is populated for a given action, whether an action supports resource-level permissions at all, and whether an ARN form is accepted in a request are all properties of individual services, documented per service and changing over time. A model that treats every action as resource-scoped and every condition key as always populated will report findings that cannot occur and miss findings that can. The conservative choice is to over-approximate the service and accept false positives, because a false positive costs a review and a false negative costs an incident.

The second divergence is the request context. The principal’s tags, the source address, the VPC endpoint, and the session’s MFA state are all part of the tuple, and the solver must be told which values are possible. Assuming the context is unconstrained produces a difference set full of tuples that no real caller could present. Assuming it is fixed to today’s values produces a proof that expires the moment a tag changes. The useful middle is to constrain the context to the values the environment can produce, and to re-run the analysis when the tag vocabulary changes, which is the coupling described in attribute conditions and tag-based access.

The third divergence is the resource policy channel. A resource-based policy can grant access that no identity policy grants, and it can do so for principals in other accounts. A model that analyses only identity policies will miss it entirely; a model that analyses resource policies must also model the cross-account evaluation, which is two independent decisions that both must allow. The confused-deputy condition described in cross-account trust and the confused deputy is a property of that joint decision and cannot be expressed in a single-account model.

The fourth divergence is temporal. Policies change, resources are created and deleted, and roles are assumed for bounded windows. A satisfiability result is about a snapshot. The snapshot is worth analysing, and it says nothing about the state after the next deployment. Analysis belongs in the deployment path, run against the candidate policies before they are applied, rather than as a periodic audit of the current state.

What a solver cannot replace

The intended predicate is the input that no tool can supply. An analysis that compares the actual policy set to an empty intended set finds everything and ranks nothing; an analysis that compares it to a hand-written approximation of intent finds only the divergences the approximation captured. The value of the exercise is proportional to how precisely intent was stated, and stating it precisely is the work that the tool appears to promise but does not do.

What the solver does supply is exhaustiveness. A human reviewer samples; a solver enumerates the whole space defined by the model, including the combinations of conditions that no single document contains. That property is worth the modelling effort for policy sets that are large, cross-account, or generated, and it is worth very little for a set of five statements that a reviewer can hold in mind.

The honest summary is that the technique converts a question about intent into a question about a formula, and the conversion is exact only when the model is. The model is never exact, so the results are sound in the direction of the over-approximation and incomplete in the direction of the service’s real behaviour. That is still more than sampling provides, and it is the reason the analysis is worth running at the point where a policy change is about to become effective.