Reach

Prove what cloud credentials, and the AI agents holding them, can actually reach.

AI agents run with real credentials: an AWS profile on a laptop, a GitHub token in an MCP config, a write token in a CI job. Reach finds those agents and the credentials they can use. It proves what those credentials can do in AWS. And it reports the agents that combine untrusted input, private data and a way to send data out (the lethal trifecta), with the cheapest way to break each one.

pip install reach-security
reach agents --project .                      # agents, tools, credentials, trifecta findings
reach can --authz authz.json --principal dev secretsmanager:GetSecretValue '*'

Try it on the deliberately vulnerable examples/reach-goat.

How the reasoning works

Reach compiles AWS IAM policies into SMT constraints and asks Z3 whether a principal can perform an action on a resource. Every answer is one of three verdicts, and Reach never rounds an unknown up or down:

Every verdict is checked three ways. A second, solver-free implementation replays each witness. A fuzzer checks the two implementations against each other. And AWS's own policy simulator plus a live S3 test check both against AWS: see validation/FINDINGS.md, which includes an error in AWS's simulator that Reach found.

Status: alpha (0.1.0). See the roadmap.

Example

$ aws iam get-account-authorization-details --output json > authz.json
$ reach can --authz authz.json --principal alice ec2:RunInstances '*'
DENIED  ec2:RunInstances on *
  principal  arn:aws:iam::123456789012:user/alice
  proof      no request context satisfies the policies (UNSAT)
  why        Implicitly denied by permissions boundary dev-boundary: it allows no request the identity policies allow.

$ reach can --policy admin-with-mfa.json iam:CreateAccessKey '*'
ALLOWED  iam:CreateAccessKey on *
  principal  arn:aws:iam::111122223333:role/reach-adhoc
  witness    iam:CreateAccessKey on arn:aws:iam::…
             aws:MultiFactorAuthPresent = "true"

Queries are existential: reach can … 's3:*' 'arn:aws:s3:::customer-pii/*' asks whether any S3 action on any object in the bucket is reachable, and the witness shows one.

Agents

$ reach agents --project . --resolve --authz authz.json

reach agents finds AI agents (Claude Code, Claude Desktop, Cursor, VS Code, Windsurf), the MCP servers each one runs, and the credentials each server is handed, plus ambient credentials that any agent with shell access can read. It reads each agent's shell mode from its own permission settings, finds AI agents in GitHub Actions workflows (and flags those triggered by text anyone can write while holding write tokens or secrets), flags secrets hardcoded in agent configs or committed in .env files, and never prints a secret value. With --resolve it signs each reachable AWS profile in to find its principal (read-only sts:GetCallerIdentity). With --authz it then asks the engine what that principal can do: read secrets, decrypt with KMS, read or write S3, modify IAM, assume roles, start compute.

Lethal trifecta

For every agent, Reach then checks for Simon Willison's lethal trifecta: untrusted input (text an attacker can write reaches the agent), private data (it can read something sensitive) and an exfiltration channel (it can send data out). Each leg is derived from evidence: built-in tools and the agent's own denied tools, its shell mode, its MCP servers (classified by a small documented catalogue; unknown servers are reported, not guessed), credentials it is handed, ambient credentials when it has a shell, proven AWS capabilities from --authz, and for CI agents their triggers, if: gates, token permissions and secrets. All three legs with an ungated way each is critical; all three behind a human approval is high. Reach names the cheapest leg to break.

Not covered yet: injected text inside files the agent reads (a cloned repository, a dependency), and tool calls pre-approved per tool in an agent's settings.

What is modelled

• Identity-based policies (inline, managed, group), permissions boundaries, session policies.
• SCPs as layers (root → OU → account), each of which must allow; the management account and service-linked roles are exempt.
• Explicit Deny from every policy type.
• Resource-based policies (bucket, key, trust policies): Principal/NotPrincipal matching, same-account grant paths (direct user, role and session grants; account grants delegate), required policies (role trust, KMS), and cross-account access needing both sides. With --authz, sts:AssumeRole queries load the role's trust policy.
• Action/NotAction, Resource/NotResource, IAM wildcards. Actions match case-insensitively; resource ARNs match segment by segment.
• Conditions: String(Not)Equals, String(Not)Like, Arn(Not)Equals, Arn(Not)Like, Bool, Null, Numeric*, Date*, IpAddress/NotIpAddress, and the …IfExists forms. Missing keys follow AWS semantics: positive operators fail, negated ones pass.
  • IP keys are 32-bit bitvectors, so CIDR matching is exact; time keys are epoch seconds, and aws:CurrentTime and aws:EpochTime share one clock, so a policy cannot be satisfied by two inconsistent times.
• The principal's own context is pinned: aws:PrincipalArn, aws:PrincipalAccount, aws:PrincipalTag/*.
• A catalogue of real IAM actions, built from AWS's Service Authorization Reference, so wildcard queries range over actions that exist.

Not modelled yet

These are always reported as UNKNOWN rather than guessed: ForAnyValue/ForAllValues; policy variables (${aws:username}); multi-valued keys; IPv6 networks; decimal or signed numbers; StringEqualsIgnoreCase and Binary*. RCPs are not part of the decision yet. Whether a Principal: "*" grant is capped by a permissions boundary or session policy is reported as UNKNOWN until verified against AWS. See the roadmap.

How Reach checks itself

• Every ALLOWED/UNKNOWN witness is replayed through a second, solver-free implementation of the evaluation logic (reach.reference). If they disagree, Reach raises an error instead of reporting a verdict.
• validation/fuzz.py generates random principals (identity policies, boundaries, SCP layers, session policies, modelled and unmodelled conditions) and demands exact agreement between the two implementations, plus soundness of every DENIED proof against sampled concrete requests.
• validation/aws_simulator.py compares Reach with AWS's own IAM policy simulator, the only check that can catch a misreading of AWS semantics that both implementations share. It has already found one real Reach bug and two modelling gaps; see validation/FINDINGS.md.

Development

python -m pip install -e ".[dev]"
python -m pytest
python -m validation.fuzz --cases 5000   # longer differential fuzzing campaign
python scripts/build_catalog.py   # refresh the action catalogue

License

AGPL-3.0-or-later.