Rhino Found 21. Z3 Found 50.

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

In 2018 Spencer Gietzen at Rhino Security Labs published the definitive reference on AWS IAM privilege escalation: 21 named methods, each a specific action or action combination that turns limited permissions into administrative ones. The research is cited by every AWS security tool. PMapper checks for it. Pacu exploits it. Prowler enumerates it. Stave has 44+ per-technique controls, one per method or close enough.

The 21 methods are correctly identified. The math says there are at least 50.

This article runs Rhino's research through a Z3 SAT solver against a synthetic principal with a permission set Rhino's research was written to characterize. The solver finds all 21 of Rhino's methods and 27 additional methods Rhino didn't enumerate. The additional methods are the same structural shapes — "can the principal modify its own permissions?", "can the principal launch compute with a privileged role?" — applied to AWS services that exist today but weren't on Rhino's enumeration in 2018.

The killer follow-up: write a Deny policy that blocks every action on Rhino's list. Re-run the solver. 24 methods still reachable.

The collapse

Rhino enumerated 21 methods. They group into 5 structural patterns:

#	Pattern	Rhino methods
1	Policy Self-Mutation	1, 2, 7-13 (9 methods)
2	Credential Creation / Theft	4, 5, 6, 14
3	Compute + PassRole	3, 15-21 (8 methods)
4	Indirect Compute Invocation	16
5	Role Trust Modification	14

Each pattern is one structural shape: "principal can modify own permissions," "principal can hijack another principal's credentials," "principal can launch compute with a role," "principal can trigger compute indirectly," "principal can change a role's trust." The 21 methods are 21 instances of these five shapes.

A checklist scanner writes a separate predicate for each instance: 21 checks. A Z3 prover writes a separate query for each shape: 5 queries. The collapse ratio is 21 → 5.

Z3 prover

For each pattern, the prover holds a registry of known methods that fit the shape. Pattern 3's registry, for example:

ec2:RunInstances + iam:PassRole                                    [Rhino  3]
lambda:CreateFunction + lambda:InvokeFunction + iam:PassRole       [Rhino 15]
lambda:CreateFunction + lambda:CreateEventSourceMapping            [Rhino 16]
lambda:UpdateFunctionCode                                          [Rhino 17]
glue:CreateDevEndpoint + iam:PassRole                              [Rhino 18]
glue:UpdateDevEndpoint                                             [Rhino 19]
cloudformation:CreateStack + iam:PassRole                          [Rhino 20]
datapipeline:CreatePipeline + datapipeline:PutPipelineDefinition   [Rhino 21]
autoscaling:CreateLaunchConfiguration + CreateAutoScalingGroup     [NEW]
ecs:RunTask + iam:PassRole                                         [NEW]
ecs:CreateService + iam:PassRole                                   [NEW]
codebuild:CreateProject + codebuild:StartBuild + iam:PassRole      [NEW]
sagemaker:CreateNotebookInstance + iam:PassRole                    [NEW]
sagemaker:CreateTrainingJob + iam:PassRole                         [NEW]
batch:SubmitJob + iam:PassRole                                     [NEW]
states:CreateStateMachine + iam:PassRole                           [NEW]
apprunner:CreateService + iam:PassRole                             [NEW]

Eight Rhino methods. Nine additions. Same shape: any service that lets you launch compute with a specified IAM role is in the same structural class. Adding a new service to the registry is one struct entry. No new predicate, control YAML or check.

The query: "is there a method in this registry whose actions are all effectively allowed for the principal (in some Allow statement, not in any Deny)?" The solver returns the index of any reachable method. SAT iff the registry has at least one reachable entry.

The full results on a vulnerable principal

Run the prover against a principal that grants every relevant action:

====================================================================
== rhino-vulnerable (all 21 Rhino methods enabled)
====================================================================

--- Pattern 1: Policy Self-Mutation ---
  registry size: 13 methods (9 Rhino-numbered + 4 additional)
  reachable:     13 / 13 methods
  verdict:       SAT — at least one method reachable; full list:
    [Rhino 01] iam:CreatePolicyVersion → activate admin version on a policy the principal uses
    [Rhino 02] iam:SetDefaultPolicyVersion → activate dormant admin version
    [Rhino 07] iam:AttachUserPolicy → attach AdministratorAccess to self
    [Rhino 08] iam:AttachGroupPolicy → attach admin to own group
    [Rhino 09] iam:AttachRolePolicy → attach admin to assumable role
    [Rhino 10] iam:PutUserPolicy → create admin inline on self
    [Rhino 11] iam:PutGroupPolicy → create admin inline on own group
    [Rhino 12] iam:PutRolePolicy → create admin inline on own role
    [Rhino 13] iam:AddUserToGroup → join admin group
    [NEW    ] iam:CreatePolicy + iam:AttachUserPolicy → create admin policy and attach
    [NEW    ] iam:DeleteUserPolicy + iam:PutUserPolicy → drop restrictive inline, replace
    [NEW    ] iam:DetachUserPolicy + iam:AttachUserPolicy → swap boundary for admin
    [NEW    ] iam:DeleteRolePermissionsBoundary → remove permissions boundary on assumable role

--- Pattern 2: Credential Creation / Theft ---
  registry size: 7 methods (4 Rhino-numbered + 3 additional)
  reachable:     7 / 7 methods
  verdict:       SAT
    [Rhino 04] iam:CreateAccessKey
    [Rhino 05] iam:CreateLoginProfile
    [Rhino 06] iam:UpdateLoginProfile
    [Rhino 14] iam:UpdateAssumeRolePolicy
    [NEW    ] iam:CreateVirtualMFADevice + iam:EnableMFADevice
    [NEW    ] iam:DeactivateMFADevice
    [NEW    ] sts:GetFederationToken

--- Pattern 3: Compute + PassRole ---
  registry size: 17 methods (8 Rhino-numbered + 9 additional)
  reachable:     17 / 17 methods
  verdict:       SAT
    (all 17 methods listed)

--- Pattern 4: Indirect Compute Invocation ---
  registry size: 10 methods (1 Rhino-numbered + 9 additional)
  reachable:     10 / 10 methods
  verdict:       SAT
    (all 10 methods listed)

--- Pattern 5: Role Trust Modification ---
  registry size: 3 methods (1 Rhino-numbered + 2 additional)
  reachable:     3 / 3 methods
  verdict:       SAT
    (all 3 methods listed)

--- Cross-pattern summary ---
  registry total: 50 methods across 5 patterns
  reachable:      50 methods
  Rhino's 21 hit: 21 / 21
  beyond Rhino:   27 methods (cross-pattern, with overlaps)

50 reachable methods. 5 queries. Every one of Rhino's 21 confirmed.

The Script Said "Confirmed." The Attack Failed.

The collapse ratio above understates the value. "Rhino found 21, Z3 found 50" sounds like Z3's contribution is more methods. That framing misses the bigger win: Z3 also eliminates false positives the script-style checkers report.

A real-world penetration test, written up by Security Shenanigans (October 2020), illustrates the problem. The attacker had iam:PassRole and ec2:RunInstances. Pattern 3 / Rhino Method 3 looks for this exact pair. aws_escalate.py ran and reported:

Confirmed — privilege escalation possible

The attacker launched an EC2 instance with an admin role attached. The instance started. The reverse-shell user-data fired. Nothing connected back. The default security group had no egress rules — the standard "least-privilege" default that AWS ships. The escalation was confirmed but not exploitable.

The attacker eventually pivoted: enumerated security groups (ec2:DescribeSecurityGroups), found a hadoop-cluster SG with full egress, enumerated subnets (ec2:DescribeSubnets) for one in the same VPC, and re-launched. The escalation worked. But it required four constraints the script never checked.

This is shipped in the example as fixtures/real-world-pattern3/. Five assets:

arn:aws:iam:::user/rhino-attacker          (PassRole, RunInstances, ListRoles, no GetRole)
arn:aws:iam:::role/danger-role             (admin, trusts ec2.amazonaws.com)
arn:aws:ec2:::security-group/sg-f73b339e   (default, no egress)
arn:aws:ec2:::security-group/sg-42csce3f   (hadoop-cluster, all egress)
arn:aws:ec2:::subnet/subnet-a213as8c       (vpc-a1b2c3d4, matches both SGs)

Z3 encodes the full conjunction:

exploitable = passrole
            ∧ run_instances
            ∧ can_discover_role          ; ListRoles OR GetRole
            ∧ role_is_admin
            ∧ role_trusts_ec2
            ∧ exists_egress_sg           ; DescribeSGs ∧ SG.has_egress
            ∧ exists_valid_subnet        ; DescribeSubnets ∧ subnet.vpc=sg.vpc

Three queries on the same fixture:

--- Default SG only (no egress) ---
  verdict: UNSAT
  failed:  security group sg-f73b339e has no egress rules — reverse-shell
           user-data cannot connect back

--- Hadoop SG (full egress) ---
  verdict: SAT — full compound satisfied
  witness: PassRole→arn:aws:iam:::role/danger-role + RunInstances + ListRoles
           + sg=sg-42csce3f + subnet in vpc=vpc-a1b2c3d4

--- Without iam:ListRoles (no role discovery) ---
  verdict: UNSAT
  failed:  role discovery (no iam:ListRoles, no iam:GetRole)
  note:    PassRole on Resource:* is useless without knowing which
           role to pass — script checkers miss this

Three different verdicts on three different scenarios that all share the PassRole + RunInstances pair the script keys on. The script reports "Confirmed" three times. Z3 reports SAT once.

The granular permission bypass

Notice the third clause: iam:ListRoles OR iam:GetRole. The real-world fixture allows ListRoles but denies GetRole. A defender who reads "block GetRole" as the fix is wrong. ListRoles returns the role's trust policy in the response payload. The attacker doesn't need GetRole to read a trust policy; ListRoles already discloses it. Z3's disjunction encodes this correctly. A script-style checker that lists "GetRole" as the discovery permission misses the bypass entirely.

Why this matters for the headline number

Check	aws_escalate.py	Z3 compound
PassRole + RunInstances	Confirmed	necessary, not sufficient
Discoverable admin role	not checked	ListRoles OR GetRole
Role trusts ec2.amazonaws.com	not checked	trust policy clause
Security group with egress	not checked	sg.egress_rules ≠ ∅
Subnet in SG's VPC	not checked	subnet.vpc_id = sg.vpc_id
Result	"Confirmed"	SAT or UNSAT

The script checks 1 condition. Z3 checks 5. In a real environment where default SGs have no egress, the script's "Confirmed" is wrong on every account whose attacker hasn't yet enumerated SGs and subnets. Z3 is right relative to the modeled constraints and when the model is incomplete (missing AMI availability, for example) it returns UNSAT instead of false-positive SAT.

So the headline is wrong. "Rhino found 21, Z3 found 50" sounds like a counting argument. The sharper claim is two-sided:

• Recall: Z3 finds the methods Rhino enumerated and finds methods Rhino didn't, in the same query.
• Precision: Z3 reports UNSAT when the compound that matters fails — even if the action-list checker reports "Confirmed."

The Bybit/Safe{WALLET} extension to the iam-overpermission-wildcard example shows the dual case from the other side: the heuristic boolean stays silent on a prefix wildcard while Z3 finds the production write. Together the two extensions sketch what a sound + complete checker looks like at the boundary between "policy is broad" and "the resulting attack chain is reachable" — different questions, different provers, both necessary.

The deny-list refutation

The natural defensive move after reading Rhino's research is to write a Deny policy listing all 21 actions:

{
  "Effect": "Deny",
  "Action": [
    "iam:CreatePolicyVersion", "iam:SetDefaultPolicyVersion",
    "iam:AttachUserPolicy", "iam:AttachGroupPolicy", "iam:AttachRolePolicy",
    "iam:PutUserPolicy", "iam:PutGroupPolicy", "iam:PutRolePolicy",
    "iam:AddUserToGroup",
    "iam:CreateAccessKey", "iam:CreateLoginProfile",
    "iam:UpdateLoginProfile", "iam:UpdateAssumeRolePolicy",
    "ec2:RunInstances",
    "lambda:CreateFunction", "lambda:UpdateFunctionCode",
    "lambda:CreateEventSourceMapping",
    "glue:CreateDevEndpoint", "glue:UpdateDevEndpoint",
    "cloudformation:CreateStack",
    "datapipeline:CreatePipeline"
  ],
  "Resource": "*"
}

Re-run the prover:

====================================================================
== partial-deny (deny covers Rhino's 21 actions)
====================================================================

--- Pattern 1: Policy Self-Mutation ---
  reachable: 1 / 13 methods
    [NEW    ] iam:DeleteRolePermissionsBoundary

--- Pattern 2: Credential Creation / Theft ---
  reachable: 3 / 7 methods
    [NEW    ] iam:CreateVirtualMFADevice + iam:EnableMFADevice
    [NEW    ] iam:DeactivateMFADevice
    [NEW    ] sts:GetFederationToken

--- Pattern 3: Compute + PassRole ---
  reachable: 9 / 17 methods
    [NEW    ] autoscaling:CreateLaunchConfiguration + autoscaling:CreateAutoScalingGroup
    [NEW    ] ecs:RunTask
    [NEW    ] ecs:CreateService
    [NEW    ] codebuild:CreateProject + codebuild:StartBuild
    [NEW    ] sagemaker:CreateNotebookInstance
    [NEW    ] sagemaker:CreateTrainingJob
    [NEW    ] batch:SubmitJob
    [NEW    ] states:CreateStateMachine
    [NEW    ] apprunner:CreateService

--- Pattern 4: Indirect Compute Invocation ---
  reachable: 10 / 10 methods
    [Rhino 16] dynamodb:PutItem (the partial deny didn't include this)
    [NEW    ] sqs:SendMessage
    [NEW    ] sns:Publish
    [NEW    ] s3:PutObject
    [NEW    ] events:PutRule + events:PutTargets
    [NEW    ] iot:CreateTopicRule
    [NEW    ] ses:CreateReceiptRule
    [NEW    ] cognito-idp:UpdateUserPool
    [NEW    ] cloudwatch:PutMetricAlarm
    [NEW    ] kinesis:PutRecord

--- Pattern 5: Role Trust Modification ---
  reachable: 1 / 3 methods
    [NEW    ] iam:DeleteRolePolicy

--- Cross-pattern summary ---
  reachable:      24 methods
  Rhino's 21 hit: 1 / 21
  beyond Rhino:   23 methods

24 reachable methods after the defender did everything Rhino's research told them to. The deny-list approach catches 20 of 21 Rhino-numbered methods (Rhino 16's dynamodb:PutItem slipped through because the defender thought of it as a data-write action, not a compute-trigger). The 27 additional methods Z3 finds — the autoscaling chain, the ECS chain, the SQS trigger, the CloudWatch alarm — those weren't on Rhino's list, so they aren't on the defender's deny list, so they aren't blocked.

That's the proof.

Why structural beats enumeration

AWS adds roughly one new compute service per quarter. Each new compute service is a potential new entry in Pattern 3's registry. Each new event source is a potential new entry in Pattern 4. The defender's deny list grows monotonically. Their research budget does not.

A structural query asks "is there any method in this shape that the principal can execute?" The query itself doesn't change as new services launch. The registry changes — one new line per new service. The Z3 evaluation runs in milliseconds. The cost of extending coverage is one struct entry plus a recompile.

A heuristic enumeration asks "does the principal have permission to call this specific action?" The heuristic itself is correct for what it checks. The coverage is fragile. Each new method requires a new predicate, control YAML and test. The defender's catalogue grows at a rate determined by research bandwidth. AWS's API surface grows at a rate determined by AWS's product roadmap. These rates are not comparable.

This is Lambert's argument applied to defense: enumeration loses to a growing surface; verification proves coverage within a model. The model is the five patterns. New methods that fit any of those five shapes get coverage automatically. Methods that don't fit any shape — a brand new attack class — require a sixth pattern, which is also one query.

The remediated case

Least privilege closes everything:

====================================================================
== remediated (least-privilege)
====================================================================

--- Pattern 1: Policy Self-Mutation ---           UNSAT
--- Pattern 2: Credential Creation / Theft ---     UNSAT
--- Pattern 3: Compute + PassRole ---              UNSAT
--- Pattern 4: Indirect Compute Invocation ---     UNSAT
--- Pattern 5: Role Trust Modification ---         UNSAT

--- Cross-pattern summary ---
  reachable:      0 methods
  Rhino's 21 hit: 0 / 21
  beyond Rhino:   0 methods

The remediated principal has:

• No self-mutation actions (no iam:Attach*, iam:Put*, iam:Create* against IAM resources).
• No credential-modification actions on other principals.
• iam:PassRole scoped to one specific role ARN.
• No iam:UpdateAssumeRolePolicy.
• The roles it can pass to are not admin-equivalent.

All five patterns return UNSAT. There is no escalation path within the modeled space.

The least-privilege configuration of the remediation checklist looks like in mathematical form: scope the resource ARNs, drop the self-mutation actions, refuse the broad iam:PassRole grant, and the SAT solver returns UNSAT on every pattern.

What pattern-matching tools see

Run a per-technique scanner against the rhino-vulnerable principal. The output is 21 separate findings: "principal has CreatePolicyVersion," "principal has AttachUserPolicy," "principal has RunInstances + PassRole," etc. Each is correct. None of them composes the 21 findings into "and here are the 27 other paths in the same shape that aren't on your radar."

Run the per-technique scanner against partial-deny. The output is fewer findings. The deny closes most of them. The output reads as a successful remediation. But the 24 paths Z3 still finds aren't in the scanner's list, so they don't appear in the report. The defender ships the change, runs the scan, sees the green dashboard, and concludes the work is done.

The math says otherwise.

The architectural rule

Don't build deny lists of known privesc actions. Build allow lists of known-needed actions, scoped by resource ARN, and rely on the implicit deny for everything else.

// What the defender wrote (deny-list — fragile):
{
  "Effect": "Deny",
  "Action": [...21 actions Rhino enumerated...],
  "Resource": "*"
}

// What math suggests instead (allow-list — sound):
{
  "Effect": "Allow",
  "Action": ["s3:GetObject", "s3:ListBucket"],
  "Resource": ["arn:aws:s3:::data-team-bucket",
               "arn:aws:s3:::data-team-bucket/*"]
},
{
  "Effect": "Allow",
  "Action": "iam:PassRole",
  "Resource": ["arn:aws:iam::*:role/data-team-job-role"]
}

The first form is a list of known bad. It grows. It trails AWS's product roadmap. It's never complete. The second form is a list of known good. It grows only when the team's actual needs grow. Everything else is implicitly denied. Patterns 1, 2, 4, 5 don't fire because the actions aren't in the allow list. Pattern 3 doesn't fire because iam:PassRole is scoped to a non-admin role.

Z3 returns UNSAT on all five patterns. That's not "we caught the methods we knew about." It's "no method in the modeled space exists." Different proposition.

Checklist

• IAM identity policies use Allow-with-resource-ARN-scoping rather than Deny-with-action-blocklist
• iam:PassRole resource is a list of specific role ARNs, not Resource: "*" with a service condition
• No principal has self-mutation actions (iam:Attach*, iam:Put* on IAM resources, iam:DeleteRolePermissionsBoundary, iam:UpdateAssumeRolePolicy)
• No principal has credential-modification actions on other principals (iam:CreateAccessKey, iam:UpdateLoginProfile, MFA-related actions on roles other than self)
• When AWS announces a new compute service, the org's posture review treats it as a Pattern 3 candidate by default — the registry gets a new entry, the prover runs against existing principals, every match is a finding
• CI runs a pattern-based prover (this article's template) against post-deploy observation snapshots, not just per-technique heuristic checks

The meta-lesson

Rhino did the foundational research that made every subsequent IAM privesc tool possible. The ecosystem rallied around the 21 methods. Z3 confirms all 21 of them. It just demonstrates that 21 is a lower bound, not the total. The total is "every method that fits these five shapes," and that number is whatever AWS launches next.

Defenders who think in lists will always be one quarter behind AWS's release calendar. Defenders who think in shapes are bounded by their model and the model is small enough to keep current. Five patterns. New service launches? Add it to the right registry. Re-run the prover. Done.

Rhino found 21. Z3 found 50. 24 of those still work after blocking everything Rhino listed. That's six sentences and the case for thinking structurally.

---

The example shipped is at stave/examples/iam-21-privesc-5-patterns/ — a CEL evaluation via pkg/stave.Apply (scoped to one of Stave's 44+ per-technique IAM escalation controls; fires on the vulnerable and partial-deny fixtures, silent on remediated) and a Z3 SAT prover that runs the five pattern queries across all three fixtures and prints the cross-pattern summary quoted in this article. 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, with no cloud credentials.