From 82377d42bd22b8590377c6af0a3478ff811b7ae9 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 23:44:38 +0000 Subject: [PATCH 1/2] fix(echidnabot): send the route credential; keep obligation text out of the manifest echidnabot's GraphQL API now needs a bearer credential (hyperpolymath/echidnabot#192). Hypatia holds the route credential, which may only call submitProofObligation for repositories echidnabot lists. - EchidnabotObligation.auth_headers/0 reads HYPATIA_ECHIDNABOT_TOKEN (trimmed; unset or blank sends no header) and both senders use it: FleetDispatcher on the per-bot HYPATIA_ECHIDNABOT_URL path only, never the fleet coordinator, and LearningScheduler's re-queue. - The dispatch manifest line for echidnabot records variables_sha256 instead of the variables. Claim and context can quote unpublished code, and data/verisim is a git-backed tree. Other bots are unchanged. - Tests capture request headers: the credential reaches the per-bot path and the re-queue, is absent when the variable is blank, never reaches the fleet coordinator, and the manifest line holds no claim or context. Plan: metadatastician/standards#1397 (Wave 0, merged row 2). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- docs/wiki-pages/Operations.md | 1 + lib/echidnabot_obligation.ex | 39 +++++++++++++++++++ lib/fleet_dispatcher.ex | 46 +++++++++++++++++----- lib/learning_scheduler.ex | 5 ++- test/echidnabot_dispatch_test.exs | 64 +++++++++++++++++++++++++++++-- 5 files changed, 140 insertions(+), 15 deletions(-) diff --git a/docs/wiki-pages/Operations.md b/docs/wiki-pages/Operations.md index 7adf9430..ea9ff53e 100644 --- a/docs/wiki-pages/Operations.md +++ b/docs/wiki-pages/Operations.md @@ -58,6 +58,7 @@ The supervision tree starts Bandit on port 9090 (9099 under `MIX_ENV=test`): | `HYPATIA_HTTP_PORT` | Override the Bandit listen port (default 9090) | | `HYPATIA_VERISIM_URL` | verisim-api base URL. No default: unset or blank turns off prover hints, strategy-shift detection and recommender retraining | | `HYPATIA_ECHIDNABOT_URL` | echidnabot base URL (`/graphql` is appended). No default: unset or blank means strategy-shift re-queues are logged and dropped | +| `HYPATIA_ECHIDNABOT_TOKEN` | echidnabot's *route* credential (its `ECHIDNABOT_API_ROUTE_TOKEN`), sent as a bearer header to `HYPATIA_ECHIDNABOT_URL` only. Unset or blank sends no header, and echidnabot answers 401 | | `HYPATIA_FLEET_PATH` | Path to the gitbot-fleet checkout | | `HYPATIA_ALERT_WEBHOOK_URL` | Webhook for watcher alerts | | `HYPATIA_ALERT_LOG_FILE` | File sink for watcher alerts | diff --git a/lib/echidnabot_obligation.ex b/lib/echidnabot_obligation.ex index 452c4cbe..73156a14 100644 --- a/lib/echidnabot_obligation.ex +++ b/lib/echidnabot_obligation.ex @@ -97,6 +97,45 @@ defmodule Hypatia.EchidnabotObligation do @spec graphql_url(String.t()) :: String.t() def graphql_url(base_url) when is_binary(base_url), do: base_url <> "/graphql" + @token_env "HYPATIA_ECHIDNABOT_TOKEN" + + @doc """ + The `:httpc` request headers that authenticate hypatia to echidnabot. + + echidnabot's GraphQL API needs a bearer credential. Hypatia holds the + *route* credential, which may only call `submitProofObligation`, for the + repositories echidnabot's `[api] route_repos` lists. It is read from + `HYPATIA_ECHIDNABOT_TOKEN`, with surrounding whitespace removed; when that + is unset or blank no header is sent and echidnabot answers 401. + + Send these headers only to `HYPATIA_ECHIDNABOT_URL`, never to another + service. The credential never appears in a log line or a manifest. + """ + @spec auth_headers() :: [{charlist(), charlist()}] + def auth_headers do + case System.get_env(@token_env) do + value when is_binary(value) -> + case String.trim(value) do + "" -> [] + token -> [{~c"authorization", String.to_charlist("Bearer " <> token)}] + end + + nil -> + [] + end + end + + @doc """ + The manifest form of an obligation's GraphQL variables: a SHA-256 digest of + their JSON encoding, so a manifest line can be matched to a request without + holding the claim or context text. Claim and context can quote unpublished + code, and the manifest lives in a git-backed tree. + """ + @spec variables_digest(map()) :: String.t() + def variables_digest(variables) when is_map(variables) do + :crypto.hash(:sha256, Jason.encode!(variables)) |> Base.encode16(case: :lower) + end + # Add the optional `prover` field when there is a ProverKind for it. defp put_prover(input, nil), do: input defp put_prover(input, kind), do: Map.put(input, "prover", kind) diff --git a/lib/fleet_dispatcher.ex b/lib/fleet_dispatcher.ex index 8eb56f58..b7d08102 100644 --- a/lib/fleet_dispatcher.ex +++ b/lib/fleet_dispatcher.ex @@ -744,8 +744,13 @@ defmodule Hypatia.FleetDispatcher do # # `variables` (default nil) is the GraphQL variables map for a document # that declares them, as echidnabot's submitProofObligation does. When - # given, it is recorded in the manifest line next to `query` and sent in - # the request's JSON envelope. + # given, it is sent in the request's JSON envelope. The manifest line + # records it too, except for echidnabot: an obligation's claim and context + # can quote unpublished code and the manifest lives in a git-backed tree, so + # that line records only a digest of the variables (`variables_sha256`). + # + # Only the per-bot echidnabot path (HYPATIA_ECHIDNABOT_URL) carries + # echidnabot's bearer credential; the fleet coordinator never sees it. defp execute_graphql(query, bot_name, variables \\ nil) do # Dual dispatch: file-based (immediate) + HTTP (when fleet API available) dispatch_record = @@ -755,7 +760,7 @@ defmodule Hypatia.FleetDispatcher do "dispatched_at" => DateTime.utc_now() |> DateTime.to_iso8601(), "status" => "pending" } - |> maybe_put_variables(variables) + |> manifest_variables(bot_name, variables) # 1. Always write to dispatch manifest (dispatch-runner.sh reads this) manifest_result = write_manifest(dispatch_record) @@ -775,9 +780,14 @@ defmodule Hypatia.FleetDispatcher do graphql_envelope? = description != :none and String.starts_with?(description, "via per-bot") + headers = + if graphql_envelope? and bot_name == "echidnabot", + do: Hypatia.EchidnabotObligation.auth_headers(), + else: [] + cond do target_url -> - case live_post(target_url, body, graphql_envelope?) do + case live_post(target_url, body, graphql_envelope?, headers) do :ok -> Logger.info("Live dispatch to #{bot_name} succeeded (#{description})") {:ok, :dispatched} @@ -821,8 +831,8 @@ defmodule Hypatia.FleetDispatcher do # a 2xx whose JSON body carries a non-empty `errors` list is a failure, as # GraphQL-over-HTTP reports resolver errors with status 200. Exceptions and # exits (e.g. :inets not started) become `{:error, _}` instead of crashing. - defp live_post(url, body, graphql_envelope?) do - case http_post(url, body) do + defp live_post(url, body, graphql_envelope?, headers) do + case http_post(url, body, headers) do {:ok, _status, response_body} when graphql_envelope? -> graphql_errors(response_body) @@ -897,13 +907,29 @@ defmodule Hypatia.FleetDispatcher do defp maybe_put_variables(map, nil), do: map defp maybe_put_variables(map, variables), do: Map.put(map, "variables", variables) - # POST a JSON body. Returns `{:ok, status, body}` for a 2xx response, - # `{:error, {:http_status, status}}` for any other status, or the :httpc error. - defp http_post(url, body) do + # The variables a manifest line records: a digest for echidnabot (see + # execute_graphql/3), the variables themselves for any other bot. + defp manifest_variables(record, _bot_name, nil), do: record + + defp manifest_variables(record, "echidnabot", variables), + do: + Map.put( + record, + "variables_sha256", + Hypatia.EchidnabotObligation.variables_digest(variables) + ) + + defp manifest_variables(record, _bot_name, variables), + do: maybe_put_variables(record, variables) + + # POST a JSON body with `headers` added. Returns `{:ok, status, body}` for a + # 2xx response, `{:error, {:http_status, status}}` for any other status, or + # the :httpc error. + defp http_post(url, body, headers) do # Attempt HTTP POST -- works if :httpc is available (OTP built-in) case :httpc.request( :post, - {String.to_charlist(url), [{~c"content-type", ~c"application/json"}], + {String.to_charlist(url), [{~c"content-type", ~c"application/json"} | headers], ~c"application/json", String.to_charlist(body)}, [{:timeout, 10_000}], [] diff --git a/lib/learning_scheduler.ex b/lib/learning_scheduler.ex index 6bf74ada..d81e427c 100644 --- a/lib/learning_scheduler.ex +++ b/lib/learning_scheduler.ex @@ -494,8 +494,9 @@ defmodule Hypatia.LearningScheduler do case :httpc.request( :post, - {String.to_charlist(url), [{~c"accept", ~c"application/json"}], ~c"application/json", - body}, + {String.to_charlist(url), + [{~c"accept", ~c"application/json"} | EchidnabotObligation.auth_headers()], + ~c"application/json", body}, [{:timeout, timeout_ms}], [] ) do diff --git a/test/echidnabot_dispatch_test.exs b/test/echidnabot_dispatch_test.exs index 49b66f7d..1d56c79b 100644 --- a/test/echidnabot_dispatch_test.exs +++ b/test/echidnabot_dispatch_test.exs @@ -31,6 +31,7 @@ defmodule Hypatia.EchidnabotDispatchTest do on_exit(fn -> System.delete_env("HYPATIA_ECHIDNABOT_URL") + System.delete_env("HYPATIA_ECHIDNABOT_TOKEN") System.delete_env("HYPATIA_FLEET_URL") Application.put_env(:hypatia, :verisimdb_data_path, original_path) File.rm_rf!(data_path) @@ -53,6 +54,7 @@ defmodule Hypatia.EchidnabotDispatchTest do [request_line | header_lines] = String.split(head, "\r\n") body = recv_body(sock, body_start, content_length(header_lines)) send(test_pid, {:captured, request_line, body}) + send(test_pid, {:captured_headers, header_lines}) :gen_tcp.send( sock, @@ -107,6 +109,20 @@ defmodule Hypatia.EchidnabotDispatchTest do {request_line, Jason.decode!(body)} end + # The captured request's headers as a map of lower-cased name => value. + # Call after captured!/0. + defp captured_headers! do + assert_receive {:captured_headers, header_lines}, 5_000 + + Map.new(header_lines, fn line -> + [name, value] = String.split(line, ":", parts: 2) + {String.downcase(String.trim(name)), String.trim(value)} + end) + end + + # Test-only credential (the `test-` prefix marks it for the secret scanner). + @token "test-route-credential-0123456789abcdef" + # A :proof_obligation finding carrying the hostile claim, with `overrides` merged in. defp obligation(overrides) do Map.merge( @@ -154,19 +170,52 @@ defmodule Hypatia.EchidnabotDispatchTest do refute Map.has_key?(envelope["variables"]["input"], "prover") end - test "records the variables in the manifest line next to the static query", %{ + test "records only a digest of the variables in the manifest line", %{ manifest: manifest } do System.put_env("HYPATIA_ECHIDNABOT_URL", capturing_server(200, @accepted)) assert {:ok, :dispatched} = FleetDispatcher.dispatch_finding(obligation(%{})) - _ = captured!() + {_request_line, envelope} = captured!() [line] = manifest |> File.read!() |> String.split("\n", trim: true) record = Jason.decode!(line) assert record["bot"] == "echidnabot" assert record["query"] == Hypatia.EchidnabotObligation.mutation() - assert record["variables"]["input"]["claim"] == @hostile_claim + refute Map.has_key?(record, "variables") + refute line =~ "line one" + refute line =~ "across lines" + + assert record["variables_sha256"] == + Hypatia.EchidnabotObligation.variables_digest(envelope["variables"]) + end + + test "sends the route credential on the per-bot echidnabot path" do + System.put_env("HYPATIA_ECHIDNABOT_TOKEN", " " <> @token <> "\n") + System.put_env("HYPATIA_ECHIDNABOT_URL", capturing_server(200, @accepted)) + + assert {:ok, :dispatched} = FleetDispatcher.dispatch_finding(obligation(%{})) + _ = captured!() + assert captured_headers!()["authorization"] == "Bearer " <> @token + end + + test "sends no authorization header when HYPATIA_ECHIDNABOT_TOKEN is blank" do + System.put_env("HYPATIA_ECHIDNABOT_TOKEN", " ") + System.put_env("HYPATIA_ECHIDNABOT_URL", capturing_server(200, @accepted)) + + assert {:ok, :dispatched} = FleetDispatcher.dispatch_finding(obligation(%{})) + _ = captured!() + refute Map.has_key?(captured_headers!(), "authorization") + end + + test "never sends the echidnabot credential to the fleet coordinator" do + System.put_env("HYPATIA_ECHIDNABOT_TOKEN", @token) + System.put_env("HYPATIA_FLEET_URL", capturing_server(200, "{}")) + + assert {:ok, :dispatched} = FleetDispatcher.dispatch_finding(obligation(%{})) + {request_line, _envelope} = captured!() + assert request_line =~ ~r{^POST /dispatch/echidnabot HTTP/1\.[01]$} + refute Map.has_key?(captured_headers!(), "authorization") end test "sends the JSON envelope, variables included, on the fleet-coordinator path" do @@ -261,5 +310,14 @@ defmodule Hypatia.EchidnabotDispatchTest do refute Map.has_key?(envelope["variables"]["input"], "prover") refute inspect(envelope) =~ "LEAN4" end + + test "sends the route credential with each re-queue" do + System.put_env("HYPATIA_ECHIDNABOT_TOKEN", @token) + System.put_env("HYPATIA_ECHIDNABOT_URL", capturing_server(200, @accepted)) + + assert :ok = LearningScheduler.requeue_candidates("cls", "coq", ["att-3"]) + _ = captured!() + assert captured_headers!()["authorization"] == "Bearer " <> @token + end end end From 359f0a8f14c2955e2addab23193098dd32d8d4d0 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 04:50:02 +0000 Subject: [PATCH 2/2] fix(dispatch): do not follow redirects on the authenticated echidnabot POSTs :httpc follows redirects by default. Probed on OTP 25: for 307/308 it re-POSTs the body to the Location host and reports that host's 2xx as success; for 301/302/303 it re-sends as GET. CodeRabbit reports that OTP releases before 27.3.4.13 also forward the authorization header across hosts (the repo pins 27.3.4.4). Either way the obligation's claim and context, and possibly the route credential, could reach a host other than HYPATIA_ECHIDNABOT_URL. FleetDispatcher.http_post/3 and LearningScheduler.http_post_json/3 now pass {:autoredirect, false}; a 3xx is reported as {:error, {:http_status, 3xx}}. Two tests point the echidnabot URL at a server that answers 307/308 and assert the redirect target is never contacted. The manifest digest test now computes the expected SHA-256 itself instead of calling variables_digest/1. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgzT72Tq2HTJmikyNg --- lib/fleet_dispatcher.ex | 7 +++- lib/learning_scheduler.ex | 4 ++- test/echidnabot_dispatch_test.exs | 57 +++++++++++++++++++++++++++++-- 3 files changed, 64 insertions(+), 4 deletions(-) diff --git a/lib/fleet_dispatcher.ex b/lib/fleet_dispatcher.ex index b7d08102..c6538158 100644 --- a/lib/fleet_dispatcher.ex +++ b/lib/fleet_dispatcher.ex @@ -925,13 +925,18 @@ defmodule Hypatia.FleetDispatcher do # POST a JSON body with `headers` added. Returns `{:ok, status, body}` for a # 2xx response, `{:error, {:http_status, status}}` for any other status, or # the :httpc error. + # + # Redirects are not followed. :httpc would otherwise re-send the body (and, + # on some OTP releases, the authorization header) to whatever host the + # Location names, and report that host's 2xx as a delivered dispatch. A + # redirect is reported as `{:error, {:http_status, 3xx}}`. defp http_post(url, body, headers) do # Attempt HTTP POST -- works if :httpc is available (OTP built-in) case :httpc.request( :post, {String.to_charlist(url), [{~c"content-type", ~c"application/json"} | headers], ~c"application/json", String.to_charlist(body)}, - [{:timeout, 10_000}], + [{:timeout, 10_000}, {:autoredirect, false}], [] ) do {:ok, {{_, status, _}, _, response_body}} when status in 200..299 -> diff --git a/lib/learning_scheduler.ex b/lib/learning_scheduler.ex index d81e427c..57d76ace 100644 --- a/lib/learning_scheduler.ex +++ b/lib/learning_scheduler.ex @@ -497,7 +497,9 @@ defmodule Hypatia.LearningScheduler do {String.to_charlist(url), [{~c"accept", ~c"application/json"} | EchidnabotObligation.auth_headers()], ~c"application/json", body}, - [{:timeout, timeout_ms}], + # Never follow a redirect with the credential and the obligation + # body: a 3xx is reported as {:error, {:http_status, 3xx}}. + [{:timeout, timeout_ms}, {:autoredirect, false}], [] ) do {:ok, {{_, status, _}, _headers, resp_body}} when status in 200..299 -> diff --git a/test/echidnabot_dispatch_test.exs b/test/echidnabot_dispatch_test.exs index 1d56c79b..dba1b7c8 100644 --- a/test/echidnabot_dispatch_test.exs +++ b/test/echidnabot_dispatch_test.exs @@ -69,6 +69,33 @@ defmodule Hypatia.EchidnabotDispatchTest do "http://127.0.0.1:#{port}" end + # Answer exactly one request with `status` and `location`, then send + # `:redirect_served` to the test process. Returns the base URL. + defp redirecting_server(status, location) do + test_pid = self() + {:ok, listen} = :gen_tcp.listen(0, [:binary, packet: :raw, active: false, reuseaddr: true]) + {:ok, port} = :inet.port(listen) + + spawn_link(fn -> + {:ok, sock} = :gen_tcp.accept(listen) + {head, body_start} = recv_head(sock, "") + [_request_line | header_lines] = String.split(head, "\r\n") + _ = recv_body(sock, body_start, content_length(header_lines)) + + :gen_tcp.send( + sock, + "HTTP/1.1 #{status} X\r\nlocation: #{location}\r\n" <> + "content-length: 0\r\nconnection: close\r\n\r\n" + ) + + send(test_pid, :redirect_served) + :gen_tcp.close(sock) + :gen_tcp.close(listen) + end) + + "http://127.0.0.1:#{port}" + end + # Read until the end of the HTTP header block; returns {head, body_so_far}. defp recv_head(sock, acc) do case :binary.split(acc, "\r\n\r\n") do @@ -186,8 +213,23 @@ defmodule Hypatia.EchidnabotDispatchTest do refute line =~ "line one" refute line =~ "across lines" - assert record["variables_sha256"] == - Hypatia.EchidnabotObligation.variables_digest(envelope["variables"]) + # Computed here, not with variables_digest/1, so a wrong digest fails. + expected = + :crypto.hash(:sha256, Jason.encode!(envelope["variables"])) + |> Base.encode16(case: :lower) + + assert record["variables_sha256"] == expected + end + + test "does not follow a redirect with the credential and the obligation" do + System.put_env("HYPATIA_ECHIDNABOT_TOKEN", @token) + elsewhere = capturing_server(200, @accepted) + System.put_env("HYPATIA_ECHIDNABOT_URL", redirecting_server(307, elsewhere <> "/graphql")) + + FleetDispatcher.dispatch_finding(obligation(%{})) + + assert_receive :redirect_served, 5_000 + refute_receive {:captured, _, _}, 1_000 end test "sends the route credential on the per-bot echidnabot path" do @@ -319,5 +361,16 @@ defmodule Hypatia.EchidnabotDispatchTest do _ = captured!() assert captured_headers!()["authorization"] == "Bearer " <> @token end + + test "does not follow a redirect with the credential" do + System.put_env("HYPATIA_ECHIDNABOT_TOKEN", @token) + elsewhere = capturing_server(200, @accepted) + System.put_env("HYPATIA_ECHIDNABOT_URL", redirecting_server(308, elsewhere <> "/graphql")) + + LearningScheduler.requeue_candidates("cls", "coq", ["att-4"]) + + assert_receive :redirect_served, 5_000 + refute_receive {:captured, _, _}, 1_000 + end end end