Your Deny Policy Blocks Six Privesc Paths. There Are Nine.

✓ Human-authored analysis; AI used for formatting and proofreading.

In July 2022 Edoardo Rosa published a writeup documenting a privilege escalation in AWS where a principal carrying the AWS-managed DataScientist policy plus AmazonElasticMapReduceFullAccess could escalate to admin even with an explicit deny policy in place. The deny DemoDenyPrivEscs in the writeup listed six actions:

{
  "Effect": "Deny",
  "Action": [
    "cloudformation:CreateStack",
    "cloudformation:UpdateStack",
    "ec2:RunInstances",
    "lambda:Create*",
    "lambda:Update*",
    "lambda:InvokeFunction"
  ],
  "Resource": "*"
}

Each one is a known compute-launch path that, combined with iam:PassRole, lets a principal launch compute running as a different role. The deny list reads like the result of a security review where someone enumerated "ways to launch EC2 with a role" and copied them into a policy.

The writeup shows that this list is incomplete. The author found one bypass: autoscaling:CreateLaunchConfiguration + autoscaling:CreateAutoScalingGroup by manual inspection of the AWS service catalog. The path works: the launch configuration specifies an admin role as the instance profile, the autoscaling group launches an EC2 with that role, the principal reads IMDS credentials and gains admin.

This article runs the same configuration through a Z3 SAT solver with a registry of nine known compute-launch vectors. The solver finds five bypasses. After remediation when the deny list is expanded to cover all nine the solver proves the architectural residual: every new compute service AWS adds becomes a new bypass path.

The deny-list approach to privilege escalation prevention is structurally fragile. The math says so.

A compute-launch vector is any (set of actions) combination that, with iam:PassRole, results in compute running as a specified role. The known vectors:

Nine vectors. Each one is a different code path inside AWS, but each one ends at the same place: an EC2-like compute environment running with the IAM role you named.

The writeup's deny list covers four: ec2:RunInstances, lambda:CreateFunction (via lambda:Create*), lambda:UpdateFunctionConfiguration (via lambda:Update*), and cloudformation:CreateStack. Plus cloudformation:UpdateStack (which doesn't itself launch compute but is included for completeness) and lambda:InvokeFunction (also not a compute-launch). The five it misses are autoscaling, ECS, CodeBuild, Glue, and SageMaker.

The author found one of those five. The other four were sitting there untouched.

The Z3 prover walks the principal's three policies DataScientist, EMRFullAccess, DemoDenyPrivEscs and computes the effective permission set: actions that appear in at least one Allow statement and no Deny statement. For each of the nine compute-launch vectors, the prover checks whether all required actions are effectively permitted and iam:PassRole is allowed for the vector's PassedToService.

vector_available(vector) :=
  ALL action in vector.RequiredActions:
    action in any Allow statement
    AND action not in any Deny statement
  AND iam:PassRole is allowed AND not denied
  AND vector.PassedToService in some PassRole condition

The Z3 query for Finding 1: is there any vector for which vector_available(vector) is true?

--- Finding 1: deny coverage gap ---
  query:    among 9 known compute-launch vectors, is any one
            effectively permitted (Allow ∧ ¬Deny)?
  vectors available: 1 / 9
  verdict:  SAT — witness: autoscaling — Auto Scaling launch config + group with instance profile
            actions: [autoscaling:CreateLaunchConfiguration autoscaling:CreateAutoScalingGroup]
            (deny does not cover these actions; the path is open)

vectors available: 1 / 9 The prover counts the autoscaling vector as the one reachable path. The other available vectors are filtered by the PassedToService condition: ECS needs ecs-tasks.amazonaws.com in the condition list, which isn't there; CodeBuild needs codebuild.amazonaws.com, also missing; same for Glue and SageMaker. The autoscaling vector matches because EMRFullAccess's PassRole condition includes ec2.amazonaws.com.

But the deny coverage table separate from the SAT proof shows which actions the deny does and doesn't cover:

--- Deny coverage analysis ---
  ec2             BLOCKED    : Direct EC2 launch with instance profile
  lambda          BLOCKED    : Create Lambda with execution role
  lambda          BLOCKED    : Update existing Lambda to use different execution role
  cloudformation  BLOCKED    : Create CloudFormation stack with execution role
  autoscaling     NOT BLOCKED : Auto Scaling launch config + group with instance profile
  ecs             NOT BLOCKED : Run ECS task with task role
  codebuild       NOT BLOCKED : Create and start CodeBuild project with service role
  glue            NOT BLOCKED : Create Glue job with execution role
  sagemaker       NOT BLOCKED : Create SageMaker notebook with execution role

Five vectors not blocked. The autoscaling one is currently exploitable because the principal's PassRole condition includes EC2. The other four are not currently exploitable because the PassRole condition list doesn't include their respective services. But that's a fragile gate. If the principal later acquires ec2.amazonaws.com broader PassRole (say, through a different attached policy that broadens the service list), or if AWS introduces a new service whose role-passing convention reuses ec2.amazonaws.com, four more vectors become immediately reachable. The deny doesn't block them because the deny doesn't know about them.

--- Finding 2: PassRole reaches an admin-equivalent role ---
  query:    is there an admin role whose trust matches the principal's
            PassRole `iam:PassedToService` condition?
  reachable admin roles: 1 / 1
  verdict:  SAT — witness: arn:aws:iam::111122223333:role/demo-EC2Admin
            (trusts [ec2.amazonaws.com]; has AdministratorAccess; PassRole condition
             admits any role trusting one of those services)

The EMR policy's PassRole grant:

{
  "Effect": "Allow",
  "Action": "iam:PassRole",
  "Resource": "*",
  "Condition": {
    "StringEquals": {
      "iam:PassedToService": [
        "elasticmapreduce.amazonaws.com",
        "ec2.amazonaws.com"
      ]
    }
  }
}

Resource: "*" and a service-only condition. This is the second architectural fragility: the grant scopes which services the role can be passed to, but not which roles can be passed. Any role in the account trusting elasticmapreduce.amazonaws.com or ec2.amazonaws.com is a passable target. The fixture's demo-EC2Admin trusts ec2.amazonaws.com and has AdministratorAccess.

--- Finding 3: complete privesc chain ---
  query:    is there an available compute-launch vector + an admin
            role + a trust relationship that all line up?
  compound paths: 1
  verdict:  SAT — witness: vector=autoscaling role=arn:aws:iam::111122223333:role/demo-EC2Admin
            chain: [autoscaling:CreateLaunchConfiguration autoscaling:CreateAutoScalingGroup] → role with AdministratorAccess assumed by EC2 →
            principal reads IMDS credentials → admin

The conjunction lands. A vector is reachable, an admin role is PassRole-reachable, and the role's trust service matches the vector's PassedToService. Three API calls CreateLaunchConfiguration, CreateAutoScalingGroup, then SSH into the launched instance and the principal has admin.

The natural fix: expand the deny list to cover every known compute-launch action.

 {
   "Effect": "Deny",
   "Action": [
     "cloudformation:CreateStack",
     "cloudformation:UpdateStack",
     "ec2:RunInstances",
     "lambda:Create*",
     "lambda:Update*",
-    "lambda:InvokeFunction"
+    "lambda:InvokeFunction",
+    "autoscaling:CreateLaunchConfiguration",
+    "autoscaling:CreateAutoScalingGroup",
+    "autoscaling:UpdateAutoScalingGroup",
+    "ecs:RunTask",
+    "ecs:CreateService",
+    "codebuild:CreateProject",
+    "codebuild:StartBuild",
+    "glue:CreateJob",
+    "sagemaker:CreateNotebookInstance",
+    "sagemaker:CreateTrainingJob"
   ],
   "Resource": "*"
 }

Re-run the prover:

========== remediated-config (deny expanded to all 9 known vectors) ==========
--- Finding 1: deny coverage gap ---
  vectors available: 0 / 9
  verdict:  UNSAT — every known compute-launch vector is denied
            (the expanded deny list covers all 9 known vectors today;
             see Finding 2 for the residual structural risk)

--- Finding 2: PassRole reaches an admin-equivalent role ---
  verdict:  SAT — witness: arn:aws:iam::111122223333:role/demo-EC2Admin
            **RESIDUAL** — the remediated config closes today's launch
            vectors but does not scope PassRole by role ARN. Any new
            compute service AWS adds becomes an immediate exploit
            path until the deny list is expanded.

--- Finding 3: complete privesc chain ---
  compound paths: 0
  verdict:  UNSAT — no compound privesc path open
            (Finding 1 closed all launch vectors; without one of those,
             the PassRole reachability in Finding 2 has nowhere to land)

Two of three queries flipped to UNSAT. Finding 2 remains SAT.

The remediation works. Finding 3 is UNSAT, no exploit path is currently open. But Finding 2's persistent SAT is the formal proof that the architecture is structurally fragile. The principal can still pass an admin role to "any service in the condition list." The principal cannot currently use that role because all known compute-launch services are denied. The day AWS introduces a new compute service that the deny list doesn't know about and AWS introduces roughly a new service per quarter. Finding 3 flips back to SAT.

Two ways to scope iam:PassRole:

// What the writeup uses (and what the remediation
// keeps unchanged):
{
  "Effect": "Allow",
  "Action": "iam:PassRole",
  "Resource": "*",
  "Condition": {
    "StringEquals": {
      "iam:PassedToService": [
        "elasticmapreduce.amazonaws.com",
        "ec2.amazonaws.com"
      ]
    }
  }
}
// What's structurally sound:
{
  "Effect": "Allow",
  "Action": "iam:PassRole",
  "Resource": [
    "arn:aws:iam::111122223333:role/EMRClusterRole",
    "arn:aws:iam::111122223333:role/EMRDataNodeRole"
  ]
}

The first form scopes by which services and delegates the question of "which roles trust those services" to the IAM trust-policy graph, which the operator does not control globally. The second form scopes by which roles which is explicit and finite.

The deny list approach is a chase: every time AWS adds a service that supports an instance profile or task role, the deny list grows. The PassRole-by-role approach is a fixed enumeration: the only roles that can ever be passed are the named ones, regardless of what AWS launches next month. Z3's residual SAT on Finding 2 is the formal way of saying "the deny list is the wrong shape; the PassRole grant is the right shape."

A heuristic IAM scanner like PMapper detects this specific bypass. Edoardo Rosa's writeup acknowledges PMapper. But a heuristic scanner reports "this principal can launch autoscaling with an admin role". A true positive, the kind of finding a SOC reviewer would action. The reviewer fixes autoscaling and moves on.

The Z3 prover reports the same finding and the deny coverage table and the residual. The reviewer sees:

That last point is the difference between "close the autoscaling hole" and "close the deny-list-architecture issue." The first a heuristic recommends. The second formal verification recommends.

iam:PassRole with Resource: "*". The resource is always a specific role ARN list stave apply against post-deploy observation snapshots; the existing CTL.IAM.ESCALATE.PASSROLE.AUTOSCALING.001 and similar per-technique controls fire on regressions The researcher found one bypass through expert knowledge. Z3 found five. After remediation, the solver is still finding something. A structural feature of the architecture that guarantees more exploits will appear. That's the difference between checking the configuration's current state and checking the configuration's durability. Pattern matchers do the first. Z3 does both.

The example at iam-autoscaling-privesc-bypass has two binaries side by side: a CEL evaluation via pkg/stave.Apply (uses the existing CTL.IAM.ESCALATE.PASSROLE.AUTOSCALING.001 per-technique control) and a Z3 SAT prover that walks the principal's effective permission set against a 9-vector compute-launch registry, prints the deny coverage table, and surfaces the residual PassRole-scoping finding that survives remediation. The Z3 binary lives in a sibling Go module so its libz3 link stays out of Stave's main vendored tree. Stave detects this pattern and 31 other H1-grounded scenarios from local AWS configuration snapshots, without cloud credentials.