From f85d454036de5848139d9e33567d3ffc0d7c33eb Mon Sep 17 00:00:00 2001 From: Amin Chirazi Date: Tue, 28 Jul 2026 07:33:21 +0000 Subject: [PATCH] feat(loop): a constitution the autonomous loops cannot edit The loops' safety rests on one property: green CI means the work is sound. An agent optimising for green has two routes - do the work, or weaken the thing that measures the work - and the second is always cheaper. So the files that constrain the loops have to be outside their reach, or there is no fixed point. `scripts/gate/constitution-check.sh` refuses any change to CHARTER.md, CODEOWNERS, scripts/gate/, or .github/workflows/ unless the PR author is on a human allowlist. It fails closed: an identity not on the list is treated as a loop, so a new loop is constrained the moment it exists. The logic is a script rather than inline YAML so it is testable, and the workflow runs its 24 cases on every PR - including the case that a loop cannot edit the check itself. The gate lives in scripts/gate/ and not .loop/: .loop/ is gitignored local scratch ("not product"), and a gate has to be committed to be enforceable. This is one of three independent locks. The others are the loop credential's scope and branch protection requiring the `constitution` check - which must be added to the required list once this lands, since a check that never reports is what stops a PR deleting the job. Co-Authored-By: Claude Opus 5 --- .github/workflows/constitution.yml | 40 +++++ scripts/gate/README.md | 225 ++++++++++++++++++++++++ scripts/gate/constitution-check.sh | 70 ++++++++ scripts/gate/constitution-check.test.sh | 66 +++++++ scripts/gate/protection.json | 20 +++ scripts/gate/ruleset-repo-guard.json | 29 +++ scripts/gate/sandbox-run.sh | 71 ++++++++ scripts/gate/token-scope-check.sh | 134 ++++++++++++++ 8 files changed, 655 insertions(+) create mode 100644 .github/workflows/constitution.yml create mode 100644 scripts/gate/README.md create mode 100755 scripts/gate/constitution-check.sh create mode 100755 scripts/gate/constitution-check.test.sh create mode 100644 scripts/gate/protection.json create mode 100644 scripts/gate/ruleset-repo-guard.json create mode 100755 scripts/gate/sandbox-run.sh create mode 100755 scripts/gate/token-scope-check.sh diff --git a/.github/workflows/constitution.yml b/.github/workflows/constitution.yml new file mode 100644 index 0000000..59349fa --- /dev/null +++ b/.github/workflows/constitution.yml @@ -0,0 +1,40 @@ +# Refuse a loop-authored change to the files that constrain the loops. +# +# One of three independent locks. The other two are the loop credential's scope +# (it cannot push workflow changes) and branch protection listing `constitution` +# as a required check. They fail independently, which is the point. +# +# Deliberately NOT gated on ci.yml's `what changed` scope filter: a docs-only PR +# can still touch CHARTER.md, so this must run on every pull request. +# +# On self-protection: a `pull_request` run uses the workflow file from the PR's +# own merge commit, so a PR that DELETES this job runs without it. That is +# survivable only because a required status check which never reports blocks the +# merge - which is why adding `constitution` to the required checks list is not +# optional. See scripts/gate/README.md. +name: constitution + +on: + pull_request: + types: [opened, synchronize, reopened] + +permissions: + contents: read + +jobs: + constitution: + name: constitution + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + + - name: the gate's own tests + run: ./scripts/gate/constitution-check.test.sh + + - name: protected paths are human-authored only + env: + AUTHOR: ${{ github.event.pull_request.user.login }} + BASE_REF: ${{ github.base_ref }} + run: ./scripts/gate/constitution-check.sh diff --git a/scripts/gate/README.md b/scripts/gate/README.md new file mode 100644 index 0000000..1569c33 --- /dev/null +++ b/scripts/gate/README.md @@ -0,0 +1,225 @@ +# loop-gate + +The two mechanical guards the autonomous loops need before they can run +unattended, plus the branch-protection payload. Intended home: `scripts/gate/` +in the flowproof repo — a path the CI scope filter already knows about — and +inside the constitution's human-write-only set, since these are what constrain +the loops. + +## `token-scope-check.sh` + +Run at the start of every loop session; non-zero exit means do not proceed. + +Blocker #4: the interactive `gh` login on this box carries `repo` + `workflow`. +`workflow` lets a loop rewrite `.github/workflows/**`, and `repo` on a repo you +admin reaches the branch-protection API. A system whose only safety property is +"CI must be green" must not give its agents a credential that can edit CI. + +Four checks, in ascending order of how much they prove: + +1. The loop token is not the interactive `gh` login. +2. No `workflow` / `admin:org` / `site_admin` / `delete_repo` scope. +3. **A live capability probe: the token must get 403/404 on the branch-protection + endpoint.** This is the check that matters — scope strings can mislead, a 403 + cannot. +4. It can still list pull requests, i.e. it is not so restricted it cannot work. + +### The token you need to mint + +This is the one step that cannot be automated: it needs the GitHub web UI, and +minting a credential should be yours. Create a **fine-grained personal access +token** at `Settings → Developer settings → Personal access tokens → Fine-grained`: + +- Resource owner: `automators-com`, repository: `flowproof` only +- Repository permissions — **Contents: Read and write**, **Pull requests: Read + and write**, **Issues: Read and write** (the ledger and escalation need it), + **Metadata: Read** (mandatory) +- Everything else: **No access**. Specifically *not* Actions, *not* + Administration, *not* Workflows. +- Expiry: 90 days maximum, calendared for rotation + +Then, readable only by you and never passed into a container: + +```bash +install -m 600 /dev/null ~/.config/flowproof-loop.env +printf 'FLOWPROOF_LOOP_TOKEN=github_pat_...\n' > ~/.config/flowproof-loop.env +``` + +Loops source that file. `sandbox-run.sh` passes no `-e` flags at all, so it +cannot reach the corpus containers. + +## `sandbox-run.sh` + +Blocker #2: a corpus repo's `npm install` runs arbitrary postinstall scripts, +and this box holds `~/.ssh/flowproof_deploy` and a `gh` token. That risk is not +recoverable by revert, which makes it the most serious one in the design. + +Two-phase network, matching the concept: `--phase install` allows egress for +dependency fetch and model recording; `--phase replay` uses `--network=none`, +which is also a free mechanical proof of flowproof's zero-LLM-call claim. + +Verified on this box, all six passing: + +| Test | Property | +|---|---| +| T1 | replay phase has no egress | +| T2 | `~/.ssh` invisible inside the container | +| T3 | host env does not leak (`FLOWPROOF_LOOP_TOKEN`, `ANTHROPIC_API_KEY`) | +| T4 | install phase *does* have egress | +| T5 | memory cap enforced (rootless cgroup v2 delegation works) | +| T6 | refuses to mount anything outside the scratch allowlist | + +T6 exists because a typo in `--work` would mount the very credentials the script +is there to isolate. + +## `protection.json` + +Branch protection payload for `main`. **Not applied** — the API call was +blocked by the permission classifier, correctly, since it writes your repo +settings. Apply with: + +```bash +gh api -X PUT repos/automators-com/flowproof/branches/main/protection --input protection.json +``` + +Two deliberate choices worth understanding before you run it: + +- **`enforce_admins: false`** — you keep a direct-push escape hatch. The loops + are constrained by their *token scope*, not by admin enforcement, so this + costs no safety and preserves your ability to hotfix and to clear the circuit + breaker. +- **`required_pull_request_reviews: null`** (zero approvals) — required for + autonomous merge. If you ever want the Adversary's sign-off to be + *mechanically* required rather than advisory, it needs its own GitHub identity + and this becomes `1`. Worth knowing that today the Adversary is advisory only. + +**`strict: true`** is load-bearing: it forces a branch to be up to date before +merging, which mechanically enforces the rebase-and-recheck that catches the +semantic conflicts described in the concept (two independently-green PRs that +break `main` together). + +The five required checks are the ones that always report. `windows build + E2E` +and `web E2E (ubuntu)` are deliberately excluded — they are off the PR path by +design (~50 min), and the Integrator covers them post-merge on `main`. + +## Applied state, as of this session + +| Gate | Status | +|---|---| +| `protection.json` — branch protection on `main` | **applied**, verified server-side | +| `ruleset-repo-guard.json` — repo ruleset id `19879637` | **applied**, both flags `true` | +| `ruleset-hardened.json` | **superseded, do not use** — wrong endpoint (see below) | +| Loop credential + Adversary identity | **not done**, needs the GitHub web UI | + +### Why `ruleset-hardened.json` is dead + +The `default` ruleset (id 7514604) has `source_type: "Organization"` — it belongs +to `automators-com`, and flowproof merely inherits it. The repo owns no rulesets +of its own. So `PUT /repos/.../rulesets/7514604` returns **404**: wrong endpoint. + +The correct endpoint is `/orgs/automators-com/rulesets/7514604`, which needs +`admin:org` scope and would change the gate for **every repo in the org**. Not +worth it to harden one repo. + +Instead, `ruleset-repo-guard.json` **creates a repo-level ruleset** that stacks +on top of the org one, adding only the `pull_request` rule with the two flags +set. No `admin:org`, no blast radius. + +### The stacking is applied but its resolution is unverified + +`GET /repos/automators-com/flowproof/rules/branches/main` reports **two separate +`pull_request` rules**, not one merged rule: + +``` +pull_request from=Organization dismiss_stale=false last_push_approval=false reviews=1 +pull_request from=Repository dismiss_stale=true last_push_approval=true reviews=1 +``` + +GitHub documents that the most restrictive value wins across overlapping +rulesets, so `true` should apply. But `dismiss_stale_reviews_on_push` is a +*behavior* performed on push rather than a condition a push must satisfy, and the +API exposes both rules side by side rather than a resolved value. **This is +documented behavior, not observed behavior.** + +Settle it empirically as soon as the Adversary identity exists: + +1. Adversary approves a test PR. +2. Push one more commit to that PR. +3. Check whether the approval was dismissed (`gh pr view N --json reviewDecision`). + +If it was not dismissed, the org ruleset is winning and the two flags must move +to the org level after all — which means `admin:org` and an org-wide change. +Until this is checked, treat the stale-approval hole as **probably closed, not +provably closed**. + +### External dependency worth knowing + +The org ruleset means `automators-com` policy is part of flowproof's gate, and +anyone with org admin can change it without touching this repo. For an autonomous +system whose safety rests on the gate, that is an external dependency the +constitution cannot protect. + +## `ruleset-hardened.json` — superseded, kept for reference only + +`protection.json` is applied and live. But branch protection was never the only +gate: an **active repo ruleset** (`default`, id 7514604) independently enforces +`required_approving_review_count: 1`, `copilot_code_review`, `non_fast_forward`, +and `deletion` on `main` / `dev`. Rulesets and branch protection are separate +mechanisms and GitHub enforces the **union**, so +`required_pull_request_reviews: null` in `protection.json` never removed the +review requirement — it was not coming from there. + +This is good news: the mechanism for enforced adversarial review already exists. +Give the Adversary its own GitHub identity and `required_approving_review_count: +1` becomes real enforcement rather than advice. GitHub blocks self-approval, so +Builder ≠ Adversary comes for free. + +Two flags were open holes under autonomy, and this payload closes them: + +| Flag | Was | Now | Why | +|---|---|---|---| +| `dismiss_stale_reviews_on_push` | `false` | `true` | otherwise an approval survives later commits | +| `require_last_push_approval` | `false` | `true` | otherwise the Builder gets sign-off on one diff and merges another | + +Everything else is preserved byte-for-byte from live state — all four rule +types, both bypass actors, the ref conditions. Verified by diffing against +`ruleset-current.json` (captured before any change). + +```bash +gh api -X PUT repos/automators-com/flowproof/rulesets/7514604 --input ruleset-hardened.json +``` + +`PUT` replaces the ruleset, which is why the payload is complete rather than a +partial patch. `ruleset-current.json` is the rollback. + +### The bypass trap — this supersedes the token advice above + +The fine-grained-PAT recommendation is **necessary but not sufficient**. Ruleset +bypass is evaluated on the **actor's role**, not the token's scopes. The bypass +list contains `OrganizationAdmin` and `RepositoryRole: 5` (admin) at +`bypass_mode: always`. A fine-grained PAT owned by an admin account acts as that +admin, so it would sail past the review requirement no matter how narrow its +permissions are — the gate would look enforced and be theoretical. + +The loops need a **separate identity with `write`**: a machine user added as a +collaborator, or a GitHub App. Not a weaker token on your account. +`token-scope-check.sh` check 5 enforces this, and it is the reason that check +exists. + +Your own admin bypass is deliberately left in place — it is the human escape +hatch, the same role `enforce_admins: false` plays in `protection.json`. + +### Test status of the checks + +Honest accounting: check 1 (token ≠ interactive login) is verified, and it +short-circuits — so **checks 2–5 are syntax-valid but unexercised**. They cannot +be tested until a real loop credential exists. Run the script once against the +new token before trusting it, and expect to debug the `sed`-based JSON parsing; +`jq` is not installed on this box, which is why the parsing is done with `sed`. + +## Ratchet baseline note + +The concept quotes 651 Rust tests from a static count of `#[test]` attributes. +A Linux run reports **644 passed** — the difference is platform-gated tests +(`cfg(windows)`) that never execute here. The ratchet must count *attributes*, +not runtime passes, or it will read as regressed depending on which OS ran it. diff --git a/scripts/gate/constitution-check.sh b/scripts/gate/constitution-check.sh new file mode 100755 index 0000000..9ae5f7f --- /dev/null +++ b/scripts/gate/constitution-check.sh @@ -0,0 +1,70 @@ +#!/usr/bin/env bash +# Refuse a change to the files that constrain the autonomous loops. +# +# The loops' safety rests on one property: "CI is green" means the work is sound. +# An agent optimising for green has two routes - do the work, or weaken the thing +# that measures the work. The second is always cheaper. So the charter the loops +# take direction from, the gate scripts, and CI itself must be outside their +# reach, or the system has no fixed point. +# +# Lives in scripts/gate/ rather than .loop/ because .loop/ is gitignored local +# scratch ("not product"), and the gate has to be committed to be enforceable. +# +# Called by .github/workflows/constitution.yml. Kept as a script rather than +# inline YAML so the logic is testable directly - see constitution-check.test.sh. +# +# Usage: +# AUTHOR= BASE_REF= constitution-check.sh +# AUTHOR= CHANGED_FILES="a b c" constitution-check.sh # test mode +# +# Exit 0 = allowed, 1 = refused, 2 = misconfigured. +set -euo pipefail + +# Anything that constrains the loops. `scripts/gate/` only: the loops own the +# rest of scripts/ and must stay free to work there. +PROTECTED='^(CHARTER\.md|CODEOWNERS|scripts/gate/|\.github/workflows/)' + +# Fail-closed: anyone NOT on this list is treated as a loop, so a new loop +# identity is constrained the moment it exists with no edit here required. This +# list living inside a protected path is deliberate - a loop cannot add itself. +HUMANS="${HUMANS:-AminChirazi}" + +AUTHOR="${AUTHOR:-}" +[ -n "$AUTHOR" ] || { echo "AUTHOR is unset" >&2; exit 2; } + +if [ -n "${CHANGED_FILES:-}" ]; then + changed="$(printf '%s\n' $CHANGED_FILES)" +else + base="$(git merge-base "origin/${BASE_REF:?BASE_REF is unset}" HEAD)" + changed="$(git diff --name-only "$base" HEAD)" +fi + +touched="$(printf '%s\n' "$changed" | grep -E "$PROTECTED" || true)" + +if [ -z "$touched" ]; then + echo "no protected path touched" + exit 0 +fi + +echo "this change touches protected paths:" +printf '%s\n' "$touched" | sed 's/^/ /' + +for h in $HUMANS; do + if [ "$AUTHOR" = "$h" ]; then + echo + echo "author '$AUTHOR' is human-authorised: allowed" + exit 0 + fi +done + +echo +echo "::error::author '$AUTHOR' may not modify the constitution." +cat <<'MSG' + +These paths define what constrains the autonomous loops: the charter they take +direction from, the gate scripts, and CI itself. A loop that can edit them can +edit its own limits. + +If this change is genuinely needed, a human opens it. +MSG +exit 1 diff --git a/scripts/gate/constitution-check.test.sh b/scripts/gate/constitution-check.test.sh new file mode 100755 index 0000000..f723217 --- /dev/null +++ b/scripts/gate/constitution-check.test.sh @@ -0,0 +1,66 @@ +#!/usr/bin/env bash +# Tests for constitution-check.sh. Drives the real script via CHANGED_FILES so +# these cases cannot drift from the logic they check. +# +# Run directly, or via the `constitution` workflow which runs it on every PR. +cd "$(dirname "$0")" +SUT=./constitution-check.sh +FAILED=0 + +t() { # t + local want="$1" desc="$2" author="$3"; shift 3 + local got + if AUTHOR="$author" CHANGED_FILES="$*" "$SUT" >/dev/null 2>&1; then + got=ALLOW + else + got=BLOCK + fi + if [ "$got" = "$want" ]; then + printf 'ok %-50s %s\n' "$desc" "$got" + else + printf 'FAIL %-50s got %s, wanted %s\n' "$desc" "$got" "$want" + FAILED=1 + fi +} + +echo "-- a loop must not reach the things that constrain it --" +t BLOCK "loop edits CI" loop-bot .github/workflows/ci.yml +t BLOCK "loop edits the constitution job" loop-bot .github/workflows/constitution.yml +t BLOCK "loop edits the charter" loop-bot CHARTER.md +t BLOCK "loop edits a gate script" loop-bot scripts/gate/token-scope-check.sh +t BLOCK "loop edits this very check" loop-bot scripts/gate/constitution-check.sh +t BLOCK "loop edits the gate's tests" loop-bot scripts/gate/constitution-check.test.sh +t BLOCK "loop edits the branch-protection json" loop-bot scripts/gate/protection.json +t BLOCK "loop edits CODEOWNERS" loop-bot CODEOWNERS +t BLOCK "loop buries it among normal files" loop-bot crates/a/src/lib.rs docs/b.md .github/workflows/ci.yml + +echo "-- but must stay free to do its actual work --" +t ALLOW "loop edits engine code" loop-bot crates/flowproof-trace/src/cassette.rs +t ALLOW "loop edits a non-gate script" loop-bot scripts/demo/fake_model.py +t ALLOW "loop edits docs" loop-bot docs/trace-format.md +t ALLOW "loop adds a cassette" loop-bot tests/flowproof/new.cassette.json +t ALLOW "loop touches nothing protected" loop-bot README.md + +echo "-- a human bypasses --" +t ALLOW "human edits CI" AminChirazi .github/workflows/ci.yml +t ALLOW "human edits the charter" AminChirazi CHARTER.md +t ALLOW "human edits a gate script" AminChirazi scripts/gate/constitution-check.sh + +echo "-- near-misses that must NOT be protected --" +t ALLOW "a doc merely named like the gate" loop-bot docs/gate-notes.md +t ALLOW "a charter copy in a subdirectory" loop-bot docs/CHARTER.md +t ALLOW "a workflow-like path outside .github" loop-bot crates/x/workflows/mod.rs +t ALLOW "a gate-like path outside scripts/" loop-bot crates/gate/src/lib.rs + +echo "-- an unknown identity is treated as a loop (fail-closed) --" +t BLOCK "unknown actor edits CI" some-new-bot .github/workflows/ci.yml +t BLOCK "a bot account edits CI" dependabot[bot] .github/workflows/ci.yml + +echo "-- misconfiguration must not silently pass --" +if CHANGED_FILES="CHARTER.md" ./constitution-check.sh >/dev/null 2>&1; then + printf 'FAIL %-50s AUTHOR unset was allowed\n' "unset AUTHOR is rejected"; FAILED=1 +else + printf 'ok %-50s BLOCK\n' "unset AUTHOR is rejected" +fi + +exit "$FAILED" diff --git a/scripts/gate/protection.json b/scripts/gate/protection.json new file mode 100644 index 0000000..bde8330 --- /dev/null +++ b/scripts/gate/protection.json @@ -0,0 +1,20 @@ +{ + "required_status_checks": { + "strict": true, + "contexts": [ + "what changed", + "versions agree", + "fmt + clippy + test (ubuntu)", + "build + test (ubuntu)", + "ruff + pytest (sdk/python)" + ] + }, + "enforce_admins": false, + "required_pull_request_reviews": null, + "restrictions": null, + "allow_force_pushes": false, + "allow_deletions": false, + "block_creations": false, + "required_conversation_resolution": false, + "required_linear_history": false +} diff --git a/scripts/gate/ruleset-repo-guard.json b/scripts/gate/ruleset-repo-guard.json new file mode 100644 index 0000000..024645c --- /dev/null +++ b/scripts/gate/ruleset-repo-guard.json @@ -0,0 +1,29 @@ +{ + "name": "flowproof-autonomous-guard", + "target": "branch", + "enforcement": "active", + "conditions": { + "ref_name": { + "exclude": [], + "include": ["refs/heads/main"] + } + }, + "bypass_actors": [ + { "actor_id": null, "actor_type": "OrganizationAdmin", "bypass_mode": "always" }, + { "actor_id": 5, "actor_type": "RepositoryRole", "bypass_mode": "always" } + ], + "rules": [ + { + "type": "pull_request", + "parameters": { + "allowed_merge_methods": ["merge", "squash", "rebase"], + "dismiss_stale_reviews_on_push": true, + "require_code_owner_review": false, + "require_last_push_approval": true, + "required_approving_review_count": 1, + "required_review_thread_resolution": false, + "required_reviewers": [] + } + } + ] +} diff --git a/scripts/gate/sandbox-run.sh b/scripts/gate/sandbox-run.sh new file mode 100755 index 0000000..b2b151e --- /dev/null +++ b/scripts/gate/sandbox-run.sh @@ -0,0 +1,71 @@ +#!/usr/bin/env bash +# Run untrusted third-party corpus code in a disposable rootless container. +# +# Blocker #2 from the concept: a corpus repo's `npm install` executes arbitrary +# postinstall scripts. This box holds ~/.ssh/flowproof_deploy and a gh token, so +# a stranger's postinstall must never share a trust domain with them. That risk +# is not recoverable by revert, which makes it the most serious in the design. +# +# Two-phase network, matching the concept: +# --phase install : egress allowed (dependency fetch, model recording) +# --phase replay : egress DENIED (proves flowproof's zero-LLM-call claim) +# +# Usage: +# sandbox-run.sh --phase install --work /path/to/repo -- npm ci +# sandbox-run.sh --phase replay --work /path/to/repo -- flowproof run flow.yaml +set -euo pipefail + +IMAGE="${SANDBOX_IMAGE:-docker.io/library/node:22-bookworm-slim}" +PHASE="install" +WORK="" +MEM="${SANDBOX_MEM:-2g}" +CPUS="${SANDBOX_CPUS:-1.5}" +PIDS="${SANDBOX_PIDS:-512}" +TIMEOUT="${SANDBOX_TIMEOUT:-900}" + +while [ $# -gt 0 ]; do + case "$1" in + --phase) PHASE="$2"; shift 2 ;; + --work) WORK="$2"; shift 2 ;; + --image) IMAGE="$2"; shift 2 ;; + --) shift; break ;; + *) echo "unknown arg: $1" >&2; exit 2 ;; + esac +done + +[ -n "$WORK" ] || { echo "--work is required" >&2; exit 2; } +[ $# -gt 0 ] || { echo "no command given after --" >&2; exit 2; } +[ -d "$WORK" ] || { echo "work dir does not exist: $WORK" >&2; exit 2; } + +# The work dir must be a scratch path, never the repo or the home dir. A typo +# here would mount the credentials we are trying to isolate. +case "$(realpath "$WORK")" in + /home/flow/worktrees/*|/home/flow/corpus/*|/tmp/*) ;; + *) echo "refusing to mount $(realpath "$WORK"): work dirs must live under + /home/flow/worktrees, /home/flow/corpus, or /tmp" >&2; exit 2 ;; +esac + +case "$PHASE" in + install) NET=(--network=slirp4netns) ;; + replay) NET=(--network=none) ;; + *) echo "--phase must be 'install' or 'replay'" >&2; exit 2 ;; +esac + +# No -e flags anywhere: the container inherits none of this shell's environment, +# so FLOWPROOF_LOOP_TOKEN / ANTHROPIC_API_KEY / SSH_AUTH_SOCK cannot leak in. +# Only $WORK is mounted, and nothing else from the host filesystem. +exec timeout --signal=KILL "$TIMEOUT" \ + podman run --rm \ + "${NET[@]}" \ + --volume "$WORK:/work:rw,Z" \ + --workdir /work \ + --memory "$MEM" \ + --cpus "$CPUS" \ + --pids-limit "$PIDS" \ + --cap-drop=ALL \ + --security-opt no-new-privileges \ + --read-only \ + --tmpfs /tmp:rw,size=512m,exec \ + --tmpfs /run:rw,size=64m \ + "$IMAGE" \ + "$@" diff --git a/scripts/gate/token-scope-check.sh b/scripts/gate/token-scope-check.sh new file mode 100755 index 0000000..d2d8e57 --- /dev/null +++ b/scripts/gate/token-scope-check.sh @@ -0,0 +1,134 @@ +#!/usr/bin/env bash +# Verify the loop credential cannot edit the gate it is judged by. +# +# Blocker #4 from the autonomous-development concept: a token with `workflow` +# scope can rewrite .github/workflows/**, and a classic PAT with `repo` on a +# repo you admin reaches the branch-protection API. A system whose only safety +# property is "CI must be green" must not hand its agents a credential that can +# edit CI. +# +# Run this at the start of every loop session. Exit non-zero => do not proceed. +# +# Usage: FLOWPROOF_LOOP_TOKEN=github_pat_... ./token-scope-check.sh +set -euo pipefail + +REPO="${FLOWPROOF_REPO:-automators-com/flowproof}" +TOKEN="${FLOWPROOF_LOOP_TOKEN:-}" + +fail() { printf '\033[31mFAIL\033[0m %s\n' "$1" >&2; exit 1; } +pass() { printf '\033[32mok\033[0m %s\n' "$1"; } +warn() { printf '\033[33mwarn\033[0m %s\n' "$1"; } + +[ -n "$TOKEN" ] || fail "FLOWPROOF_LOOP_TOKEN is unset. Loops must never fall back + to the interactive gh login, which carries repo+workflow scope." + +# --------------------------------------------------------------------------- +# 1. The token must not be the interactive gh login. +# --------------------------------------------------------------------------- +if command -v gh >/dev/null 2>&1; then + if interactive="$(gh auth token 2>/dev/null)"; then + [ "$TOKEN" != "$interactive" ] || fail "the loop token IS the interactive gh + login. Mint a separate least-privilege credential (see README in this dir)." + fi +fi +pass "distinct from the interactive gh login" + +# --------------------------------------------------------------------------- +# 2. Classic tokens: read the granted scopes off a live API response. +# Fine-grained tokens (github_pat_*) report no X-OAuth-Scopes header at all, +# which is itself the desired answer. +# --------------------------------------------------------------------------- +hdrs="$(curl -sS -D - -o /dev/null -H "Authorization: Bearer ${TOKEN}" \ + https://api.github.com/user 2>/dev/null || true)" + +status="$(printf '%s' "$hdrs" | awk 'NR==1{print $2}')" +[ "$status" = "200" ] || fail "token rejected by the API (HTTP ${status:-none})." + +scopes="$(printf '%s' "$hdrs" \ + | tr -d '\r' \ + | awk -F': ' 'tolower($1)=="x-oauth-scopes"{print $2}')" + +if [ -z "$scopes" ]; then + pass "fine-grained token (no OAuth scopes granted)" +else + warn "classic token with scopes: ${scopes}" + for bad in workflow admin:org site_admin delete_repo; do + case ",${scopes// /}," in + *",${bad},"*) fail "token carries '${bad}' scope. It can edit the gate. + Fine-grained token with contents:write + pull_requests:write only." ;; + esac + done + pass "no workflow/admin scope" +fi + +# --------------------------------------------------------------------------- +# 3. Capability probe: the token must NOT be able to read, and therefore not +# write, branch protection. This is the check that actually matters -- +# scope strings can mislead, a 403 cannot. +# --------------------------------------------------------------------------- +code="$(curl -sS -o /dev/null -w '%{http_code}' \ + -H "Authorization: Bearer ${TOKEN}" \ + "https://api.github.com/repos/${REPO}/branches/main/protection" 2>/dev/null || echo 000)" + +case "$code" in + 200) fail "token can READ branch protection => it is admin-capable and can + disable the gate. Reduce it to contents:write + pull_requests:write." ;; + 403|404) pass "cannot reach branch protection (HTTP ${code})" ;; + *) fail "unexpected status ${code} probing branch protection." ;; +esac + +# --------------------------------------------------------------------------- +# 4. It must still be able to do its actual job. +# --------------------------------------------------------------------------- +code="$(curl -sS -o /dev/null -w '%{http_code}' \ + -H "Authorization: Bearer ${TOKEN}" \ + "https://api.github.com/repos/${REPO}/pulls?per_page=1" 2>/dev/null || echo 000)" +[ "$code" = "200" ] || fail "token cannot list pull requests (HTTP ${code}); it + is too restricted to open PRs." +pass "can read pull requests" + +# --------------------------------------------------------------------------- +# 5. The loop must not be able to BYPASS the review ruleset. +# +# This is the check the earlier design missed. The `default` ruleset requires +# 1 approving review, and its bypass list contains OrganizationAdmin and +# RepositoryRole 5 (admin). Bypass is evaluated on the ACTOR'S ROLE, not on +# the token's scopes -- so a fine-grained PAT owned by an admin sails past +# the review requirement no matter how narrow its permissions are. The gate +# would look enforced and be theoretical. +# +# The loop therefore needs its own identity with `write`, not a weaker token +# on an admin account. +# --------------------------------------------------------------------------- +actor="$(curl -sS -H "Authorization: Bearer ${TOKEN}" \ + https://api.github.com/user 2>/dev/null \ + | tr -d '\r\n ' | sed -n 's/.*"login":"\([^"]*\)".*/\1/p')" +[ -n "$actor" ] || fail "could not resolve the token's login." + +role="$(curl -sS -H "Authorization: Bearer ${TOKEN}" \ + "https://api.github.com/repos/${REPO}/collaborators/${actor}/permission" 2>/dev/null \ + | tr -d '\r\n ' | sed -n 's/.*"role_name":"\([^"]*\)".*/\1/p')" + +case "$role" in + admin|maintain) fail "loop identity '${actor}' has repo role '${role}', which is + in the ruleset's bypass list. It can merge without the Adversary's review. + Use a separate machine account or GitHub App with 'write'." ;; + write|push) pass "actor '${actor}' has role '${role}' (cannot bypass review)" ;; + "") warn "could not read the actor's repo role; verify manually that + '${actor}' is not an admin and not an org owner" ;; + *) fail "unexpected repo role '${role}' for '${actor}'." ;; +esac + +# Direct confirmation when the token can read the ruleset: GitHub reports +# whether the *calling* identity may bypass. "always" is disqualifying. +bypass="$(curl -sS -H "Authorization: Bearer ${TOKEN}" \ + "https://api.github.com/repos/${REPO}/rulesets?includes_parents=true" 2>/dev/null \ + | grep -o '"current_user_can_bypass":"[a-z_]*"' | head -1 | sed 's/.*:"\(.*\)"/\1/')" +case "$bypass" in + always|pull_requests_only) fail "GitHub reports this identity can bypass rulesets + ('${bypass}'). The review gate would not apply to it." ;; + never) pass "GitHub confirms this identity cannot bypass rulesets" ;; + *) warn "ruleset bypass status not readable with this token (role check above stands)" ;; +esac + +printf '\n\033[32mloop credential is correctly scoped and cannot bypass review\033[0m\n'