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..0609433 --- /dev/null +++ b/deploy/hetzner/README.adoc @@ -0,0 +1,254 @@ +// 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`. +* *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) + +[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. +* 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: ++ +[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 +`podman login ghcr.io` as the deploy user. + +== 1. Server preparation (as root) + +[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 + +# 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 + +# Destination for the Caddyfile and the Caddy build context +mkdir -p /opt/echidna && chown deploy:deploy /opt/echidna +---- + +== 2. Install the deploy unit + +Create the quadlet directory *before* copying anything into it — as +the deploy user on the server: + +[source,console] +---- +mkdir -p ~/.config/containers/systemd +---- + +Then, from your workstation in this directory: + +[source,console] +---- +scp Caddyfile Containerfile.caddy deploy@:/opt/echidna/ +scp echidna.network echidna.container caddy.container \ + deploy@:~/.config/containers/systemd/ +---- + +Back on the server, as deploy: + +[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: + +[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: +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 + +[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: + +[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: + +[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): + +[source,console] +---- +sudo reboot +# after it returns: +podman ps && curl -s https://api.nesy-prover.dev/api/health +---- + +== 5. Updates and rollback + +`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/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..51e3e55 --- /dev/null +++ b/deploy/hetzner/echidna.container @@ -0,0 +1,41 @@ +# 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 +# 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 + +[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