fix(echidnabot): send the route credential; keep obligation text out of the manifest

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 |

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)

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,15 +907,36 @@ 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.
+  #
+  # 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"}],
+           {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 ->

lib/learning_scheduler.ex

@@ -494,9 +494,12 @@ defmodule Hypatia.LearningScheduler do
 
     case :httpc.request(
            :post,
-           {String.to_charlist(url), [{~c"accept", ~c"application/json"}], ~c"application/json",
-            body},
-           [{:timeout, timeout_ms}],
+           {String.to_charlist(url),
+            [{~c"accept", ~c"application/json"} | EchidnabotObligation.auth_headers()],
+            ~c"application/json", body},
+           # 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 ->

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,
@@ -67,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
@@ -107,6 +136,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 +197,67 @@ 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"
+
+      # 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
+      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 +352,25 @@ 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
+
+    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