Your Lambda Has Admin on S3 and Doesn't Know It

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

The Lambda function reads one file from one bucket. The policy attached to its execution role looks like this:

{
  "Statement": [
    {
      "Effect": "Allow",
      "Action": "s3:*",
      "Resource": "*"
    },
    {
      "Effect": "Allow",
      "Action": [
        "logs:CreateLogGroup",
        "logs:CreateLogStream",
        "logs:PutLogEvents"
      ],
      "Resource": "arn:aws:logs:us-east-1:111122223333:*"
    }
  ]
}

The CloudWatch Logs statement is correctly scoped with three specific actions on the account's log-group ARN namespace. The developer who wrote this policy knows how to scope a permission set. They wrote the second statement deliberately.

The first statement is "this works, ship it" reflex. s3:* on * is the policy that requires the least time to write and the least time to debug; the function doesn't fail on permission errors during local testing; nobody asks "what S3 actions does this code call?" before merge.

The Capital One breach was this configuration plus an SSRF on a publicly-reachable web application. The SSRF reached the EC2 metadata endpoint, retrieved temporary credentials for the role attached to the running compute, and used those credentials' s3:* grant to read 100 million records from buckets the application never intended to touch.

What s3:* Grants

The S3 service has more than 100 actions. Most teams only think about a handful:

• s3:GetObject — read.
• s3:PutObject — write.
• s3:ListBucket — list.
• s3:DeleteObject — delete.

s3:* admits all of those, plus all of these:

A function that calls s3:GetObject once gets every one of these on every bucket the account owns. The Lambda's control plane is now an attack surface for the entire account's S3 footprint.

The System Invariant

Sensitive IAM actions (s3:*, kms:Decrypt,
dynamodb:*, secretsmanager:GetSecretValue,
sts:AssumeRole, etc.) must scope their Resource
element to specific ARNs.

In Stave's observation schema, the engine pre-computes a boolean by walking each role's attached policy statements:

{
  "id": "arn:aws:iam::111122223333:role/DataProcessorLambdaRole",
  "type": "aws_iam_role",
  "properties": {
    "identity": {
      "kind": "role",
      "trusted_services": ["lambda.amazonaws.com"],
      "policies": {
        "has_resource_wildcard_on_sensitive": true,
        "attached_policies": [
          {
            "name": "DataProcessorBroadPolicy",
            "statements": [
              {"Effect": "Allow", "Action": "s3:*", "Resource": "*"},
              {"Effect": "Allow", "Action": ["logs:..."], "Resource": "arn:aws:logs:..."}
            ]
          }
        ]
      }
    }
  }
}

has_resource_wildcard_on_sensitive is the engine's verdict; attached_policies[].statements carries the evidence. CEL reads the boolean to fire the control. Z3 reads the statements to enumerate the specific dangerous calls the wildcard admits.

The Stave Control

id: CTL.IAM.POLICY.RESOURCE.WILDCARD.001
name: Sensitive Actions Must Not Use Resource Wildcard
severity: high
unsafe_predicate:
  all:
    - field: properties.identity.policies.has_resource_wildcard_on_sensitive
      op: eq
      value: true

One leaf clause. The engine has already done the work of deciding whether any of the role's statements pair a sensitive action with Resource: "*". CEL's job is to report it.

Why CEL is Not Enough

The customer reading the finding sees:

Your role has a wildcard sensitive action.

…and asks the follow-up:

Which actions? And on which buckets?

CEL evaluates a state predicate. It does not enumerate the admitted action × resource set. The risk of s3:* on * is not "your policy is broad". It is "your role can do these specific dangerous things on these specific sensitive resources."

The Z3 Witness Model

The companion program at stave/examples/iam-overpermission-wildcard/z3prove/ walks the role's policy statements and encodes:

0 = (s3:GetObject,        app-data-production/input/file.csv)    intended
1 = (s3:PutObject,        app-data-production/output/result.json) intended
2 = (s3:PutBucketPolicy,  customer-pii-bucket)                   DANGEROUS
3 = (s3:DeleteObject,     billing-archives/jan-2026.csv)         DANGEROUS
4 = (s3:PutBucketAcl,     audit-logs-bucket)                     DANGEROUS

The Go side computes which witnesses each Allow statement admits s3:* matches every s3:Foo action; Resource: "*" matches every ARN and feeds the admitted-set boolean to Z3. The solver then discharges:

unsafe = admitted ∧ dangerous ∧ ¬intended

Output for the broad policy:

=== before (s3:* on *) ===
  policy statements: 2
    [0] Effect=Allow Action=s3:* Resource=*
    [1] Effect=Allow Action=[logs:CreateLogGroup logs:CreateLogStream logs:PutLogEvents] Resource=arn:aws:logs:us-east-1:111122223333:*
  admitted requests: 5 / 5
  intended scope:    [s3:GetObject → app-data-production/input/file.csv
                      s3:PutObject → app-data-production/output/result.json]
  dangerous set:     [s3:PutBucketPolicy → customer-pii-bucket
                      s3:DeleteObject → billing-archives/jan-2026.csv
                      s3:PutBucketAcl → audit-logs-bucket]
  verdict: SAT — witness: s3:PutBucketPolicy on customer-pii-bucket

Five of five witnesses admitted. The solver picks the first dangerous-and-not-intended one as a proof: an attacker with this role's credentials can make customer-pii-bucket public with a single s3:PutBucketPolicy call. The customer does not need to read the policy carefully or imagine the attack chain. The witness is the attack chain.

After the policy is scoped:

=== after  (scoped actions + ARNs) ===
  policy statements: 3
    [0] Effect=Allow Action=s3:GetObject Resource=arn:aws:s3:::app-data-production/input/*
    [1] Effect=Allow Action=s3:PutObject Resource=arn:aws:s3:::app-data-production/output/*
    [2] Effect=Allow Action=[logs:...] Resource=arn:aws:logs:...
  admitted requests: 2 / 5
  ...
  verdict: UNSAT — no dangerous action admitted outside intended scope

UNSAT. Two admitted requests, both intended. No dangerous-and-unintended request remains.

The CI Gate

The same policy that grants s3:* on * also contains a correctly-scoped CloudWatch Logs statement:

{
  "Effect": "Allow",
  "Action": [
    "logs:CreateLogGroup",
    "logs:CreateLogStream",
    "logs:PutLogEvents"
  ],
  "Resource": "arn:aws:logs:us-east-1:111122223333:*"
}

Three specific actions, one regional ARN namespace. The developer knew how to scope a permission. They chose not to scope S3, because:

1. The function's S3 usage was being iterated on during development; broad permissions kept the test loop fast.
2. Scoping S3 requires knowing the exact bucket prefix the function reads, which depends on whether you're in dev, staging, or prod. The developer was about to template that out, but the deadline arrived first.
3. The same broad policy worked the last time the team shipped a Lambda. Nobody filed a follow-up to scope it.

Pen testers and SOC analysts often blame the developer who wrote this kind of policy. The CloudWatch Logs statement proves they had the skill. What they didn't have was a CI gate that said "you're shipping s3:*, this fails the build."

The Remediation

 {
   "Statement": [
     {
       "Effect": "Allow",
-      "Action": "s3:*",
-      "Resource": "*"
+      "Action": "s3:GetObject",
+      "Resource": "arn:aws:s3:::app-data-production/input/*"
+    },
+    {
+      "Effect": "Allow",
+      "Action": "s3:PutObject",
+      "Resource": "arn:aws:s3:::app-data-production/output/*"
     },
     {
       "Effect": "Allow",
       "Action": ["logs:CreateLogGroup", "logs:CreateLogStream", "logs:PutLogEvents"],
       "Resource": "arn:aws:logs:us-east-1:111122223333:*"
     }
   ]
 }

Three lines turn into seven. The function's behaviour doesn't change; the role's reach does. The CEL predicate goes from has_resource_wildcard_on_sensitive: true to false; Z3 goes from SAT-with-witness to UNSAT.

The Prevention Lesson

The fix is three layers, in order of leverage:

Service Control Policy denying wildcard sensitive actions for compute roles. At the organisation level:

{
  "Sid": "DenyWildcardSensitiveActions",
  "Effect": "Deny",
  "Action": [
    "s3:*",
    "kms:*",
    "dynamodb:*",
    "secretsmanager:*"
  ],
  "Resource": "*",
  "Condition": {
    "ArnNotLike": {
      "aws:PrincipalArn": [
        "arn:aws:iam::*:role/SecurityBootstrap*",
        "arn:aws:iam::*:role/CloudOps*"
      ]
    }
  }
}

The SCP refuses to apply any policy of this shape to non-bootstrap roles. The denial is global and silent. The developer's broad-policy attempt fails at policy-attach time, never reaches deploy.

Module-level enforcement in IaC. The Terraform / CDK / Pulumi module that creates a Lambda execution role takes an s3_resources: list(string) parameter. The module composes the statement itself; passing ["*"] is rejected at plan time.

CI gate on stave apply. The example shipped with this article is the template. A PR that introduces a role with has_resource_wildcard_on_sensitive: true produces exit 3 from CTL.IAM.POLICY.RESOURCE.WILDCARD.001. Same predicate, same exit code as the example; the build fails before the PR is mergeable.

The CI gate catches policies created outside IaC. A console click during incident response, an emergency hotfix, a third-party service that creates a role on first install. The other two layers prevent the unsafe shape. The CI gate makes sure the prevention is working.

Checklist

• Service Control Policy denies wildcard sensitive actions on Resource: "*" for non-bootstrap roles
• IaC modules for compute-service execution roles take a typed list of allowed resources, not a free-form policy document
• stave apply runs in CI against the post-deploy observation snapshot; PRs with has_resource_wildcard_on_sensitive: true fail
• Production roles do not pair s3:*, kms:*, dynamodb:*, or secretsmanager:* with Resource: "*"
• Code review for new Lambda functions reads the role's policy, not just the function's code, because what the role can do matters more than what the function currently does

The policy in the before fixture is honest. It says: "I am too broad." The CEL predicate reads the boolean and agrees; the Z3 witness names the specific dangerous call. The SCP at the org level makes that combination impossible to ship in the first place. The lesson is "infrastructure should make broad policies hard to write by mistake."

The $1.5B Wildcard: When company-frontend-* Matches Production

The Lambda fixture above uses Resource: "*". The CEL predicate sets has_resource_wildcard_on_sensitive: true and the control fires loudly. That is the easy case.

The interesting case is the one the boolean misses. In March 2025, attackers stole $1.5 billion in ETH from Bybit's hot wallet. The attack didn't exploit Bybit's infrastructure directly. It exploited Safe{WALLET}'s. A developer at the wallet provider had an IAM policy roughly like this:

{
  "Effect": "Allow",
  "Action": [
    "s3:GetObject",
    "s3:PutObject",
    "s3:DeleteObject",
    "s3:ListBucket"
  ],
  "Resource": [
    "arn:aws:s3:::company-frontend-*",
    "arn:aws:s3:::company-frontend-*/*"
  ]
}

Every action is a specific named operation; every resource is scoped to a prefix. The CEL boolean has_resource_wildcard_on_sensitive is set to false. The engine is reading "scoped" because the ARN isn't the literal *. The policy looks fine to a heuristic checker.

It is not fine. The prefix company-frontend-* matches both company-frontend-dev (intended) and company-frontend-prod (not intended). The developer could write to production. The production bucket served the application's JavaScript via CloudFront. Compromise the developer's machine, run a single aws s3 cp app.js s3://company-frontend-prod/app.js, and every user of the application loads attacker-supplied code on the next page reload.

This is in the example as fixtures/bybit-pattern-before/. The CEL control stays silent on it. Z3 finds the witness:

=== bybit-pattern-before (developer with s3:PutObject on company-frontend-*) ===
  policy statements: 1
    [0] Effect=Allow
        Action=[s3:GetObject s3:PutObject s3:DeleteObject s3:ListBucket]
        Resource=[arn:aws:s3:::company-frontend-*
                  arn:aws:s3:::company-frontend-*/*]
  buckets observed:  2
    - company-frontend-prod   environment=production   served_via=cloudfront
    - company-frontend-dev   environment=development   served_via=

  --- Bybit Pattern: Developer Write to Production S3 ---
  verdict: SAT
  witness: s3:PutObject on arn:aws:s3:::company-frontend-prod/app.js
           (resource pattern matches both dev and prod)
  rationale: environment=production, served_via=cloudfront — modifying
             app.js is a supply chain attack via CloudFront

Z3 enumerates buckets by integer index, asks for an admitted-by-policy witness whose environment tag is production, and reports the prod bucket. The prefix wildcard the heuristic accepted is the same wildcard Z3 makes concrete.

The compound finding — undetectable supply chain

Write access to production isn't enough on its own. The attacker needs the write to be invisible. Z3's second query compounds four conditions:

write_access_to_prod   ∧   no_mfa_condition   ∧
no_ip_condition        ∧   no_object_logging

Each is independently not remarkable. Together they describe the Bybit attack:

  --- Compound: Undetectable Production Write ---
  verdict: SAT
  witness: developer can write to production S3 from any IP,
           without MFA, with no CloudTrail data-event record
  rationale: write_access=true   no_mfa=true   no_ip=true   no_logging=true

A heuristic scanner would issue four separate alerts ("policy is broad", "no MFA condition", "no IP restriction", "data events disabled"). Most of which look like reasonable choices in isolation. Together they are the attack path. Z3 finds the conjunction.

Why this is the harder case

The Lambda example fires on the CEL boolean. The Bybit example does not. It caused a $1.5 billion theft. Because the unsafe state is a join across multiple assets:

The CEL control isn't broken. It's working as designed: it detects what its boolean field encodes, and the boolean encodes "literal Resource:*". The policy that took down Safe{WALLET} doesn't have that. It has a prefix wildcard that, paired with the bucket naming convention, admits the action that mattered.

This is the case for two-level architecture. The CEL boolean covers the obvious case in milliseconds. The Z3 prover covers the conjunctive case with the same observation file, same asset graph, different reasoning depth. Both fire on fixtures that ship with this article. One catches the easy case; the other catches the case that happens.

The fix is one character

company-frontend-* → company-frontend-dev.

The remediated fixture splits the policy into
two statements: full read/write on dev, read-only on prod.
Z3 reports UNSAT on both queries:

  --- Bybit Pattern: Developer Write to Production S3 ---
  verdict: UNSAT
  rationale: no production bucket admitted by s3:PutObject

  --- Compound: Undetectable Production Write ---
  verdict: UNSAT
  rationale: write_access=false   no_mfa=true   no_ip=true   no_logging=true

One character difference between the policies that enabled the largest cryptocurrency theft in history. The infrastructure question — how do you make that mistake hard to commit by accident is the same one the Lambda example raises. The answer is the same: typed IaC modules, SCPs that deny prefix-wildcard resources on production buckets, and a checker that reasons about which buckets the wildcard admits, not just whether it looks like a wildcard.

The example at iam-overpermission-wildcard is two binaries side by side: a CEL evaluation via pkg/stave.Apply (asserts the unsafe state when the attached policy has a wildcard sensitive action) and a Z3 SAT prover (extracts a concrete dangerous action the policy admits — s3:PutBucketPolicy on customer-pii-bucket in the demo). 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.