From 9a7a0bd4af4ec6d8e70731334c0776177c74dda0 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 07:15:26 +0000 Subject: [PATCH 1/4] fix(deploy): containment stopgap for api.nesy-prover.dev Owner ruling 2026-11-05. The public API has no authentication, and its execution routes spawn prover binaries on caller input. The unit also ran :latest with AutoUpdate=registry, so every release auto-deployed to production. - Caddyfile: forward only GET/HEAD on /api/health and /api/provers. Every other request gets a 403 from Caddy and never reaches the container: /api/prove, /api/verify*, /api/session/*, /api/agent/*, /api/search and the rest. - echidna.container: drop AutoUpdate=registry and set Pull=never, so the host keeps running the image it already has. This freezes the image; it does not verify it. - README.adoc and docs/HOSTING.adoc: a host runbook (disable the auto-update timer, record the running digest, restart, probe), and the exit condition: the stopgap ends in the change that lands bearer auth and re-pins to the signed image by digest. Tested locally: - caddy 2.6.2 validates a copy with the rate_limit plugin directive stripped. - Behind it, a stub backend refuses 15 execution and path-trick requests and forwards the 2 allowed routes. - podman 4.9.3 quadlet -dryrun emits --pull never and no auto-update label. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- deploy/hetzner/Caddyfile | 28 +++++++++++++++++++---- deploy/hetzner/README.adoc | 39 ++++++++++++++++++++++++++++++++ deploy/hetzner/echidna.container | 12 ++++++---- docs/HOSTING.adoc | 10 +++++--- 4 files changed, 76 insertions(+), 13 deletions(-) diff --git a/deploy/hetzner/Caddyfile b/deploy/hetzner/Caddyfile index 00a8ad92..af372bc5 100644 --- a/deploy/hetzner/Caddyfile +++ b/deploy/hetzner/Caddyfile @@ -34,11 +34,29 @@ api.nesy-prover.dev { -Server } - # `echidna` resolves on the shared podman network (echidna.network); - # the API container publishes no host port. - reverse_proxy echidna:8081 { - transport http { - response_header_timeout 120s + # CONTAINMENT STOPGAP (owner ruling 2026-11-05). The API has no + # authentication yet and its execution routes spawn prover binaries + # on caller input. Until bearer auth lands on every execution route, + # only these two read-only GET routes are forwarded. Everything else, + # including /api/prove, /api/verify*, /api/session/* and + # /api/agent/*, is refused here and never reaches the container. + # Remove this matcher only in the change that enables auth. + @public { + method GET HEAD + path /api/health /api/provers + } + + handle @public { + # `echidna` resolves on the shared podman network (echidna.network); + # the API container publishes no host port. + reverse_proxy echidna:8081 { + transport http { + response_header_timeout 120s + } } } + + handle { + respond "Prover execution is disabled on this host until authentication is enabled." 403 + } } diff --git a/deploy/hetzner/README.adoc b/deploy/hetzner/README.adoc index 35d99015..02c6cafb 100644 --- a/deploy/hetzner/README.adoc +++ b/deploy/hetzner/README.adoc @@ -30,6 +30,41 @@ Let's Encrypt), orchestrated with podman systemd quadlets. If abuse appears, add a bearer-token matcher in the Caddyfile for POST routes. A server-side per-request prover timeout is tracked as a follow-up issue in the main repo. + *Superseded 2026-11-05*: see <>. + +[[containment-stopgap]] +== Containment stopgap (owner ruling 2026-11-05) + +Until bearer authentication lands on every execution route, this host +serves read-only routes only, and it no longer rolls out new images by +itself. + +* The `Caddyfile` forwards only `GET`/`HEAD` on `/api/health` and + `/api/provers`. Every other request is answered `403` by Caddy and + never reaches the container. That includes `/api/prove`, + `/api/verify*`, `/api/session/*`, `/api/agent/*` and `/api/search`. +* `echidna.container` drops `AutoUpdate=registry` and sets `Pull=never`. + The unit runs the image already on the host, so a newly published + `:latest` is not deployed. This *freezes* the running image. It does + not verify it. + +Apply on the host as the `deploy` user. Record the running digest +first, so the freeze is auditable: + +[source,console] +---- +systemctl --user disable --now podman-auto-update.timer +podman image inspect --format '{{.Digest}}' ghcr.io/hyperpolymath/echidna:latest # record this +# copy the updated Caddyfile and echidna.container into place, then: +systemctl --user daemon-reload +systemctl --user restart echidna caddy +curl -s -o /dev/null -w '%{http_code}\n' https://api.nesy-prover.dev/api/health # expect 200 +curl -s -o /dev/null -w '%{http_code}\n' -X POST https://api.nesy-prover.dev/api/verify # expect 403 +---- + +The stopgap ends in the change that enables authentication. That change +re-pins `Image=` to the signed image by digest and removes the `@public` +matcher. Do not re-enable `podman-auto-update.timer` before then. == 0. Preflight (read-only, do first) @@ -195,6 +230,10 @@ podman ps && curl -s https://api.nesy-prover.dev/api/health == 5. Updates and rollback +NOTE: Unattended rollout is *disabled* while the +<> is in force. The commands below describe the +mechanism for when it is restored with a signed, digest-pinned image. + `ghcr-publish.yml` pushes a new `:latest` on every GitHub release. Enable unattended rollout: diff --git a/deploy/hetzner/echidna.container b/deploy/hetzner/echidna.container index 51e3e552..8dec43cd 100644 --- a/deploy/hetzner/echidna.container +++ b/deploy/hetzner/echidna.container @@ -8,17 +8,19 @@ # over echidna-net), memory/pids limits, tmpfs /tmp, no privilege # escalation. Healthcheck uses the binary — the image ships no curl. # -# Image tag :latest is intentional together with AutoUpdate=registry + -# podman-auto-update.timer: new releases roll out automatically and a -# failing healthcheck rolls back. For pinned mode, set Image= to a -# :vX.Y.Z tag or digest and bump via PR (see README.adoc). +# CONTAINMENT STOPGAP (owner ruling 2026-11-05): automatic rollout is OFF. +# AutoUpdate=registry is removed and Pull=never makes the unit run the +# image already on the host, so a newly published :latest is never pulled. +# This freezes the running image; it does not verify it. Re-pin to the +# signed image by digest in the change that lands authentication +# (see README.adoc, "Containment stopgap"). [Unit] Description=ECHIDNA theorem-prover API [Container] Image=ghcr.io/hyperpolymath/echidna:latest -AutoUpdate=registry +Pull=never ContainerName=echidna Network=echidna.network Exec=server --port 8081 --host 0.0.0.0 --cors diff --git a/docs/HOSTING.adoc b/docs/HOSTING.adoc index aa7118bc..30753ee6 100644 --- a/docs/HOSTING.adoc +++ b/docs/HOSTING.adoc @@ -84,9 +84,13 @@ through Caddy a *1 MB request body cap* * the container is capped at `+--memory=1500m --pids-limit=512+`, with a tmpfs `+/tmp+` and `+NoNewPrivileges+` -* `+AutoUpdate=registry+` plus `+HealthOnFailure=kill+` means a new -release rolls out unattended and an unhealthy container *fails the -unit*, which is what makes rollback actually fire +* `+HealthOnFailure=kill+` means an unhealthy container *fails the +unit*, so systemd restarts it +* *Containment stopgap (2026-11-05):* Caddy forwards only `GET`/`HEAD` +on `+/api/health+` and `+/api/provers+`, and refuses every execution +route with `403`. `+AutoUpdate=registry+` is off, and `+Pull=never+` +freezes the running image until authentication lands. See +link:../deploy/hetzner/README.adoc#containment-stopgap[the runbook]. ==== Why the caging matters From b3af878430a3c031ac268debddc4754345507306 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 07:29:35 +0000 Subject: [PATCH 2/4] fix(deploy): keep the rate limit on the stopgap routes; harden the runbook MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CodeRabbit review of #461. - Caddyfile: the site-level rate_limit (ordered `before reverse_proxy`) sorted after the new terminal `handle` blocks, so it never ran. The limiter and both handlers now sit in one `route` block, which keeps the written order, with the limiter first. Reproduced with a stand-in directive ordered the same way: with the old layout it was absent on proxied requests, and with the route block it is present. Every refusal still holds. - README runbook: - detect a quadlet or appendix install before changing anything, and give the appendix host its own step (only the proxy changes there); - record the running container's image ID, not the tag's digest, and re-point :latest at it if they differ, so Pull=never restarts the image that was running; - verify the same image afterwards. - §5 note: the auto-update commands apply only to a tag-based Image= with AutoUpdate=registry. A digest pin changes only by PR. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- deploy/hetzner/Caddyfile | 38 +++++++++++++---------- deploy/hetzner/README.adoc | 62 ++++++++++++++++++++++++++++++++++---- 2 files changed, 78 insertions(+), 22 deletions(-) diff --git a/deploy/hetzner/Caddyfile b/deploy/hetzner/Caddyfile index af372bc5..096acfa4 100644 --- a/deploy/hetzner/Caddyfile +++ b/deploy/hetzner/Caddyfile @@ -18,13 +18,6 @@ api.nesy-prover.dev { request_body { max_size 1MB } - rate_limit { - zone api { - key {remote_host} - events 30 - window 1m - } - } header { Strict-Transport-Security "max-age=31536000" @@ -46,17 +39,30 @@ api.nesy-prover.dev { path /api/health /api/provers } - handle @public { - # `echidna` resolves on the shared podman network (echidna.network); - # the API container publishes no host port. - reverse_proxy echidna:8081 { - transport http { - response_header_timeout 120s + # `route` keeps the written order. The rate limiter must run first: at + # site level Caddy would sort it after the terminal `handle` blocks + # below, and it would then never run. + route { + rate_limit { + zone api { + key {remote_host} + events 30 + window 1m } } - } - handle { - respond "Prover execution is disabled on this host until authentication is enabled." 403 + handle @public { + # `echidna` resolves on the shared podman network (echidna.network); + # the API container publishes no host port. + reverse_proxy echidna:8081 { + transport http { + response_header_timeout 120s + } + } + } + + handle { + respond "Prover execution is disabled on this host until authentication is enabled." 403 + } } } diff --git a/deploy/hetzner/README.adoc b/deploy/hetzner/README.adoc index 02c6cafb..43b7d225 100644 --- a/deploy/hetzner/README.adoc +++ b/deploy/hetzner/README.adoc @@ -48,20 +48,67 @@ itself. `:latest` is not deployed. This *freezes* the running image. It does not verify it. -Apply on the host as the `deploy` user. Record the running digest -first, so the freeze is auditable: +Apply on the host as the `deploy` user. + +*1. Find out which install this host has.* These steps are for a host +installed with the quadlets in §2 (units `echidna.service` and +`caddy.service`). A host installed from the appendix runs +`container-echidna` and `container-caddy` instead. For that kind of host, +use step 4 instead of step 3. + +[source,console] +---- +systemctl --user cat echidna.service caddy.service >/dev/null && echo quadlet +systemctl --user cat container-echidna.service container-caddy.service >/dev/null && echo appendix +---- + +*2. Record the image the container is running.* Record the running +container's image ID, not the tag's digest. If an auto-update or a manual +pull has moved the local `:latest` tag since the container started, a +restart with `Pull=never` would start the image the tag now points to. [source,console] ---- systemctl --user disable --now podman-auto-update.timer -podman image inspect --format '{{.Digest}}' ghcr.io/hyperpolymath/echidna:latest # record this -# copy the updated Caddyfile and echidna.container into place, then: +RUNNING=$(podman container inspect echidna --format '{{.Image}}') # record this +TAGGED=$(podman image inspect --format '{{.Id}}' ghcr.io/hyperpolymath/echidna:latest) +echo "running=$RUNNING tagged=$TAGGED" +# If they differ, point :latest back at the running image before restarting: +[ "$RUNNING" = "$TAGGED" ] || podman tag "$RUNNING" ghcr.io/hyperpolymath/echidna:latest +---- + +*3. Quadlet host.* Copy the updated `Caddyfile` and `echidna.container` +into place, then: + +[source,console] +---- systemctl --user daemon-reload systemctl --user restart echidna caddy +---- + +*4. Appendix host.* Those containers carry no auto-update label, and +`podman generate systemd --new` units do not pull an image that is +already present. So only the proxy changes. Copy the updated +`Caddyfile` to `/opt/echidna/Caddyfile`, then: + +[source,console] +---- +systemctl --user restart container-caddy +---- + +*5. Verify, on either kind of host.* The container must still run the +image recorded in step 2. + +[source,console] +---- +[ "$(podman container inspect echidna --format '{{.Image}}')" = "$RUNNING" ] && echo same-image curl -s -o /dev/null -w '%{http_code}\n' https://api.nesy-prover.dev/api/health # expect 200 curl -s -o /dev/null -w '%{http_code}\n' -X POST https://api.nesy-prover.dev/api/verify # expect 403 ---- +Stop and reassess if step 1 prints neither `quadlet` nor `appendix`, or if +step 5 does not print `same-image`, `200` and `403`. + The stopgap ends in the change that enables authentication. That change re-pins `Image=` to the signed image by digest and removes the `@public` matcher. Do not re-enable `podman-auto-update.timer` before then. @@ -231,8 +278,11 @@ podman ps && curl -s https://api.nesy-prover.dev/api/health == 5. Updates and rollback NOTE: Unattended rollout is *disabled* while the -<> is in force. The commands below describe the -mechanism for when it is restored with a signed, digest-pinned image. +<> is in force. The commands below apply only to a +tag-based `Image=` with `AutoUpdate=registry`, because `podman +auto-update` acts only on containers that carry that label. A +digest-pinned image, which is what the change ending the stopgap +introduces, changes only through a PR that bumps the digest. `ghcr-publish.yml` pushes a new `:latest` on every GitHub release. Enable unattended rollout: From cdca71c08a876f98ef7045c34abfe161e8214200 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 5 Nov 2026 17:48:46 +0000 Subject: [PATCH 3/4] Update deploy/hetzner/README.adoc Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- deploy/hetzner/README.adoc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/deploy/hetzner/README.adoc b/deploy/hetzner/README.adoc index 43b7d225..cbe0b79e 100644 --- a/deploy/hetzner/README.adoc +++ b/deploy/hetzner/README.adoc @@ -70,11 +70,11 @@ restart with `Pull=never` would start the image the tag now points to. [source,console] ---- systemctl --user disable --now podman-auto-update.timer -RUNNING=$(podman container inspect echidna --format '{{.Image}}') # record this -TAGGED=$(podman image inspect --format '{{.Id}}' ghcr.io/hyperpolymath/echidna:latest) +RUNNING=$(podman container inspect echidna --format '{{.Image}}') || exit 1 +TAGGED=$(podman image inspect --format '{{.Id}}' ghcr.io/hyperpolymath/echidna:latest) || exit 1 echo "running=$RUNNING tagged=$TAGGED" # If they differ, point :latest back at the running image before restarting: -[ "$RUNNING" = "$TAGGED" ] || podman tag "$RUNNING" ghcr.io/hyperpolymath/echidna:latest +[ "$RUNNING" = "$TAGGED" ] || podman tag "$RUNNING" ghcr.io/hyperpolymath/echidna:latest || exit 1 ---- *3. Quadlet host.* Copy the updated `Caddyfile` and `echidna.container` From 55877bd6582671bb0c0dc6da71e0afb55fc47e91 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 5 Nov 2026 17:49:17 +0000 Subject: [PATCH 4/4] Update deploy/hetzner/README.adoc Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- deploy/hetzner/README.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deploy/hetzner/README.adoc b/deploy/hetzner/README.adoc index cbe0b79e..b1e93402 100644 --- a/deploy/hetzner/README.adoc +++ b/deploy/hetzner/README.adoc @@ -106,7 +106,7 @@ curl -s -o /dev/null -w '%{http_code}\n' https://api.nesy-prover.dev/api/health curl -s -o /dev/null -w '%{http_code}\n' -X POST https://api.nesy-prover.dev/api/verify # expect 403 ---- -Stop and reassess if step 1 prints neither `quadlet` nor `appendix`, or if +Stop and reassess if step 1 does not print exactly one of `quadlet` or `appendix`, or if step 5 does not print `same-image`, `200` and `403`. The stopgap ends in the change that enables authentication. That change