From b2b2a148256b9f92a3166cf9a5c86477b19cf63c Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 15:42:50 +0100 Subject: [PATCH 1/2] feat(deploy): Hetzner deploy unit for api.nesy-prover.dev Complete single-box deployment for the public API: rootless podman systemd quadlets (echidna API + Caddy TLS proxy), a Caddy image built on-host with mholt/caddy-ratelimit, and an operator runbook. The API is unauthenticated and spawns prover binaries on user input, so it is caged: no published host port (Caddy-only reachability over the quadlet network), 30 req/min/IP rate limit, 1 MB body cap, memory/pids limits, tmpfs /tmp, NoNewPrivileges. Updates roll out via podman-auto-update with healthcheck-gated rollback. Verified locally: quadlet -dryrun generates all three units with zero warnings and correct dependency ordering; the Caddy image builds with podman and 'caddy validate' accepts the Caddyfile with http.handlers.rate_limit present. Co-Authored-By: Claude Fable 5 --- deploy/hetzner/Caddyfile | 44 +++++++ deploy/hetzner/Containerfile.caddy | 15 +++ deploy/hetzner/README.adoc | 181 +++++++++++++++++++++++++++++ deploy/hetzner/caddy.container | 31 +++++ deploy/hetzner/echidna.container | 37 ++++++ deploy/hetzner/echidna.network | 9 ++ deploy/hetzner/env.example | 18 +++ 7 files changed, 335 insertions(+) create mode 100644 deploy/hetzner/Caddyfile create mode 100644 deploy/hetzner/Containerfile.caddy create mode 100644 deploy/hetzner/README.adoc create mode 100644 deploy/hetzner/caddy.container create mode 100644 deploy/hetzner/echidna.container create mode 100644 deploy/hetzner/echidna.network create mode 100644 deploy/hetzner/env.example diff --git a/deploy/hetzner/Caddyfile b/deploy/hetzner/Caddyfile new file mode 100644 index 0000000..00a8ad9 --- /dev/null +++ b/deploy/hetzner/Caddyfile @@ -0,0 +1,44 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# TLS-terminating reverse proxy for the public ECHIDNA API. +# Runs in the localhost/caddy-rl:2 image (see Containerfile.caddy); +# the rate_limit directive is provided by mholt/caddy-ratelimit. + +{ + email j.d.a.jewell@open.ac.uk + order rate_limit before reverse_proxy +} + +api.nesy-prover.dev { + encode zstd gzip + + # The API executes prover input; cap request size and per-client + # rate before anything reaches it. + request_body { + max_size 1MB + } + rate_limit { + zone api { + key {remote_host} + events 30 + window 1m + } + } + + header { + Strict-Transport-Security "max-age=31536000" + X-Content-Type-Options nosniff + X-Frame-Options DENY + Referrer-Policy no-referrer + -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 + } + } +} diff --git a/deploy/hetzner/Containerfile.caddy b/deploy/hetzner/Containerfile.caddy new file mode 100644 index 0000000..abe12ac --- /dev/null +++ b/deploy/hetzner/Containerfile.caddy @@ -0,0 +1,15 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Caddy with the mholt/caddy-ratelimit plugin (stock Caddy has no rate +# limiting). Built on the target host with podman — never published: +# +# podman build -f Containerfile.caddy -t localhost/caddy-rl:2 . +# +# RSR-H15: podman + Containerfile, not Docker. + +FROM docker.io/library/caddy:2-builder AS builder +RUN xcaddy build --with github.com/mholt/caddy-ratelimit + +FROM docker.io/library/caddy:2 +COPY --from=builder /usr/bin/caddy /usr/bin/caddy diff --git a/deploy/hetzner/README.adoc b/deploy/hetzner/README.adoc new file mode 100644 index 0000000..63ee490 --- /dev/null +++ b/deploy/hetzner/README.adoc @@ -0,0 +1,181 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Deploying the ECHIDNA API to Hetzner (api.nesy-prover.dev) +:toc: +:toclevels: 2 + +This directory is the complete deploy unit for running the public +ECHIDNA API on a single Hetzner server behind Caddy (auto-TLS via +Let's Encrypt), orchestrated with podman systemd quadlets. + +.What runs where +[cols="1,3"] +|=== +| `echidna` | `ghcr.io/hyperpolymath/echidna:latest`, `server --port 8081 --host 0.0.0.0 --cors`. No published host port — reachable only from Caddy over the `echidna-net` podman network. +| `caddy` | `localhost/caddy-rl:2` (built on-box from `Containerfile.caddy`), ports 80/443, terminates TLS for `api.nesy-prover.dev`, rate-limits (30 req/min/IP), caps request bodies at 1 MB. +|=== + +== Decision record + +* *Quadlets over podman-compose*: systemd-native restart-on-boot with no + extra daemon, unit-level dependency ordering, and first-class + `AutoUpdate=registry` integration with `podman-auto-update.timer` + (which rolls back automatically when the updated container fails its + healthcheck). Requires podman >= 4.4. +* *Rootless*: the API executes user-supplied prover input; run both + units as an unprivileged `deploy` user with linger. +* *Caddy over svalinn*: the estate's svalinn/vordr stack is not yet + CI-proven; Caddy is the low-risk choice for a public endpoint. The + `container/compose.toml` selur stack remains for local development. +* *No API auth at launch*: the service is deliberately public but caged + (rate limit, body cap, memory/pids limits, tmpfs, unpublished port). + 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. + +== 0. Preflight (read-only, do first) + + ssh @ 'cat /etc/os-release; free -h; df -h /; nproc; ss -tlnp; podman --version' + +Gates — stop and reassess if any fail: + +* Ports 80/443 unbound (`ss -tlnp` shows no listener). If something + else owns them, this plan does not apply as-is. +* >= 2 GB RAM free for the `:latest` image (Z3 + Lean). The `:full` + image (Isabelle/Agda/Julia) needs >= 4 GB and is not deployed here. +* podman >= 4.4 for quadlets. Debian 12 ships 4.3.1 — either install a + newer podman or fall back to `podman generate systemd --new --files` + (same containers, generated units instead of quadlets). +* Image pullable anonymously: ++ + podman manifest inspect ghcr.io/hyperpolymath/echidna:latest ++ +On 401: make the GHCR package public (GitHub → Packages → echidna → +Package settings → visibility) or use a read-only PAT with +`podman login ghcr.io` as the deploy user. + +== 1. Server preparation (as root) + + apt update && apt upgrade -y + apt install -y podman unattended-upgrades + dpkg-reconfigure -f noninteractive unattended-upgrades + + # Firewall: SSH + HTTP(S) only + apt install -y ufw + ufw default deny incoming + ufw allow 22/tcp && ufw allow 80/tcp && ufw allow 443/tcp + ufw enable + + # Unprivileged deploy user with lingering services + useradd -m -s /bin/bash deploy + loginctl enable-linger deploy + + # Let rootless podman bind 80/443 + echo 'net.ipv4.ip_unprivileged_port_start=80' > /etc/sysctl.d/50-unprivileged-ports.conf + sysctl --system + +== 2. Install the deploy unit (as deploy) + +From your workstation, from this directory: + + scp Caddyfile Containerfile.caddy deploy@:/opt/echidna/ + scp echidna.network echidna.container caddy.container \ + deploy@:~/.config/containers/systemd/ + +(Create the target dirs first: `sudo mkdir -p /opt/echidna && sudo chown deploy /opt/echidna` +and `mkdir -p ~/.config/containers/systemd` as deploy.) + +On the server, as deploy: + + cd /opt/echidna + podman build -f Containerfile.caddy -t localhost/caddy-rl:2 . + podman pull ghcr.io/hyperpolymath/echidna:latest + podman image inspect --format '{{.Digest}}' ghcr.io/hyperpolymath/echidna:latest + # ^ record this digest in env.example / your notes for rollback + + systemctl --user daemon-reload + systemctl --user list-unit-files | grep -E 'echidna|caddy' + +== 3. DNS (before starting Caddy) + +Create in the Cloudflare zone for nesy-prover.dev: + + A api proxied=false (grey cloud), TTL 300 + +Grey cloud is required at launch so Caddy's Let's Encrypt HTTP-01 +challenge reaches the server directly. (Optional later hardening: +orange-cloud + a Cloudflare Origin CA cert in the Caddyfile.) + +Wait until `dig +short api.nesy-prover.dev @1.1.1.1` returns the +server IP before the first Caddy start — ACME then succeeds first try. + +== 4. Bring-up and verification + + systemctl --user start echidna caddy + podman ps # both Up, echidna (healthy) + journalctl --user -u caddy -f # watch certificate issuance + +End-to-end, from anywhere: + + curl -s https://api.nesy-prover.dev/api/health # {"status":"ok",...} + curl -s https://api.nesy-prover.dev/api/provers | head + curl -s -X POST https://api.nesy-prover.dev/api/verify \ + -H 'content-type: application/json' \ + -d '{"prover":"Z3","content":"(assert (forall ((x Int)) (= (+ x 0) x)))(check-sat)"}' + +Controls: + + # Rate limit: burst 40 requests, expect HTTP 429 after ~30 + for i in $(seq 1 40); do curl -s -o /dev/null -w '%{http_code} ' \ + https://api.nesy-prover.dev/api/health; done; echo + # Headers: HSTS present, Server header absent + curl -sI https://api.nesy-prover.dev/api/health + # Isolation: direct API port must be unreachable from outside + curl -m 5 http://:8081/api/health || echo "unreachable (correct)" + +Reboot survival (validates linger + [Install] + Restart in one shot): + + sudo reboot + # after it returns: + podman ps && curl -s https://api.nesy-prover.dev/api/health + +== 5. Updates and rollback + +Enable unattended rollout of new releases (ghcr-publish.yml pushes +`:latest` on every GitHub release): + + systemctl --user enable --now podman-auto-update.timer + podman auto-update --dry-run # see what would change + podman auto-update # roll out immediately + +`podman-auto-update` restarts the unit on a new image and rolls back +automatically if the fresh container fails its healthcheck. + +Manual rollback to a recorded digest: + + podman pull ghcr.io/hyperpolymath/echidna@ + podman tag ghcr.io/hyperpolymath/echidna@ ghcr.io/hyperpolymath/echidna:latest + systemctl --user restart echidna + +Pinned mode (opt out of auto-update): set `Image=` in +`echidna.container` to a `:vX.Y.Z` tag or digest, remove +`AutoUpdate=registry`, and bump via PR. + +== Appendix: Debian 12 fallback (podman 4.3, no quadlets) + + podman network create echidna-net + podman create --name echidna --network echidna-net \ + --memory=1500m --pids-limit=512 --tmpfs /tmp:rw,size=256m \ + --security-opt no-new-privileges \ + --health-cmd '/app/bin/echidna --version' --health-interval 30s \ + ghcr.io/hyperpolymath/echidna:latest server --port 8081 --host 0.0.0.0 --cors + podman create --name caddy --network echidna-net \ + -p 80:80 -p 443:443 \ + -v /opt/echidna/Caddyfile:/etc/caddy/Caddyfile:ro \ + -v caddy-data:/data -v caddy-config:/config \ + localhost/caddy-rl:2 + podman generate systemd --new --files --name echidna + podman generate systemd --new --files --name caddy + mkdir -p ~/.config/systemd/user && mv container-*.service ~/.config/systemd/user/ + systemctl --user daemon-reload + systemctl --user enable --now container-echidna container-caddy diff --git a/deploy/hetzner/caddy.container b/deploy/hetzner/caddy.container new file mode 100644 index 0000000..8dc3d62 --- /dev/null +++ b/deploy/hetzner/caddy.container @@ -0,0 +1,31 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Quadlet unit for the Caddy TLS proxy fronting api.nesy-prover.dev. +# +# Build the image on the host first: +# podman build -f Containerfile.caddy -t localhost/caddy-rl:2 . +# The caddy-data volume persists the ACME account and certificates — +# do not delete it casually (Let's Encrypt rate limits). + +[Unit] +Description=Caddy TLS proxy for api.nesy-prover.dev +Wants=echidna.service +After=echidna.service + +[Container] +Image=localhost/caddy-rl:2 +ContainerName=caddy +Network=echidna.network +PublishPort=80:80 +PublishPort=443:443 +Volume=/opt/echidna/Caddyfile:/etc/caddy/Caddyfile:ro +Volume=caddy-data:/data +Volume=caddy-config:/config + +[Service] +Restart=always +RestartSec=5 + +[Install] +WantedBy=default.target diff --git a/deploy/hetzner/echidna.container b/deploy/hetzner/echidna.container new file mode 100644 index 0000000..09569d3 --- /dev/null +++ b/deploy/hetzner/echidna.container @@ -0,0 +1,37 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Quadlet unit for the ECHIDNA API server. +# +# The API has no authentication and spawns prover binaries on user +# input, so it is caged: no published host port (only Caddy reaches it +# 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). + +[Unit] +Description=ECHIDNA theorem-prover API + +[Container] +Image=ghcr.io/hyperpolymath/echidna:latest +AutoUpdate=registry +ContainerName=echidna +Network=echidna.network +Exec=server --port 8081 --host 0.0.0.0 --cors +Environment=RUST_LOG=info +HealthCmd=/app/bin/echidna --version +HealthInterval=30s +Tmpfs=/tmp:rw,size=256m +NoNewPrivileges=true +PodmanArgs=--memory=1500m --pids-limit=512 + +[Service] +Restart=always +RestartSec=5 + +[Install] +WantedBy=default.target diff --git a/deploy/hetzner/echidna.network b/deploy/hetzner/echidna.network new file mode 100644 index 0000000..5f89d80 --- /dev/null +++ b/deploy/hetzner/echidna.network @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Shared podman network for the API + proxy pair. Referenced by name +# (echidna.network) from both .container units so systemd orders +# creation correctly. + +[Network] +NetworkName=echidna-net diff --git a/deploy/hetzner/env.example b/deploy/hetzner/env.example new file mode 100644 index 0000000..c52415d --- /dev/null +++ b/deploy/hetzner/env.example @@ -0,0 +1,18 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Values that vary per deployment. Nothing here is secret by design — +# the API takes no credentials; Cloudflare tokens are used from the +# operator's workstation, never stored on the server. + +# Public IPv4 of the Hetzner server (target of the api A record). +SERVER_IP= + +# Image reference actually deployed. :latest is the auto-update mode; +# record the digest at deploy time for rollback: +# podman image inspect --format '{{.Digest}}' ghcr.io/hyperpolymath/echidna:latest +ECHIDNA_IMAGE=ghcr.io/hyperpolymath/echidna:latest +ECHIDNA_IMAGE_DIGEST= + +# ACME/Let's Encrypt contact (also set in the Caddyfile global block). +ACME_EMAIL=j.d.a.jewell@open.ac.uk From 8b418b5817ed9c7991041527730d314cdafed3f2 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 16:27:19 +0100 Subject: [PATCH 2/2] fix(deploy): correct runbook ordering, rollback safety, and version gating MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adversarial review of this deploy unit found operator-facing defects: - Section 2 ran scp before the target directories existed, so a verbatim run failed on the first copy. Create /opt/echidna (root section) and ~/.config/containers/systemd (deploy user) first. - The auto-update rollback claim was not true as configured: an unhealthy-but-running container satisfies systemd, so nothing would have failed and nothing would have rolled back. Add HealthOnFailure=kill to echidna.container — an unhealthy container now fails the unit, which is what makes both Restart=always and auto-update's rollback fire — and describe the mechanism honestly. - The manual rollback procedure was silently undone by the next podman-auto-update.timer run, which re-pulls registry :latest. Stop the timer first, and document pinned mode as the durable exit. - The podman >= 4.4 floor was a guess that several keys in these units (HealthOnFailure= in particular) would not satisfy. Replace the guess with a measurement: the preflight now runs the quadlet generator in dry-run mode on the target host, which proves every key is understood regardless of version. - Clarify that the 1500m container cap sits deliberately below the 2 GB host requirement to leave headroom, and note that the plaintext isolation probe is asserting a closed port on purpose. Convert the indentation-based literal blocks to delimited source blocks so the runbook renders predictably. Verified: asciidoctor renders with no warnings; quadlet -dryrun generates all three units cleanly with --health-on-failure kill in the resulting ExecStart. Co-Authored-By: Claude Fable 5 --- deno.lock | 11 +- deploy/hetzner/README.adoc | 267 ++++++++++++++++++++----------- deploy/hetzner/echidna.container | 4 + 3 files changed, 183 insertions(+), 99 deletions(-) diff --git a/deno.lock b/deno.lock index ccc0e2c..77b75db 100644 --- a/deno.lock +++ b/deno.lock @@ -1,4 +1,11 @@ { - "version": "4", - "remote": {} + "version": "5", + "specifiers": { + "jsr:@std/yaml@*": "1.1.2" + }, + "jsr": { + "@std/yaml@1.1.2": { + "integrity": "de612653c036749ba2044165e316f52412b0f0698afffb7ee80b5331d6d2abae" + } + } } diff --git a/deploy/hetzner/README.adoc b/deploy/hetzner/README.adoc index 63ee490..0609433 100644 --- a/deploy/hetzner/README.adoc +++ b/deploy/hetzner/README.adoc @@ -19,9 +19,7 @@ Let's Encrypt), orchestrated with podman systemd quadlets. * *Quadlets over podman-compose*: systemd-native restart-on-boot with no extra daemon, unit-level dependency ordering, and first-class - `AutoUpdate=registry` integration with `podman-auto-update.timer` - (which rolls back automatically when the updated container fails its - healthcheck). Requires podman >= 4.4. + `AutoUpdate=registry` integration with `podman-auto-update.timer`. * *Rootless*: the API executes user-supplied prover input; run both units as an unprivileged `deploy` user with linger. * *Caddy over svalinn*: the estate's svalinn/vordr stack is not yet @@ -35,20 +33,41 @@ Let's Encrypt), orchestrated with podman systemd quadlets. == 0. Preflight (read-only, do first) - ssh @ 'cat /etc/os-release; free -h; df -h /; nproc; ss -tlnp; podman --version' +[source,console] +---- +ssh @ 'cat /etc/os-release; free -h; df -h /; nproc; ss -tlnp; podman --version' +---- Gates — stop and reassess if any fail: * Ports 80/443 unbound (`ss -tlnp` shows no listener). If something else owns them, this plan does not apply as-is. -* >= 2 GB RAM free for the `:latest` image (Z3 + Lean). The `:full` - image (Isabelle/Agda/Julia) needs >= 4 GB and is not deployed here. -* podman >= 4.4 for quadlets. Debian 12 ships 4.3.1 — either install a - newer podman or fall back to `podman generate systemd --new --files` - (same containers, generated units instead of quadlets). +* At least 2 GB RAM. The API container is capped at 1500 MB + (`PodmanArgs=--memory=1500m`), deliberately below the host total so + Caddy and the OS keep headroom; raise both together if you want more. + The `:full` image (Isabelle/Agda/Julia) needs >= 4 GB and is not + deployed here. +* *Quadlet keys are all understood by the installed podman.* Do not + trust a version number for this — measure it. Copy the three unit + files to the server and run the generator in dry-run mode: ++ +[source,console] +---- +scp echidna.network echidna.container caddy.container @:/tmp/qcheck/ +ssh @ 'QUADLET_UNIT_DIRS=/tmp/qcheck /usr/libexec/podman/quadlet -dryrun' +---- ++ +It must print generated `[Service]` sections for all three units with +no warnings. These units were authored and dry-run verified against podman +5.4; podman 5.x is recommended and 4.x is likely to reject at least +one key (`HealthOnFailure=` in particular). If the dry-run complains, +use the Debian-12 fallback in the appendix instead. * Image pullable anonymously: + - podman manifest inspect ghcr.io/hyperpolymath/echidna:latest +[source,console] +---- +podman manifest inspect ghcr.io/hyperpolymath/echidna:latest +---- + On 401: make the GHCR package public (GitHub → Packages → echidna → Package settings → visibility) or use a read-only PAT with @@ -56,51 +75,70 @@ Package settings → visibility) or use a read-only PAT with == 1. Server preparation (as root) - apt update && apt upgrade -y - apt install -y podman unattended-upgrades - dpkg-reconfigure -f noninteractive unattended-upgrades +[source,console] +---- +apt update && apt upgrade -y +apt install -y podman unattended-upgrades ufw +dpkg-reconfigure -f noninteractive unattended-upgrades + +# Firewall: SSH + HTTP(S) only +ufw default deny incoming +ufw allow 22/tcp && ufw allow 80/tcp && ufw allow 443/tcp +ufw enable - # Firewall: SSH + HTTP(S) only - apt install -y ufw - ufw default deny incoming - ufw allow 22/tcp && ufw allow 80/tcp && ufw allow 443/tcp - ufw enable +# Unprivileged deploy user with lingering services +useradd -m -s /bin/bash deploy +loginctl enable-linger deploy - # Unprivileged deploy user with lingering services - useradd -m -s /bin/bash deploy - loginctl enable-linger deploy +# Let rootless podman bind 80/443 +echo 'net.ipv4.ip_unprivileged_port_start=80' > /etc/sysctl.d/50-unprivileged-ports.conf +sysctl --system - # Let rootless podman bind 80/443 - echo 'net.ipv4.ip_unprivileged_port_start=80' > /etc/sysctl.d/50-unprivileged-ports.conf - sysctl --system +# Destination for the Caddyfile and the Caddy build context +mkdir -p /opt/echidna && chown deploy:deploy /opt/echidna +---- -== 2. Install the deploy unit (as deploy) +== 2. Install the deploy unit -From your workstation, from this directory: +Create the quadlet directory *before* copying anything into it — as +the deploy user on the server: - scp Caddyfile Containerfile.caddy deploy@:/opt/echidna/ - scp echidna.network echidna.container caddy.container \ - deploy@:~/.config/containers/systemd/ +[source,console] +---- +mkdir -p ~/.config/containers/systemd +---- -(Create the target dirs first: `sudo mkdir -p /opt/echidna && sudo chown deploy /opt/echidna` -and `mkdir -p ~/.config/containers/systemd` as deploy.) +Then, from your workstation in this directory: -On the server, as deploy: +[source,console] +---- +scp Caddyfile Containerfile.caddy deploy@:/opt/echidna/ +scp echidna.network echidna.container caddy.container \ + deploy@:~/.config/containers/systemd/ +---- - cd /opt/echidna - podman build -f Containerfile.caddy -t localhost/caddy-rl:2 . - podman pull ghcr.io/hyperpolymath/echidna:latest - podman image inspect --format '{{.Digest}}' ghcr.io/hyperpolymath/echidna:latest - # ^ record this digest in env.example / your notes for rollback +Back on the server, as deploy: - systemctl --user daemon-reload - systemctl --user list-unit-files | grep -E 'echidna|caddy' +[source,console] +---- +cd /opt/echidna +podman build -f Containerfile.caddy -t localhost/caddy-rl:2 . +podman pull ghcr.io/hyperpolymath/echidna:latest +podman image inspect --format '{{.Digest}}' ghcr.io/hyperpolymath/echidna:latest +# ^ record this digest in env.example / your notes for rollback + +systemctl --user daemon-reload +systemctl --user list-unit-files | grep -E 'echidna|caddy' +---- == 3. DNS (before starting Caddy) Create in the Cloudflare zone for nesy-prover.dev: - A api proxied=false (grey cloud), TTL 300 +[source] +---- +A api proxied=false (grey cloud), TTL 300 +---- Grey cloud is required at launch so Caddy's Let's Encrypt HTTP-01 challenge reaches the server directly. (Optional later hardening: @@ -111,71 +149,106 @@ server IP before the first Caddy start — ACME then succeeds first try. == 4. Bring-up and verification - systemctl --user start echidna caddy - podman ps # both Up, echidna (healthy) - journalctl --user -u caddy -f # watch certificate issuance +[source,console] +---- +systemctl --user start echidna caddy +podman ps # both Up, echidna (healthy) +journalctl --user -u caddy -f # watch certificate issuance +---- End-to-end, from anywhere: - curl -s https://api.nesy-prover.dev/api/health # {"status":"ok",...} - curl -s https://api.nesy-prover.dev/api/provers | head - curl -s -X POST https://api.nesy-prover.dev/api/verify \ - -H 'content-type: application/json' \ - -d '{"prover":"Z3","content":"(assert (forall ((x Int)) (= (+ x 0) x)))(check-sat)"}' +[source,console] +---- +curl -s https://api.nesy-prover.dev/api/health # {"status":"ok",...} +curl -s https://api.nesy-prover.dev/api/provers | head +curl -s -X POST https://api.nesy-prover.dev/api/verify \ + -H 'content-type: application/json' \ + -d '{"prover":"Z3","content":"(assert (forall ((x Int)) (= (+ x 0) x)))(check-sat)"}' +---- Controls: - # Rate limit: burst 40 requests, expect HTTP 429 after ~30 - for i in $(seq 1 40); do curl -s -o /dev/null -w '%{http_code} ' \ - https://api.nesy-prover.dev/api/health; done; echo - # Headers: HSTS present, Server header absent - curl -sI https://api.nesy-prover.dev/api/health - # Isolation: direct API port must be unreachable from outside - curl -m 5 http://:8081/api/health || echo "unreachable (correct)" +[source,console] +---- +# Rate limit: burst 40 requests, expect HTTP 429 after ~30 +for i in $(seq 1 40); do curl -s -o /dev/null -w '%{http_code} ' \ + https://api.nesy-prover.dev/api/health; done; echo + +# Headers: HSTS present, Server header absent +curl -sI https://api.nesy-prover.dev/api/health + +# Isolation: the API port must NOT be reachable directly. This probe is +# deliberately plaintext against the raw port — it is asserting that +# nothing answers there, and must fail. +curl -m 5 http://:8081/api/health && echo "REACHABLE - FIX THIS" || echo "unreachable (correct)" +---- -Reboot survival (validates linger + [Install] + Restart in one shot): +Reboot survival (validates linger + `[Install]` + Restart in one shot): - sudo reboot - # after it returns: - podman ps && curl -s https://api.nesy-prover.dev/api/health +[source,console] +---- +sudo reboot +# after it returns: +podman ps && curl -s https://api.nesy-prover.dev/api/health +---- == 5. Updates and rollback -Enable unattended rollout of new releases (ghcr-publish.yml pushes -`:latest` on every GitHub release): - - systemctl --user enable --now podman-auto-update.timer - podman auto-update --dry-run # see what would change - podman auto-update # roll out immediately - -`podman-auto-update` restarts the unit on a new image and rolls back -automatically if the fresh container fails its healthcheck. - -Manual rollback to a recorded digest: - - podman pull ghcr.io/hyperpolymath/echidna@ - podman tag ghcr.io/hyperpolymath/echidna@ ghcr.io/hyperpolymath/echidna:latest - systemctl --user restart echidna - -Pinned mode (opt out of auto-update): set `Image=` in -`echidna.container` to a `:vX.Y.Z` tag or digest, remove -`AutoUpdate=registry`, and bump via PR. - -== Appendix: Debian 12 fallback (podman 4.3, no quadlets) - - podman network create echidna-net - podman create --name echidna --network echidna-net \ - --memory=1500m --pids-limit=512 --tmpfs /tmp:rw,size=256m \ - --security-opt no-new-privileges \ - --health-cmd '/app/bin/echidna --version' --health-interval 30s \ - ghcr.io/hyperpolymath/echidna:latest server --port 8081 --host 0.0.0.0 --cors - podman create --name caddy --network echidna-net \ - -p 80:80 -p 443:443 \ - -v /opt/echidna/Caddyfile:/etc/caddy/Caddyfile:ro \ - -v caddy-data:/data -v caddy-config:/config \ - localhost/caddy-rl:2 - podman generate systemd --new --files --name echidna - podman generate systemd --new --files --name caddy - mkdir -p ~/.config/systemd/user && mv container-*.service ~/.config/systemd/user/ - systemctl --user daemon-reload - systemctl --user enable --now container-echidna container-caddy +`ghcr-publish.yml` pushes a new `:latest` on every GitHub release. +Enable unattended rollout: + +[source,console] +---- +systemctl --user enable --now podman-auto-update.timer +podman auto-update --dry-run # see what would change +podman auto-update # roll out immediately +---- + +How the safety net actually works: `podman auto-update` pulls the new +image and restarts the unit. `HealthOnFailure=kill` in +`echidna.container` means a container that goes unhealthy is killed, +which fails the systemd unit — and auto-update rolls the unit back to +the image it was running before when the restarted unit does not come +up healthy. Without that key an unhealthy-but-running container would +satisfy systemd and no rollback would occur, so do not remove it. + +Manual rollback to a recorded digest. *Stop the timer first* — +otherwise its next run pulls registry `:latest` again and silently +undoes the rollback: + +[source,console] +---- +systemctl --user disable --now podman-auto-update.timer +podman pull ghcr.io/hyperpolymath/echidna@ +podman tag ghcr.io/hyperpolymath/echidna@ ghcr.io/hyperpolymath/echidna:latest +systemctl --user restart echidna +---- + +Re-enable the timer only once a fixed `:latest` has been published, +or switch to pinned mode permanently: set `Image=` in +`echidna.container` to a `:vX.Y.Z` tag or digest, drop +`AutoUpdate=registry`, and bump it via PR. + +== Appendix: fallback for podman without quadlet support + +[source,console] +---- +podman network create echidna-net +podman create --name echidna --network echidna-net \ + --memory=1500m --pids-limit=512 --tmpfs /tmp:rw,size=256m \ + --security-opt no-new-privileges \ + --health-cmd '/app/bin/echidna --version' --health-interval 30s \ + --health-on-failure kill \ + ghcr.io/hyperpolymath/echidna:latest server --port 8081 --host 0.0.0.0 --cors +podman create --name caddy --network echidna-net \ + -p 80:80 -p 443:443 \ + -v /opt/echidna/Caddyfile:/etc/caddy/Caddyfile:ro \ + -v caddy-data:/data -v caddy-config:/config \ + localhost/caddy-rl:2 +podman generate systemd --new --files --name echidna +podman generate systemd --new --files --name caddy +mkdir -p ~/.config/systemd/user && mv container-*.service ~/.config/systemd/user/ +systemctl --user daemon-reload +systemctl --user enable --now container-echidna container-caddy +---- diff --git a/deploy/hetzner/echidna.container b/deploy/hetzner/echidna.container index 09569d3..51e3e55 100644 --- a/deploy/hetzner/echidna.container +++ b/deploy/hetzner/echidna.container @@ -25,6 +25,10 @@ Exec=server --port 8081 --host 0.0.0.0 --cors Environment=RUST_LOG=info HealthCmd=/app/bin/echidna --version HealthInterval=30s +# kill (not stop) is what integrates with systemd: an unhealthy +# container fails the unit, which is what makes Restart=always and +# podman-auto-update's rollback actually trigger. +HealthOnFailure=kill Tmpfs=/tmp:rw,size=256m NoNewPrivileges=true PodmanArgs=--memory=1500m --pids-limit=512