Metadata-Version: 2.4
Name: reach-security
Version: 0.1.0
Summary: Prove what cloud credentials, and the AI agents holding them, can actually reach - SMT-based AWS IAM reasoning with proofs and witnesses.
Author: Adam
License-Expression: AGPL-3.0-or-later
Project-URL: Homepage, https://github.com/ctrl-adam/Reach
Project-URL: Repository, https://github.com/ctrl-adam/Reach
Keywords: security,aws,iam,cloud-security,smt,z3,formal-verification,ai-agents,privilege-escalation
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Information Technology
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Operating System :: OS Independent
Classifier: Topic :: Security
Classifier: Environment :: Console
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: z3-solver>=4.12
Requires-Dist: ruamel.yaml>=0.18
Provides-Extra: dev
Requires-Dist: pytest>=7.0; extra == "dev"
Requires-Dist: pytest-cov>=4.0; extra == "dev"
Requires-Dist: ruff>=0.6.0; extra == "dev"
Requires-Dist: mypy>=1.10; extra == "dev"
Provides-Extra: aws
Requires-Dist: boto3>=1.34; extra == "aws"
Dynamic: license-file

# Reach

[![CI](https://github.com/ctrl-adam/Reach/actions/workflows/ci.yml/badge.svg)](https://github.com/ctrl-adam/Reach/actions/workflows/ci.yml)
[![License: AGPL-3.0](https://img.shields.io/badge/license-AGPL--3.0-blue.svg)](LICENSE)

**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.

```bash
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`](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:

| Verdict   | Meaning |
|-----------|---------|
| `DENIED`  | **Proof.** No request, no context value and no reading of the unmodelled conditions allows it (UNSAT). Comes with the reason: which layer blocks it, or which Deny covers it. |
| `ALLOWED` | **Witness.** A concrete request that is allowed even when every condition Reach does not model goes against the attacker. |
| `UNKNOWN` | Allowed only if some unmodelled condition goes the attacker's way. Reach lists exactly which assumptions that relies on. |

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](validation/FINDINGS.md), which includes an error in AWS's simulator that Reach found.

> Status: alpha (0.1.0). See the [roadmap](ROADMAP.md).

## Example

```console
$ 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

```console
$ 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](ROADMAP.md).

## 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](validation/FINDINGS.md).

## Development

```bash
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.
