From 4b46f3a71da93dc7d120c8ad30075679b49457b0 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:20:38 +0000 Subject: [PATCH 01/14] One parsed workflow model; RE001 and RE002 read it (#971) Hypatia.Workflow is #971's model. Each workflow is parsed once by Hypatia.Kyaml (the port of kyq's KYAML reader) into Workflow, Job and Step records: scalars a rule compares (uses, run, if) are their YAML values, folded and unquoted; mappings a rule walks (env, with) keep their nodes, so every value keeps its source line. What the reader refuses is an error at its location, never a guess. RE001 and RE002 read the model instead of scanning lines. This carries the part-2 work written against #1008 (tree-based RE001/RE002, the layout-equivalence harness, the endpoint comparison) onto main's current tree, where RE001's line reader had moved to Hypatia.WorkflowYaml; the rules after RE002 keep that reader until they move too. The three post-merge review threads on #975 are closed by construction, each with a test that fails on the line reader: - `<<: [*defaults]` is refused and reported, not misplaced; - text in a `name: |` block beside the hardener is not its input; - a folded `egress-policy: >-` is read as its value. Two defects in the endpoint comparison surfaced only when RE001 ran over real repositories, and are fixed with tests: an allowed-endpoints entry written with an expression crashed it (hypatia's own push-email-notify.yml), and a deed listing GitHub hosts drew 12 false findings on hypatia. Measured against the main branches of hypatia, standards, rsr-template-repo, choreographic-types, kyq and mathesis: the same 6 findings as the line reader. Also: the elixir_atom_from_user description names the right function and fix. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- .claude/CLAUDE.md | 2 +- .github/workflows/ci.yml | 2 + CHANGELOG.adoc | 50 + lib/hypatia/deed.ex | 11 +- lib/hypatia/workflow.ex | 226 ++++ lib/rules/code_safety.ex | 2 +- lib/rules/research_extensions.ex | 980 +++++++++--------- test/deed_test.exs | 2 + test/research_extensions_equivalence_test.exs | 229 ++++ test/research_extensions_test.exs | 339 +++++- test/workflow_test.exs | 172 +++ 11 files changed, 1482 insertions(+), 533 deletions(-) create mode 100644 lib/hypatia/workflow.ex create mode 100644 test/research_extensions_equivalence_test.exs create mode 100644 test/workflow_test.exs diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 62980ffc..476acedf 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -13,7 +13,7 @@ Hypatia is the neurosymbolic CI/CD intelligence layer for the hyperpolymath ecos ## Architecture ``` -Hypatia # 150 Elixir source files under lib/ (recursive tree count, 2026-11-04) +Hypatia # 155 Elixir source files under lib/ (recursive tree count, 2026-11-09) ├── Elixir pipeline # core: pattern analysis, dispatch, learning ├── Merge orchestration # 12 modules — leases, ledger, ticker (largest subsystem) ├── Kin subsystem # 6 modules — contingency, arbiter, gate, watchdog diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b9115f0c..8072daa8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -357,6 +357,8 @@ jobs: test/rules/audit_prevention_test.exs \ test/security_errors_test.exs \ test/research_extensions_test.exs \ + test/research_extensions_equivalence_test.exs \ + test/workflow_test.exs \ test/deed_test.exs \ test/kyaml_test.exs \ test/kyaml_conformance_test.exs diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 2a32f694..3eb59451 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -30,6 +30,56 @@ sequence is read (its harden-runner step counts), and a step opened by `-` and a comment keeps its `run:`. WH014 reads each job's steps through the same reader. On the hypatia, echidna and standards trees, WH013, WH014 and RE001 report exactly what they did before. +==== One parsed workflow model; RE001 and RE002 read it (#971) (2026-11-09) + +`Hypatia.Workflow` is #971's model: each workflow is parsed once by +`Hypatia.Kyaml`, the port of kyq's KYAML reader, into `Workflow`, `Job` and +`Step` records. Scalars a rule compares (`uses`, `run`, `if`) are their YAML +values, folded and unquoted; mappings a rule walks (`env`, `with`) keep their +nodes, so every value keeps its source line. RE001 and RE002 now read the +model instead of scanning lines (WH013 and WH014 follow, and +`Hypatia.WorkflowYaml` with them): + +* **Layout no longer changes a finding.** Block or flow YAML, plain or quoted + keys, literal or folded `run:` blocks and aliases all read the same. A new + equivalence harness (`test/research_extensions_equivalence_test.exs`) + renders seeded random workflows four ways and requires the same findings + from each. Run against the old line-based RE001, it fails on its seventh + case. +* **An unreadable workflow is reported, not guessed at.** A workflow the + reader refuses (a `<<` merge key, which GitHub also refuses; aliases past + kyq's node budget; any other KYAML error) gets a `:warn` RE001 finding at + the error, if it names `secrets`. Its deed declarations are not reported + stale. +* **The three post-merge review threads on #975 are closed by construction,** + each with a test that fails on the line reader: `<<: [*defaults]` is + refused and reported, not misplaced; text in a `name: |` block beside the + hardener is not its input, so an audit hardener no longer passes for a + block one; a folded `egress-policy: >-` is read as its value. +* **Declared endpoints are checked** against the workflow (`:warn`): a host + outside GitHub that a step names literally (a URL or a `git@host:` remote, + shell comments aside) must be covered by the job's `:endpoints`, and + harden-runner's `allowed-endpoints`, when listed, must agree with them. + An allowed entry written with an expression + (`${{ secrets.SMTP_HOST }}:465`) names its host only at run time and is not + compared, and GitHub's own hosts are outside the comparison on both sides. + `Hypatia.Deed.egress_declarations/1` now returns `:endpoints`. +* **RE002** finds harden-runner the way RE001 does: a real step, the owner in + any case, its own `with: egress-policy`. A step with no policy runs + harden-runner's default, `audit`, and is now reported. The trigger is a + `push` or `release` key of `on:`, not a `push:` anywhere in the file. + +The `code_safety/elixir_atom_from_user` description was backwards: it named +`String.to_existing_atom` as the danger. It now names `String.to_atom`. The +pattern was always right. + +Measured on 2026-11-09 against the main branches of hyperpolymath/hypatia, +rsr-template-repo, choreographic-types and mathesis, and +metadatastician/standards and kyq: RE001 and RE002 give the same 6 findings +as the line reader did. Two defects in the endpoint comparison surfaced only +there and are fixed with tests: an `allowed-endpoints` entry written with an +expression crashed it (hypatia's own `push-email-notify.yml`), and a deed +listing GitHub hosts drew 12 false findings on hypatia. ==== RE001 accepts a deed egress declaration; the job token no longer counts (2026-10-27) diff --git a/lib/hypatia/deed.ex b/lib/hypatia/deed.ex index ac633247..8a175272 100644 --- a/lib/hypatia/deed.ex +++ b/lib/hypatia/deed.ex @@ -87,7 +87,7 @@ defmodule Hypatia.Deed do The jobs declared in the repo deed's `(egress …)` clause. Returns `{:ok, deed_file, jobs}` where each job is - `%{workflow: path, job: id, secrets: MapSet, enforcement: name}`, `:none` when + `%{workflow: path, job: id, secrets: MapSet, endpoints: [string], enforcement: name}`, `:none` when the repo has no deed, or `{:error, deed_file, reason}` when the deed or the clause cannot be read. A deed without the clause declares nothing: `{:ok, deed_file, []}`. """ @@ -206,7 +206,14 @@ defmodule Hypatia.Deed do true <- Enum.all?(endpoints, &valid_endpoint?(&1, secrets)), {:symbol, enf} when enf in @enforcement <- by_key["enforcement"], true <- reason_ok?(by_key["reason"]) do - job = %{workflow: workflow, job: job, secrets: MapSet.new(secrets), enforcement: enf} + job = %{ + workflow: workflow, + job: job, + secrets: MapSet.new(secrets), + endpoints: endpoints, + enforcement: enf + } + {:cont, {:ok, [job | jobs]}} else _ -> diff --git a/lib/hypatia/workflow.ex b/lib/hypatia/workflow.ex new file mode 100644 index 00000000..4f9535bd --- /dev/null +++ b/lib/hypatia/workflow.ex @@ -0,0 +1,226 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +defmodule Hypatia.Workflow do + @moduledoc """ + One parsed model of a GitHub Actions workflow, for every rule that looks + inside workflows (#971). + + A workflow is parsed once by `Hypatia.Kyaml`, the port of kyq's KYAML reader + (YAML 1.2 Core Schema, block and flow), and read into three records: + + %Hypatia.Workflow{path, doc, triggers, env, permissions, jobs} + %Hypatia.Workflow.Job{id, line, node, runs_on, uses, if, env, permissions, steps} + %Hypatia.Workflow.Step{line, node, uses, run, run_style, with, env, if} + + Scalars a rule compares (`uses`, `run`, `if`) are their YAML *values*: a + folded or literal block scalar is folded and chomped, a quoted one + unquoted, an alias read through. Mappings a rule walks (`env`, `with`, + `permissions`) stay `Hypatia.Kyaml` nodes, so every value keeps its own + source line, and `strings/1` maps each byte of a value back to the line it + came from. A rule reports at a source line, never at a position in a + rewritten text. + + `run_style` is the scalar's style as the reader records it: `:plain`, + `:quoted` or `:block`. (The reader does not distinguish `|` from `>`; the + value already reflects the difference.) + + What the reader refuses is not guessed at. A `<<` merge key (which GitHub + Actions refuses too), a document past kyq's node budget, or any other KYAML + error is `{:error, %Hypatia.Kyaml.Error{}}`, at the error's location, and a + rule decides how to report a workflow it cannot read. + """ + + alias Hypatia.Kyaml + + defstruct [:path, :doc, triggers: [], env: nil, permissions: nil, jobs: []] + + defmodule Job do + @moduledoc "A job of a workflow: its own fields, with its steps in order." + defstruct [ + :id, + :line, + :node, + :runs_on, + :uses, + :if, + :env, + :permissions, + steps: [] + ] + end + + defmodule Step do + @moduledoc "A step of a job: its own fields, values read as YAML gives them." + defstruct [:line, :node, :uses, :run, :run_style, :with, :env, :if] + end + + @type t :: %__MODULE__{} + + @doc """ + Reads a workflow file. `{:ok, nil}` for an empty stream. + """ + def read(path), do: path |> File.read!() |> parse(path) + + @doc """ + Parses a workflow's bytes into the model. The first document is the + workflow; `{:ok, nil}` for an empty stream. + """ + def parse(bytes, path \\ nil) when is_binary(bytes) do + case Kyaml.parse(bytes) do + {:ok, []} -> {:ok, nil} + {:ok, [doc | _]} -> from_doc(doc, path) + {:error, error} -> {:error, error} + end + end + + # Past kyq's node budget the workflow is refused, as kyq's bridge refuses + # it, rather than read in part. + defp from_doc(doc, path) do + if Kyaml.within_budget?(doc) do + {:ok, + %__MODULE__{ + path: path, + doc: doc, + triggers: events(doc), + env: Kyaml.get(doc, "env"), + permissions: Kyaml.get(doc, "permissions"), + jobs: for(entry <- entries(Kyaml.get(doc, "jobs")), do: job(entry)) + }} + else + {line, column} = doc.loc + + {:error, + %Kyaml.Error{ + code: "NODE_BUDGET_EXCEEDED", + message: + "the document expands to more than #{Kyaml.node_budget()} nodes through its aliases", + line: line, + column: column + }} + end + end + + defp job(%{key: key, value: value}) do + node = Kyaml.deref(value) + + %Job{ + id: key.value, + line: elem(key.loc, 0), + node: value, + runs_on: Kyaml.get(node, "runs-on"), + uses: text(Kyaml.get(node, "uses")), + if: text(Kyaml.get(node, "if")), + env: Kyaml.get(node, "env"), + permissions: Kyaml.get(node, "permissions"), + steps: for(item <- items(Kyaml.get(node, "steps")), do: step(item)) + } + end + + defp step(item) do + node = Kyaml.deref(item) + run = Kyaml.get(node, "run") + + %Step{ + line: elem(item.loc, 0), + node: node, + uses: text(Kyaml.get(node, "uses")), + run: text(run), + run_style: run && Kyaml.deref(run)[:style], + with: Kyaml.get(node, "with"), + env: Kyaml.get(node, "env"), + if: text(Kyaml.get(node, "if")) + } + end + + @doc """ + The events of the workflow's `on:`: `on: push`, a list, or the keys of a + mapping (`on: {push: {paths: […]}}` names one event). + """ + def events(doc) do + case Kyaml.get(doc, "on") && Kyaml.deref(Kyaml.get(doc, "on")) do + %{kind: :map, entries: entries} -> Enum.map(entries, &to_string(&1.key.value)) + %{kind: :seq, items: items} -> Enum.flat_map(items, &(&1 |> text() |> List.wrap())) + %{} = scalar -> ~r/[A-Za-z_]+/ |> Regex.scan(text(scalar) || "") |> List.flatten() + nil -> [] + end + end + + @doc "A step input's value (`with: {egress-policy: block}`), or nil." + def input(%Step{with: with}, name), do: with |> Kyaml.get(name) |> text() + + @doc "The entries of a mapping node (through an alias); [] for anything else." + def entries(node) do + case node && Kyaml.deref(node) do + %{kind: :map, entries: entries} -> entries + _ -> [] + end + end + + @doc "The items of a sequence node (through an alias); [] for anything else." + def items(node) do + case node && Kyaml.deref(node) do + %{kind: :seq, items: items} -> items + _ -> [] + end + end + + @doc """ + A scalar's text, whatever it resolved to (`egress-policy: block`, `ref: 1`): + the value of a string, the source text of any other scalar; nil for a + collection or a missing node. + """ + def text(node) do + case node && Kyaml.deref(node) do + %{kind: :string, value: value} -> value + %{kind: kind, raw: raw} when kind not in [:map, :seq] -> raw + _ -> nil + end + end + + @doc """ + The string values under a node in document order, each with a function + from a byte offset in the value to its source line. A block scalar maps + each of its lines; through an alias, every offset maps to the alias's line. + The walk is bounded like the reader: past kyq's node budget a node yields + nothing more. + """ + def strings(node), do: strings(node, nil) + + def strings(nil, _), do: [] + + def strings(node, alias_line) do + if Kyaml.within_budget?(node), do: walk(node, alias_line), else: [] + end + + defp walk(%{kind: :alias, target: target, loc: {line, _}}, alias_line), + do: walk(target, alias_line || line) + + defp walk(%{kind: :map, entries: entries}, alias_line), + do: Enum.flat_map(entries, &walk(&1.value, alias_line)) + + defp walk(%{kind: :seq, items: items}, alias_line), + do: Enum.flat_map(items, &walk(&1, alias_line)) + + defp walk(%{kind: :string, value: value} = scalar, alias_line) do + line_of = + cond do + alias_line -> + fn _ -> alias_line end + + scalar.segments == [] -> + fn _ -> elem(scalar.loc, 0) end + + true -> + fn at -> + scalar.segments + |> Enum.take_while(fn {offset, _} -> offset <= at end) + |> List.last({0, elem(scalar.loc, 0) + 1}) + |> elem(1) + end + end + + [{value, line_of}] + end + + defp walk(_scalar, _alias_line), do: [] +end diff --git a/lib/rules/code_safety.ex b/lib/rules/code_safety.ex index 54aa47a9..732b30cc 100644 --- a/lib/rules/code_safety.ex +++ b/lib/rules/code_safety.ex @@ -494,7 +494,7 @@ defmodule Hypatia.Rules.CodeSafety do pattern: ~r/String\.to_atom\(/, cwe: "CWE-400", description: - "String.to_atom with user input exhausts atom table -- use to_existing_atom" + "String.to_atom with user input exhausts the atom table -- use String.to_existing_atom or a fixed map" }, %{ id: :elixir_wildcard_plug_cors, diff --git a/lib/rules/research_extensions.ex b/lib/rules/research_extensions.ex index 253071d6..a882d75e 100644 --- a/lib/rules/research_extensions.ex +++ b/lib/rules/research_extensions.ex @@ -105,23 +105,12 @@ defmodule Hypatia.Rules.ResearchExtensions do require Logger - # The workflow reader these rules share with the others that read inside - # workflows (Hypatia.WorkflowYaml). - import Hypatia.WorkflowYaml, - only: [ - active_lines: 1, - direct_job_field?: 2, - indent_of: 1, - job_field_indent: 1, - job_steps: 1, - key_line?: 2, - lines_in_steps: 2, - nesting_at: 2, - step_indent: 2, - step_key_column: 1, - strip_yaml_comment: 1, - workflow_job_lines: 1 - ] + alias Hypatia.Workflow + alias Hypatia.Workflow.Step + + # The rules after RE002 still read lines; they share this primitive with + # Hypatia.WorkflowYaml until they move to the model too (#971). + import Hypatia.WorkflowYaml, only: [indent_of: 1] # ─── Workflow-file discovery ──────────────────────────────────────── @@ -197,9 +186,6 @@ defmodule Hypatia.Rules.ResearchExtensions do # Where naming that head means fetching its code: a checkout's `ref:` or # `repository:`, or a git checkout/fetch/switch in a `run:` script. A head # SHA in `env:`, an `if:` or a `concurrency:` group only names it. - # Block (`ref: …`) or flow (`with: {ref: …}`) form, the key plain or quoted. - @re001_checkout_key ~r/(?:^|[\s{,])["']?(?:ref|repository)["']?\s*:/ - @re001_checkout_action ~r/^\s*(?:-\s+)?["']?uses["']?\s*:\s*["']?actions\/checkout@/ # One git command naming the head: no `;`, `&` or `|` between them. `\s` # spans the line break of a folded `run: >-`. @re001_git_head_fetch ~r/\bgit\s+(?:checkout|fetch|switch)\b[^;&|]*?(?:github\.event\.pull_request\.head\.|github\.event\.workflow_run\.head(?:\.|_(?:sha|branch|repository)\b)|github\.head_ref)/ @@ -253,38 +239,47 @@ defmodule Hypatia.Rules.ResearchExtensions do secret (stale), reported against the deed. An unreadable deed or clause declares nothing, and the finding says why. - `:endpoints` are not compared with the workflow: that needs run-time - observation or a model of what each action reaches. - - Full-line comments and reusable-workflow jobs without a direct `runs-on` - field are ignored. Keys are matched plain or quoted, as YAML reads them, and - YAML aliases are expanded before jobs are read (`expand_aliases/1`). + `:endpoints` are compared with what the workflow shows, as `:warn` findings: + + * a host outside GitHub that a step names literally (a URL, or a + `git@host:` remote; not in a `#` comment) must be covered by a declared + endpoint, where `*.x` covers the subdomains of x and an endpoint without a + port covers every port; + * when the job's harden-runner step lists `allowed-endpoints`, every host + outside GitHub on it must be declared, and every declared literal host + must be on it. + + What an action or a variable reaches at run time is not modelled: that + needs run-time observation. + + ## Read from the parse tree (#971) + + Each workflow is read once into `Hypatia.Workflow` (#971), over `Hypatia.Kyaml`, the port of kyq's KYAML reader + (block and flow YAML, YAML 1.2 Core Schema), and every check reads the + tree. So: + + * **`runs-on` belongs to the job directly.** A reusable job (`uses:` at + job level) delegates its runtime to the source workflow; it is local + only with its own `runs-on` key, never a sibling's. + * **The hardener is a real step.** A step whose `uses:` names + `step-security/harden-runner` (in any case, and in any scalar style) + installs it. The same text in a `run:` block, a comment or `env:` data + is not a step. + * **Layout does not change the answer.** Block or flow, plain or quoted + keys, aliases (read through, within kyq's node budget): the findings are + the same, apart from line numbers. The equivalence harness in + `test/research_extensions_equivalence_test.exs` checks this on seeded + random workflows. + + A workflow kyq would refuse (a `<<` merge key, which GitHub also refuses; + a document past the node budget; any other KYAML error) is not guessed at. + If it names `secrets`, RE001 reports it as unreadable, at the error's + location. Its declarations are not reported stale, since they cannot be + checked. Provenance: StepSecurity Harden-Runner deployment guide. - ## Why this is structural, not a regex - - The check is per job, and both halves of it are indentation-sensitive: - - * **`runs-on` must belong to this job directly.** A reusable job - (`uses:` at job level) delegates its runtime to the source workflow, so a - sibling job's `runs-on` must not satisfy it. `direct_job_field?/2` - therefore compares against the job's own field indent rather than - matching `runs-on:` anywhere in the block. - - * **The hardener must be a real step.** `harden_runner_step?/1` walks - `steps:` by indent and accepts the reference only as a step entry or a - direct property of one. Two cases make a line-oriented match wrong in - *opposite* directions, so both are handled explicitly: - - - `uses: "step-security/harden-runner@..."` — quoted scalars are valid - YAML and still install the hardener. Missing them raises a **false - positive** against an already-hardened job. - - the same text inside a block scalar (`run: |`, `env: >`) is shell or - data, not a step. `block_scalar?/1` opens a skip region until the - indent closes, because treating it as a step raises a **false - negative** that suppresses a genuine finding. - - Severity: `:high` or `:warn`, as above. Action: `:report`. + Severity: `:high` or `:warn`, as above (`:warn` for an unreadable + workflow). Action: `:report`. """ def re001_missing_harden_runner(repo_path) do {deed_file, declared, deed_note} = @@ -294,10 +289,13 @@ defmodule Hypatia.Rules.ResearchExtensions do {:error, file, reason} -> {file, %{}, "the repo deed declares nothing (#{reason})"} end - jobs = - repo_path - |> workflow_files() - |> Enum.flat_map(fn path -> re001_jobs(path, Path.relative_to(path, repo_path)) end) + workflows = re001_workflows(repo_path) + jobs = for {:ok, rel, doc} <- workflows, job <- re001_jobs(rel, doc), do: job + + # A workflow that names secrets but cannot be read is reported. Its + # declarations cannot be checked, so they are not reported stale. + unreadable = for {:unreadable, rel, error, true} <- workflows, do: {rel, error} + unread = MapSet.new(for {:unreadable, rel, _, _} <- workflows, do: rel) job_findings = Enum.flat_map(jobs, fn job -> @@ -338,7 +336,7 @@ defmodule Hypatia.Rules.ResearchExtensions do [] end - dynamic ++ drift ++ enforcement + dynamic ++ drift ++ enforcement ++ re001_endpoint_findings(job, deed_file, decl) end end) @@ -348,97 +346,132 @@ defmodule Hypatia.Rules.ResearchExtensions do stale_findings = declared |> Map.keys() - |> Enum.reject(&MapSet.member?(live, &1)) + |> Enum.reject(fn {workflow, _} = key -> + MapSet.member?(live, key) or MapSet.member?(unread, workflow) + end) |> Enum.sort() |> Enum.map(&re001_stale(&1, deed_file)) - job_findings ++ stale_findings + Enum.map(unreadable, fn {rel, error} -> re001_unreadable(rel, error) end) ++ + job_findings ++ stale_findings + end + + # The workflows of a repo as RE001 reads them: the parsed model + # (Hypatia.Workflow, over kyq's KYAML reader). A workflow the reader refuses + # is {:unreadable, …}, with whether it names secrets at all. + defp re001_workflows(repo_path) do + for path <- workflow_files(repo_path) do + rel = Path.relative_to(path, repo_path) + bytes = File.read!(path) + + case Workflow.parse(bytes, rel) do + {:ok, workflow} -> {:ok, rel, workflow} + {:error, error} -> {:unreadable, rel, error, Regex.match?(~r/secrets/i, bytes)} + end + end + end + + # A workflow that names secrets but cannot be read is reported, not skipped: + # its jobs cannot be checked, and a silent skip would read as a pass. + defp re001_unreadable(rel, error) do + %{ + rule: "RE001", + file: rel, + severity: :warn, + line: error.line, + reason: + "#{rel} could not be read as KYAML (#{error.code} at line #{error.line}, column " <> + "#{error.column}: #{error.message}), so RE001 cannot check its secret-bearing jobs", + action: :report, + detail: %{ + exposures: [], + fix: + "Rewrite the construct the reader names in the KYAML subset (kyq " <> + "docs/KYAML_SPEC.adoc; standards YAML-POLICY). GitHub Actions refuses some of " <> + "these too, such as the `<<` merge key." + } + } end # The locally executed jobs of one workflow that read a real secret, with # what each holds and what it runs next to the credential. - defp re001_jobs(path, rel) do - # Comments are not runner configuration. Preserve physical line numbers - # so existing findings are not reported against a newly added line-1 header. - active_lines = path |> read_workflow() |> active_lines() + defp re001_jobs(_rel, nil), do: [] - untrusted_events = - active_lines - |> workflow_events() - |> Enum.filter(&(&1 in @re001_untrusted_events)) + defp re001_jobs(rel, %Workflow{} = workflow) do + untrusted_events = Enum.filter(workflow.triggers, &(&1 in @re001_untrusted_events)) # Secrets in the workflow's top-level `env:` are inherited by every job, # so each job reads them too, and a declaration must list them. - workflow_env = workflow_env_lines(active_lines) - workflow_refs = secret_refs(workflow_env) - - active_lines - |> workflow_job_lines() - # Reusable jobs delegate their runtime to the source workflow. A sibling's - # runner or hardener cannot establish this job's execution policy. - |> Enum.filter(&direct_job_field?(&1, "runs-on")) - |> Enum.flat_map(fn [{header, _} | _] = job_lines -> - refs = - for {name, n} <- secret_refs(job_lines) ++ workflow_refs, - name not in @re001_ambient_secrets, - do: {name, n} - - case refs do - [] -> - [] + workflow_refs = node_secret_refs(workflow.env) + workflow_env_credentials = env_credentials(workflow.env) + + for job <- workflow.jobs, + # Reusable jobs delegate their runtime to the source workflow: only a + # job's own `runs-on` makes it local. + job.runs_on != nil, + refs = + Enum.reject( + node_secret_refs(job.node) ++ workflow_refs, + &(elem(&1, 0) in @re001_ambient_secrets) + ), + refs != [] do + steps = job.steps + + # A credential in the job's or the workflow's `env:` is in every step's + # environment, unless the step sets the same variable itself. + env_credentials = env_credentials(job.env) ++ workflow_env_credentials + + job_untrusted_events = + case job_event_gate(job) do + nil -> untrusted_events + gated -> Enum.filter(untrusted_events, &(&1 in gated)) + end - [{_, first_line} | _] -> - # A line that reads a real secret, by name or by a computed key. - credential_lines = MapSet.new(refs, &elem(&1, 1)) - credential? = fn {_, n} -> MapSet.member?(credential_lines, n) end - steps = job_steps(job_lines) - # A credential in the job's or the workflow's `env:` is in every step's - # environment. - job_env_credentials = Enum.filter(job_env_lines(job_lines) ++ workflow_env, credential?) - - job_untrusted_events = - case job_event_gate(job_lines) do - nil -> untrusted_events - gated -> Enum.filter(untrusted_events, &(&1 in gated)) - end + # A step that both holds the credential and runs fetched or head code + # hands the credential straight to that code. + shared_line = + Enum.find_value(steps, fn step -> + step_refs = + Enum.reject(node_secret_refs(step.node), &(elem(&1, 0) in @re001_ambient_secrets)) - # A step that both holds the credential and runs fetched or head code - # hands the credential straight to that code. - shared_line = - Enum.find_value(steps, fn step -> - credential = - Enum.find(step, credential?) || - Enum.find(job_env_credentials, &(not overrides_env?(step, &1))) + step_env = step.env |> Workflow.entries() |> Enum.map(& &1.key.value) - credential && step_code_exposures(step) != [] && elem(credential, 1) - end) + credential = + List.first(step_refs) || + Enum.find(env_credentials, fn {name, _} -> name not in step_env end) - [ - %{ - workflow: rel, - id: job_id(header), - line: shared_line || first_line, - secrets: MapSet.new(for {name, _} <- refs, is_binary(name), do: name), - dynamic_line: Enum.find_value(refs, fn {name, n} -> name == :dynamic && n end), - hardened?: harden_runner_step?(job_lines), - harden_policy: harden_runner_policy(steps), - exposures: re001_exposures(steps, job_untrusted_events), - shared?: shared_line != nil - } - ] - end - end) + credential && step_code_exposures(step) != [] && elem(credential, 1) + end) + + harden_step = Enum.find(steps, &harden_runner_step?/1) + + %{ + workflow: rel, + id: job.id, + line: shared_line || elem(hd(refs), 1), + secrets: MapSet.new(for {name, _} <- refs, is_binary(name), do: name), + dynamic_line: Enum.find_value(refs, fn {name, n} -> name == :dynamic && n end), + hardened?: harden_step != nil, + harden_policy: harden_step && harden_runner_policy(harden_step), + allowed_endpoints: harden_step && harden_runner_allowed(harden_step), + named_hosts: Enum.flat_map(steps, &named_hosts/1), + exposures: re001_exposures(steps, job_untrusted_events), + shared?: shared_line != nil + } + end end - # Every secret a job reads inside ${{ … }}, as {NAME, line}: the property - # form secrets.NAME and the index form secrets['NAME'] / secrets["NAME"], - # anywhere in the expression (${{ vars.X || secrets.Y }} reads Y). GitHub - # matches secret names without regard to case and stores them uppercase; the - # deed declares that stored form, so names are uppercased here. + # Every secret a node reads inside ${{ … }}, as {NAME, line}, in document + # order: the property form secrets.NAME and the index form secrets['NAME'] / + # secrets["NAME"], anywhere in the expression (${{ vars.X || secrets.Y }} + # reads Y). GitHub matches secret names without regard to case and stores + # them uppercase; the deed declares that stored form, so names are + # uppercased here. # - # The job is scanned as one text, not line by line: a folded YAML scalar can - # split one expression across physical lines, and GitHub evaluates it whole. - # A valid workflow has no unclosed ${{, so every match is a real expression. + # Each string value is read whole, as GitHub evaluates it, so an expression + # a folded block scalar spreads over lines is one expression. A read is + # reported at its own source line: a block scalar maps each of its lines, and + # what is read through an alias is reported at the alias. # # Both scans step over string literals ('…', with '' for a quote) whole, so # text inside one is never read: an expression ends at the first }} outside @@ -452,19 +485,11 @@ defmodule Hypatia.Rules.ResearchExtensions do # {:dynamic, line}, which no declaration can cover. @expression ~r/\$\{\{((?:'(?:[^']|'')*'|[^'}]|\}(?!\}))*)\}\}/ @secret_ref ~r/(? {{at, n}, at + byte_size(line) + 1} end) + defp node_secret_refs(nil), do: [] - line_of = fn at -> - {_, n} = starts |> Enum.take_while(fn {start, _} -> start <= at end) |> List.last() - n - end - - for [_, {body_at, body_len}] <- Regex.scan(@expression, text, return: :index), + defp node_secret_refs(node) do + for {text, line_of} <- Workflow.strings(node), + [_, {body_at, body_len}] <- Regex.scan(@expression, text, return: :index), [{m_at, _} | groups] <- Regex.scan(@secret_ref, binary_part(text, body_at, body_len), return: :index), # A match that opens with a quote is a string literal, read past. @@ -476,11 +501,82 @@ defmodule Hypatia.Rules.ResearchExtensions do end end - defp job_id(header) do - [_, id] = Regex.run(~r/^\s+("[^"]+"|'[^']+'|[A-Za-z0-9_-]+):/, header) - String.trim(id, "\"") |> String.trim("'") + # The `env:` variables of a workflow or job that hold a real secret, as + # {NAME, line of the read}. + defp env_credentials(env) do + for %{key: key, value: value} <- Workflow.entries(env), + {name, line} <- node_secret_refs(value), + name not in @re001_ambient_secrets, + do: {key.value, line} + end + + # The events a job-level `if:` restricts the job to, when the condition is + # nothing but `github.event_name == ''` tests joined by `||`. + # Anything more complex is not interpreted, and the job is judged on all the + # workflow's events. + defp job_event_gate(job) do + test = ~S"github\.event_name\s*==\s*'([a-z_]+)'" + + with condition when is_binary(condition) <- job.if, + condition = condition |> String.trim() |> String.replace(~r/^\$\{\{\s*|\s*\}\}$/, ""), + true <- Regex.match?(~r/^\s*#{test}(?:\s*\|\|\s*#{test})*\s*$/, condition) do + ~r/github\.event_name\s*==\s*'([a-z_]+)'/ + |> Regex.scan(condition, capture: :all_but_first) + |> List.flatten() + else + _ -> nil + end end + defp re001_exposures(steps, untrusted_events) do + code = Enum.flat_map(steps, &step_code_exposures/1) + + [ + untrusted_events != [] && + "an untrusted-input trigger (#{Enum.join(untrusted_events, ", ")})", + :head in code && "a pull-request or triggering-run head checkout", + :fetched in code && "fetched code (a piped installer or a dependency install/build)" + ] + |> Enum.filter(&is_binary/1) + end + + # What a step executes that the job cannot vouch for: `:head` when it checks + # out or fetches the head of a pull request or triggering run, `:fetched` + # when its `run:` script pipes a download into a shell or installs or builds + # dependencies. Only executable content counts: an `env:` value or a comment + # that mentions `npm ci` runs nothing. + defp step_code_exposures(step) do + # Shell comments removed; a folded command keeps its line breaks or spaces + # as YAML gives them, and the patterns' `\s+` spans either. + run = + (step.run || "") + |> String.split("\n") + |> Enum.map_join("\n", &String.replace(&1, ~r/(?:^|\s)#.*$/, "")) + + # A `ref:`/`repository:` input fetches the head only on a checkout; the + # same input on a reporting action merely names it. + checkout? = String.starts_with?(step.uses || "", "actions/checkout@") + + head? = + (checkout? and + Enum.any?(["ref", "repository"], fn input -> + Regex.match?(@re001_head_ref, Workflow.input(step, input) || "") + end)) or Regex.match?(@re001_git_head_fetch, run) + + [head? && :head, Regex.match?(@re001_fetched_code, run) && :fetched] + |> Enum.filter(& &1) + end + + # GitHub resolves an action's owner/repo without regard to case + # (Step-Security/Harden-Runner@v2 installs the same action). + defp harden_runner_step?(%Step{uses: uses}) do + Regex.match?(~r/\A(?i:step-security\/harden-runner)@/, uses || "") + end + + # The egress-policy input of a harden-runner step; harden-runner defaults to + # audit when none is set. + defp harden_runner_policy(step), do: Workflow.input(step, "egress-policy") || "audit" + # What the job runs next to its credential, for a finding's reason. defp exposure_note(%{exposures: []}), do: "" @@ -620,373 +716,241 @@ defmodule Hypatia.Rules.ResearchExtensions do } end - defp re001_stale({workflow, id}, deed_file) do - %{ - rule: "RE001", - file: deed_file, - severity: :warn, - reason: - "#{deed_file} declares egress for job `#{id}` in #{workflow}, but no locally run " <> - "job there reads a real secret — the attestation is stale", - action: :report, - detail: %{ - fix: - "Remove (job :workflow \"#{workflow}\" :job \"#{id}\") from the `(egress …)` clause, " <> - "or correct its :workflow / :job." - } - } + # ─── RE001: declared endpoints against the workflow ───────────────── + # + # A declaration's :endpoints are compared with what the workflow itself + # shows, never with what it might reach at run time: + # + # * every host outside GitHub that a step names literally (a URL, or a + # `git@host:` remote) must be covered by a declared endpoint; + # * when the job's harden-runner step lists `allowed-endpoints`, the + # hosts outside GitHub on that list and the declared literal endpoints + # must agree: the hardener enforces one list, the deed attests to it. + # + # An endpoint held in a secret or variable (`secret:`, `var:`) covers no + # literal host: a host written in the workflow is declared as itself. + + # GitHub's own endpoints, which :endpoints leaves out (ADR-009). + @github_hosts ~r/\A(?:github\.com|[a-z0-9.-]+\.github\.com|[a-z0-9.-]*githubusercontent\.com|ghcr\.io|[a-z0-9.-]+\.githubassets\.com|github\.io|[a-z0-9.-]+\.github\.io)\z/ + + @url_host ~r<\b(https?|wss?|ssh|git|ftps?)://(?:[^@/\s"'`]+@)?([A-Za-z0-9](?:[A-Za-z0-9.-]*[A-Za-z0-9])?\.[A-Za-z]{2,})(?::(\d{1,5}))?> + @scp_host ~r/(? 80, + "ws" => 80, + "https" => 443, + "wss" => 443, + "ssh" => 22, + "git" => 9418, + "ftp" => 21, + "ftps" => 990 + } + + # The hosts outside GitHub one step names literally, as {host, port, line}. + defp named_hosts(step) do + for {text, line_of} <- Workflow.strings(step.node), + {host, port, at} <- url_hosts(text) ++ scp_hosts(text), + not in_shell_comment?(text, at), + host = String.downcase(host), + not Regex.match?(@github_hosts, host), + do: {host, port, line_of.(at)} end - defp quoted_list(names), do: names |> Enum.sort() |> Enum.map_join(" ", &"\"#{&1}\"") - - defp re001_exposures(steps, untrusted_events) do - code = Enum.flat_map(steps, &step_code_exposures/1) + # Is offset `at` inside a `#` comment: after a `#` that starts the line or + # follows a blank? (A URL fragment, `/#x`, is not one.) + defp in_shell_comment?(text, at) do + line_start = + case :binary.matches(binary_part(text, 0, at), "\n") do + [] -> 0 + matches -> matches |> List.last() |> elem(0) |> Kernel.+(1) + end - [ - untrusted_events != [] && - "an untrusted-input trigger (#{Enum.join(untrusted_events, ", ")})", - :head in code && "a pull-request or triggering-run head checkout", - :fetched in code && "fetched code (a piped installer or a dependency install/build)" - ] - |> Enum.filter(&is_binary/1) + Regex.match?(~r/(?:\A|\s)#/, binary_part(text, line_start, at - line_start)) end - # What a step executes that the job cannot vouch for: `:head` when it checks - # out or fetches the head of a pull request or triggering run, `:fetched` - # when its `run:` script pipes a download into a shell or installs or builds - # dependencies. Only executable content counts: an `env:` value or a YAML - # comment that mentions `npm ci` runs nothing. - defp step_code_exposures(step) do - run_lines = step_run_lines(step) - # Joined with newlines so a folded `run: >-` command split across lines - # still matches: the patterns' `\s+` spans the line break. - run = Enum.join(run_lines, "\n") - - # A `ref:`/`repository:` input fetches the head only on a checkout; the - # same input on a reporting action merely names it. - checkout? = Enum.any?(step, fn {line, _} -> Regex.match?(@re001_checkout_action, line) end) - - head? = - (checkout? and - Enum.any?(step, fn {line, _} -> - Regex.match?(@re001_checkout_key, line) and Regex.match?(@re001_head_ref, line) - end)) or Regex.match?(@re001_git_head_fetch, run) - - [head? && :head, Regex.match?(@re001_fetched_code, run) && :fetched] - |> Enum.filter(& &1) + defp url_hosts(text) do + for [{at, _}, {s, sl}, {h, hl}, port] <- + Regex.scan(@url_host, text, return: :index, capture: :all) |> Enum.map(&pad_port/1) do + scheme = String.downcase(binary_part(text, s, sl)) + port = if port, do: String.to_integer(binary_part(text, elem(port, 0), elem(port, 1))) + {binary_part(text, h, hl), port || @default_port[scheme], at} + end end - # The script of a step's `run:`, inline or as a block scalar, with comments - # removed (YAML and shell agree that `#` after whitespace starts one). - defp step_run_lines(step) do - key_column = step_key_column(step) - - # Only the step's own `run:` property: an `env:` variable named `run` is a - # nested key, deeper than the step's properties. - case Enum.split_while(step, fn {line, _} -> - case Regex.run(~r/^(\s*(?:-\s+)?)(?:run|"run"|'run')\s*:/, line) do - [_, prefix] -> String.length(prefix) != key_column - _ -> true - end - end) do - {_, []} -> - [] - - {_, [{run_line, _} | rest]} -> - [prefix, value] = - Regex.run(~r/^(\s*(?:-\s+)?)(?:run|"run"|'run')\s*:\s*(.*)$/, run_line, - capture: :all_but_first - ) - - key_column = String.length(prefix) - - # A block scalar, its header after any anchor (`run: &script |`). - body = - if Regex.match?(~r/^(?:&[A-Za-z0-9_-]+\s+)?[>|][0-9+-]*\s*(?:#.*)?$/, value) do - rest - |> Enum.take_while(fn {line, _} -> - String.trim(line) == "" or indent_of(line) > key_column - end) - |> Enum.map(&elem(&1, 0)) - else - [value] - end + defp pad_port([all, scheme, host]), do: [all, scheme, host, nil] + defp pad_port([all, scheme, host, {_, 0}]), do: [all, scheme, host, nil] + defp pad_port(match), do: match - Enum.map(body, &String.replace(&1, ~r/(?:^|\s)#.*$/, "")) - end + defp scp_hosts(text) do + for [{at, _}, {h, hl}] <- Regex.scan(@scp_host, text, return: :index), + do: {binary_part(text, h, hl), 22, at} end - # True when the step sets the same variable as the job-level `env:` line, - # so the step-level value replaces the inherited credential. - defp overrides_env?(step, {job_line, _}) do - case Regex.run(~r/^\s*([A-Za-z_][A-Za-z0-9_]*)\s*:/, job_line) do - [_, key] -> - Enum.any?(step, fn {line, _} -> Regex.match?(~r/^\s*#{key}\s*:/, line) end) + # The literal entries of a harden-runner step's `allowed-endpoints` input + # (`host:port`, separated by spaces, newlines or commas); nil when the step + # sets none. An entry written with an expression + # (`${{ secrets.SMTP_HOST }}:${{ secrets.SMTP_PORT }}`) names its host only + # at run time, as a declared `secret:` or `var:` endpoint does, so it is + # not a literal entry. An expression is one unit however it is spaced. + defp harden_runner_allowed(step) do + case Workflow.input(step, "allowed-endpoints") do + nil -> + nil - _ -> - false + text -> + text + |> String.replace(@expression, "\0") + |> String.split(~r/[\s,]+/, trim: true) + |> Enum.reject(&String.contains?(&1, "\0")) end end - # The workflow's top-level `env:` (key at column 0) with its indented body. - # Every job, and every step in it, inherits these variables. - defp workflow_env_lines(active_lines) do - case Enum.drop_while(active_lines, fn {line, _} -> - not (indent_of(line) == 0 and key_line?(line, "env")) - end) do - [env_line | rest] -> - body = Enum.take_while(rest, fn {line, _} -> line == "" or indent_of(line) > 0 end) - [env_line | body] - - [] -> - [] + # A literal endpoint as {host pattern, port or nil}: `host` or + # `host:digits`. Anything else (secret:, var:, an expression) is nil. + defp literal_endpoint(endpoint) do + case Regex.run(~r/\A([a-z0-9*][a-z0-9.*-]*)(?::(\d{1,5}))?\z/, String.downcase(endpoint)) do + [_, host] -> {host, nil} + [_, host, port] -> {host, String.to_integer(port)} + nil -> nil end end - # The lines under the job's own `env:` key. - defp job_env_lines(job_lines) do - with field_indent when is_integer(field_indent) <- job_field_indent(job_lines), - index when is_integer(index) <- - Enum.find_index(job_lines, fn {line, _} -> - indent_of(line) == field_indent and key_line?(line, "env") - end) do - job_lines - |> Enum.drop(index) - |> then(fn [env_line | rest] -> - [env_line | Enum.take_while(rest, fn {line, _} -> indent_of(line) > field_indent end)] - end) - else - _ -> [] - end - end + # Does a declared {pattern, port} cover a host and port? `*.x` covers the + # subdomains of x (as harden-runner reads it), not x itself; an endpoint + # without a port covers every port. + defp covers?({pattern, want}, host, port) do + host_ok = + case pattern do + "*." <> suffix -> String.ends_with?(host, "." <> suffix) + _ -> pattern == host + end - # The events a job-level `if:` restricts the job to, when the condition is - # nothing but `github.event_name == ''` tests joined by `||`. - # Anything more complex is not interpreted, and the job is judged on all the - # workflow's events. - defp job_event_gate(job_lines) do - with field_indent when is_integer(field_indent) <- job_field_indent(job_lines), - {line, _} <- - Enum.find(job_lines, fn {line, _} -> - indent_of(line) == field_indent and key_line?(line, "if") - end), - [_, condition] <- Regex.run(~r/^\s*["']?if["']?\s*:\s*(.*?)\s*$/, line), - condition = condition |> String.replace(~r/^\$\{\{\s*|\s*\}\}$/, ""), - test = ~S"github\.event_name\s*==\s*'([a-z_]+)'", - true <- Regex.match?(~r/^\s*#{test}(?:\s*\|\|\s*#{test})*\s*$/, condition) do - ~r/github\.event_name\s*==\s*'([a-z_]+)'/ - |> Regex.scan(condition, capture: :all_but_first) - |> List.flatten() - else - _ -> nil - end + host_ok and (want == nil or port == nil or want == port) end - # The event names under the workflow's top-level `on:`, in any of its forms: - # `on: push`, `on: [push, issues]`, or a block of event keys or list items. - defp workflow_events(lines) do - case Enum.split_while(lines, fn {line, _} -> - not Regex.match?(~r/^["']?on["']?:/, line) - end) do - {_, []} -> - [] + defp re001_endpoint_findings(job, deed_file, decl) do + declared = decl.endpoints |> Enum.map(&literal_endpoint/1) |> Enum.reject(&is_nil/1) - {_, [{on_line, _} | rest]} -> - inline = - on_line - |> String.split(":", parts: 2) - |> List.last() - |> String.replace(~r/\s+#.*$/, "") - # `on: &events` anchors the block mapping that follows. - |> String.replace(~r/^\s*&[A-Za-z0-9_-]+/, "") - |> String.trim() - - if inline != "" do - # A flow collection may continue past the `on:` line: read on until - # its brackets balance. - rest - |> Enum.map(&elem(&1, 0)) - |> Enum.reduce_while(inline, fn line, acc -> - if nesting_at(acc, byte_size(acc)) > 0, - do: {:cont, acc <> " " <> String.trim(line)}, - else: {:halt, acc} - end) - |> inline_events() - else - block = - Enum.take_while(rest, fn {line, _} -> - String.trim(line) == "" or indent_of(line) > 0 - end) - |> Enum.reject(fn {line, _} -> String.trim(line) == "" end) - - event_indent = - block |> Enum.map(fn {line, _} -> indent_of(line) end) |> Enum.min(fn -> nil end) - - block - |> Enum.filter(fn {line, _} -> indent_of(line) == event_indent end) - |> Enum.flat_map(fn {line, _} -> - case Regex.run(~r/^\s*(?:-\s+)?["']?([A-Za-z_]+)["']?\s*:?/, line) do - [_, event] -> [event] - _ -> [] - end - end) - end - end - end + uncovered = + job.named_hosts + |> Enum.reject(fn {host, port, _} -> Enum.any?(declared, &covers?(&1, host, port)) end) + |> Enum.uniq_by(fn {host, port, _} -> {host, port} end) - # `on: {push: {paths: [issues/**]}}` names one event, push: only the map's - # top-level keys are events. A scalar or list names each of its words. - defp inline_events("{" <> _ = map) do - ~r/["']?([A-Za-z_]+)["']?\s*:/ - |> Regex.scan(map, return: :index) - |> Enum.flat_map(fn [{start, _}, {from, len}] -> - if nesting_at(map, start) == 1, do: [binary_part(map, from, len)], else: [] - end) - end + named = + if uncovered == [], + do: [], + else: [re001_unnamed_endpoints(job, deed_file, uncovered)] - defp inline_events(scalar_or_list) do - ~r/[A-Za-z_]+/ |> Regex.scan(scalar_or_list) |> List.flatten() + named ++ allowed_endpoint_findings(job, deed_file, declared) end - defp harden_runner_step?(job_lines) do - with field_indent when is_integer(field_indent) <- job_field_indent(job_lines), - step_lines when step_lines != [] <- lines_in_steps(job_lines, field_indent), - step_indent when is_integer(step_indent) <- step_indent(step_lines, field_indent) do - case Enum.reduce_while(step_lines, {false, nil, nil}, fn {line, _}, - {in_step, property_indent, - scalar_indent} -> - indent = indent_of(line) - - cond do - scalar_indent && indent > scalar_indent -> - {:cont, {in_step, property_indent, scalar_indent}} - - indent == step_indent and Regex.match?(~r/^\s*-\s+/, line) -> - if harden_runner_uses?(line) do - {:halt, true} - else - {:cont, {true, nil, block_scalar?(line) && indent}} - end - - in_step and indent > step_indent -> - direct_property? = is_nil(property_indent) or indent == property_indent - property_indent = property_indent || indent - - if direct_property? and harden_runner_uses?(line) do - {:halt, true} - else - {:cont, {in_step, property_indent, block_scalar?(line) && indent}} - end - - true -> - {:cont, {in_step, property_indent, nil}} - end - end) do - true -> true - _ -> false - end - else - _ -> false - end - end + defp allowed_endpoint_findings(%{allowed_endpoints: nil}, _deed_file, _declared), do: [] - # The egress-policy input of the job's harden-runner step; harden-runner - # defaults to audit when none is set. nil without the step. - defp harden_runner_policy(steps) do - case Enum.find(steps, fn step -> - Enum.any?(step, fn {line, _} -> harden_runner_uses?(line) end) - end) do - nil -> nil - step -> step |> step_inputs() |> Map.get("egress-policy", "audit") - end - end + defp allowed_endpoint_findings(job, deed_file, declared) do + allowed = + job.allowed_endpoints + |> Enum.map(&literal_endpoint/1) + |> Enum.reject(fn endpoint -> + endpoint == nil or Regex.match?(@github_hosts, elem(endpoint, 0)) + end) - # One step's `with:` inputs as %{name => value}, from a block mapping under - # the key or a flow mapping on its line. A YAML comment sets no input, so - # comments are stripped first: `uses: …@v2 # egress-policy: block` leaves - # the policy at its default. - @with_key ~r/^(\s*(?:-\s+)?)(?:with|"with"|'with')\s*:(?:\s(.*))?$/ - @block_input ~r/^\s*["']?([A-Za-z0-9_-]+)["']?\s*:(?:\s+(.*))?$/ - @flow_input ~r/[{,]\s*["']?([A-Za-z0-9_-]+)["']?\s*:\s*("(?:[^"\\]|\\.)*"|'(?:[^']|'')*'|[^,}]*)/ - defp step_inputs(step) do - lines = Enum.map(step, fn {line, _} -> strip_yaml_comment(line) end) - - case Enum.find_index(lines, &Regex.match?(@with_key, &1)) do - nil -> - %{} - - index -> - [with_line | rest] = Enum.drop(lines, index) - [lead, inline] = with_key_parts(with_line) - - if String.starts_with?(inline, "{") do - # A flow mapping may continue past the `with:` line. - rest - |> Enum.reduce_while(inline, fn line, acc -> - if nesting_at(acc, byte_size(acc)) > 0, - do: {:cont, acc <> " " <> String.trim(line)}, - else: {:halt, acc} - end) - |> then(&Regex.scan(@flow_input, &1, capture: :all_but_first)) - |> Map.new(fn [name, value] -> {name, scalar_value(value)} end) - else - column = String.length(lead) - body = Enum.take_while(rest, &(String.trim(&1) == "" or indent_of(&1) > column)) - - child_indent = - body - |> Enum.reject(&(String.trim(&1) == "")) - |> Enum.map(&indent_of/1) - |> Enum.min(fn -> nil end) - - for line <- body, - indent_of(line) == child_indent, - [_ | captures] <- [Regex.run(@block_input, line)], - into: %{} do - case captures do - [name, value] -> {name, scalar_value(value)} - [name] -> {name, ""} - end - end - end - end - end + # What the hardener lets out must be declared. A declared literal host + # must be let out, or block mode stops the job; a declared wildcard is a + # wider claim than any list it covers, and is not held to one. GitHub's + # own hosts are outside the comparison on both sides: a deed may list + # them, and the hardener's list is not held to them. + undeclared = Enum.reject(allowed, fn {h, p} -> Enum.any?(declared, &covers?(&1, h, p)) end) + + blocked = + Enum.reject(declared, fn {h, p} -> + String.starts_with?(h, "*.") or Regex.match?(@github_hosts, h) or + Enum.any?(allowed, &covers?(&1, h, p)) + end) - defp with_key_parts(line) do - case Regex.run(@with_key, line) do - [_, lead, inline] -> [lead, String.trim(inline)] - [_, lead] -> [lead, ""] + if undeclared == [] and blocked == [] do + [] + else + [re001_allowed_mismatch(job, deed_file, undeclared, blocked)] end end - # A plain or quoted scalar's text. - defp scalar_value(value) do - value = String.trim(value) + defp endpoint_text({host, nil}), do: "\"#{host}\"" + defp endpoint_text({host, port}), do: "\"#{host}:#{port}\"" - cond do - Regex.match?(~r/^"(?:[^"\\]|\\.)*"$/, value) -> - String.slice(value, 1..-2//1) + defp re001_unnamed_endpoints(job, deed_file, uncovered) do + [{_, _, line} | _] = uncovered + names = Enum.map_join(uncovered, " ", fn {h, p, _} -> endpoint_text({h, p}) end) - Regex.match?(~r/^'(?:[^']|'')*'$/, value) -> - value |> String.slice(1..-2//1) |> String.replace("''", "'") + %{ + rule: "RE001", + file: job.workflow, + severity: :warn, + line: line, + reason: + "job `#{job.id}` in #{job.workflow} names #{names} literally, but its egress " <> + "declaration in #{deed_file} does not list it", + action: :report, + detail: %{ + exposures: job.exposures, + fix: + "Add #{names} to :endpoints of (job :workflow \"#{job.workflow}\" :job \"#{job.id}\") " <> + "in #{deed_file}, or stop the job reaching it. An endpoint held in a secret " <> + "or variable does not cover a host written in the workflow." + } + } + end - true -> - value - end + defp re001_allowed_mismatch(job, deed_file, undeclared, blocked) do + parts = + Enum.reject( + [ + if(undeclared != [], + do: "lets out undeclared #{Enum.map_join(undeclared, " ", &endpoint_text/1)}" + ), + if(blocked != [], + do: "does not allow declared #{Enum.map_join(blocked, " ", &endpoint_text/1)}" + ) + ], + &is_nil/1 + ) + + %{ + rule: "RE001", + file: job.workflow, + severity: :warn, + line: job.line, + reason: + "job `#{job.id}` in #{job.workflow}: harden-runner's allowed-endpoints " <> + Enum.join(parts, "; ") <> " (egress declaration in #{deed_file})", + action: :report, + detail: %{ + exposures: job.exposures, + fix: + "Make the hosts outside GitHub in the harden-runner step's allowed-endpoints and " <> + ":endpoints of (job :workflow \"#{job.workflow}\" :job \"#{job.id}\") in " <> + "#{deed_file} name the same endpoints." + } + } end - # GitHub resolves an action's owner/repo without regard to case - # (Step-Security/Harden-Runner@v2 installs the same action); the `uses:` - # key itself is case-sensitive YAML. - defp harden_runner_uses?(line) do - Regex.match?( - ~r/^\s*(?:-\s+)?(?:uses|"uses"|'uses')\s*:\s*["']?(?i:step-security\/harden-runner)@/, - line - ) + defp re001_stale({workflow, id}, deed_file) do + %{ + rule: "RE001", + file: deed_file, + severity: :warn, + reason: + "#{deed_file} declares egress for job `#{id}` in #{workflow}, but no locally run " <> + "job there reads a real secret — the attestation is stale", + action: :report, + detail: %{ + fix: + "Remove (job :workflow \"#{workflow}\" :job \"#{id}\") from the `(egress …)` clause, " <> + "or correct its :workflow / :job." + } + } end - defp block_scalar?(line), - do: Regex.match?(~r/:\s*(?:&[A-Za-z0-9_-]+\s+)?[>|][0-9+-]*\s*(?:#.*)?$/, line) + defp quoted_list(names), do: names |> Enum.sort() |> Enum.map_join(" ", &"\"#{&1}\"") # ─── RE002: Harden-Runner in audit-only mode ───────────────────────── @@ -997,45 +961,49 @@ defmodule Hypatia.Rules.ResearchExtensions do becomes a finding when it persists on a workflow that touches protected branches (or runs on `push` to default). + Read from the parsed workflow (`Hypatia.Workflow`), as RE001 is: a hardener + is a real step whose `uses:` names `step-security/harden-runner` (any + case, as RE001 accepts it), its policy is that step's own + `with: egress-policy`, and a step with no policy runs harden-runner's + default, `audit`. The trigger is a `push` or `release` event in the + workflow's `on:`. A workflow that cannot be read is RE001's to report. + Severity: `:high`. Action: `:report`. """ def re002_harden_runner_audit_mode(repo_path) do - repo_path - |> workflow_files() - |> Enum.flat_map(fn path -> - content = File.read!(path) - rel = Path.relative_to(path, repo_path) - - installs_harden? = Regex.match?(~r/uses:\s*step-security\/harden-runner/, content) + for {:ok, rel, %Workflow{} = workflow} <- re001_workflows(repo_path), + Enum.any?(workflow.triggers, &(&1 in ["push", "release"])), + audit = audit_hardeners(workflow), + audit != [] do + defaulted? = Enum.all?(audit, &(&1 == :default)) - audit_mode? = Regex.match?(~r/egress-policy:\s*audit\b/, content) - - protected_branch_trigger? = - Regex.match?(~r/^\s*on:\s*push\b/m, content) or - Regex.match?(~r/^\s+push:/m, content) or - Regex.match?(~r/^\s+release:/m, content) + %{ + rule: "RE002", + file: rel, + severity: :high, + reason: + "workflow #{rel} runs harden-runner in `egress-policy: audit`" <> + if(defaulted?, do: " (its default: no egress-policy is set)", else: "") <> + " — telemetry-only, never blocks; on a protected-branch trigger this is not containment", + action: :report, + detail: %{ + fix: + "Set `egress-policy: block` on the harden-runner step once " <> + "the allow-list is stable. Keep `audit` only for first-rollout windows." + } + } + end + end - if installs_harden? and audit_mode? and protected_branch_trigger? do - [ - %{ - rule: "RE002", - file: rel, - severity: :high, - reason: - "workflow #{rel} runs harden-runner in `egress-policy: audit` — " <> - "telemetry-only, never blocks; on a protected-branch trigger this is not containment", - action: :report, - detail: %{ - fix: - "Switch `egress-policy: audit` to `egress-policy: block` once " <> - "the allow-list is stable. Keep `audit` only for first-rollout windows." - } - } - ] - else - [] - end - end) + # The audit-mode harden-runner steps of a workflow's jobs: `:explicit` for + # `egress-policy: audit`, `:default` for a step that sets no policy. + defp audit_hardeners(%Workflow{jobs: jobs}) do + for job <- jobs, + step <- job.steps, + harden_runner_step?(step), + harden_runner_policy(step) == "audit" do + if Workflow.input(step, "egress-policy"), do: :explicit, else: :default + end end # ─── RE003: cache key interpolates attacker-controlled input ───────── diff --git a/test/deed_test.exs b/test/deed_test.exs index 2484bb10..8288c815 100644 --- a/test/deed_test.exs +++ b/test/deed_test.exs @@ -219,10 +219,12 @@ defmodule Hypatia.DeedTest do workflow: ".github/workflows/push-email-notify.yml", job: "notify", secrets: MapSet.new(~w(SMTP_HOST SMTP_PORT SMTP_USER SMTP_PASS)), + endpoints: ["secret:SMTP_HOST"], enforcement: "none" } assert sonar.secrets == MapSet.new(["SONAR_TOKEN"]) + assert sonar.endpoints == ["sonarcloud.io", "*.sonarcloud.io:443", "var:SONAR_HOST"] end end diff --git a/test/research_extensions_equivalence_test.exs b/test/research_extensions_equivalence_test.exs new file mode 100644 index 00000000..33ce9ef3 --- /dev/null +++ b/test/research_extensions_equivalence_test.exs @@ -0,0 +1,229 @@ +# SPDX-License-Identifier: MPL-2.0 +defmodule Hypatia.Rules.ResearchExtensionsEquivalenceTest do + @moduledoc """ + RE001 and RE002 read the parsed workflow (#971), so they must not depend on + how a workflow is written. Each seeded random workflow is rendered four + ways (block YAML with plain scalars, KYAML flow as `yq -o kyaml` writes it, + block with every key and value single-quoted, and block with each `run:` as + a literal block scalar), and every rendering must give the same findings, + apart from line numbers. + + A failure names the seed and the case, so it reproduces with + `HYPATIA_EQUIV_SEED=`. + """ + use ExUnit.Case, async: true + + alias Hypatia.Rules.ResearchExtensions + + @cases 150 + @sha "1234567890abcdef1234567890abcdef12345678" + + setup_all do + seed = + case System.get_env("HYPATIA_EQUIV_SEED") do + nil -> 20_261_104 + text -> String.to_integer(text) + end + + {:ok, seed: seed} + end + + test "RE001 and RE002 findings do not depend on how a workflow is written", %{seed: seed} do + :rand.seed(:exsss, {seed, seed + 1, seed + 2}) + + for n <- 1..@cases do + workflow = gen_workflow() + + [first | rest] = + for style <- [:block, :flow, :quoted, :literal] do + {style, findings(render(workflow, style))} + end + + {_, expected} = first + + for {style, got} <- rest do + assert got == expected, """ + seed #{seed}, case #{n}: #{style} differs from block + block: + #{render(workflow, :block)} + #{style}: + #{render(workflow, style)} + """ + end + end + end + + test "the generator reaches every outcome the harness is meant to compare", %{seed: seed} do + :rand.seed(:exsss, {seed, seed + 1, seed + 2}) + + rules = + for _ <- 1..@cases, f <- findings(render(gen_workflow(), :block)), into: MapSet.new() do + {f.rule, f.severity} + end + + assert {"RE001", :high} in rules or {"RE001", :critical} in rules + assert {"RE002", :high} in rules + end + + # ─── findings, line-free ──────────────────────────────────────────── + + defp findings(yaml) do + dir = Path.join(System.tmp_dir!(), "hyp-equiv-#{System.unique_integer([:positive])}") + File.mkdir_p!(Path.join(dir, ".github/workflows")) + File.write!(Path.join(dir, ".github/workflows/w.yml"), yaml) + + try do + (ResearchExtensions.re001_missing_harden_runner(dir) ++ + ResearchExtensions.re002_harden_runner_audit_mode(dir)) + |> Enum.map(&strip_lines/1) + |> Enum.sort() + after + File.rm_rf!(dir) + end + end + + defp strip_lines(%{} = map) do + for {k, v} <- map, + not (is_atom(k) and String.contains?(Atom.to_string(k), "line")), + into: %{} do + {k, strip_lines(v)} + end + end + + defp strip_lines(list) when is_list(list), do: Enum.map(list, &strip_lines/1) + defp strip_lines(text) when is_binary(text), do: Regex.replace(~r/\bline \d+|:\d+\b/, text, "") + defp strip_lines(other), do: other + + # ─── generator ───────────────────────────────────────────────────── + # A workflow is ordered pairs, so every rendering keeps one key order. + + defp gen_workflow do + events = + Enum.take_random(["push", "pull_request", "pull_request_target", "release"], pick(1..3)) + + on = if coin(), do: {:map, Enum.map(events, &{&1, {:map, []}})}, else: {:seq, events} + + jobs = for i <- 1..pick(1..3), do: {"job#{i}", gen_job()} + top = [{"on", on}, {"jobs", {:map, jobs}}] + + top = + if chance(0.2), + do: [{"name", "w"}, {"env", {:map, [{"TOP", secret()}]}} | top], + else: [{"name", "w"} | top] + + {:map, top} + end + + defp gen_job do + steps = Enum.shuffle(for _ <- 1..pick(1..4), do: gen_step()) + steps = if chance(0.4), do: [harden_step() | steps], else: steps + + entries = + [{"steps", {:seq, steps}}] + |> then(&if(chance(0.25), do: [{"env", {:map, [{"JOB_KEY", secret()}]}} | &1], else: &1)) + |> then(&if(chance(0.9), do: [{"runs-on", "ubuntu-latest"} | &1], else: &1)) + + {:map, entries} + end + + defp harden_step do + owner = Enum.random(["step-security", "Step-Security"]) + uses = {"uses", "#{owner}/harden-runner@#{@sha}"} + + case Enum.random([:audit, :block, :none]) do + :none -> {:map, [uses]} + policy -> {:map, [uses, {"with", {:map, [{"egress-policy", Atom.to_string(policy)}]}}]} + end + end + + defp gen_step do + case pick(1..4) do + 1 -> + {:map, [{"run", "echo #{secret()}"}]} + + 2 -> + {:map, + [{"uses", "actions/upload-artifact@#{@sha}"}, {"with", {:map, [{"token", secret()}]}}]} + + 3 -> + ref = if coin(), do: [{"ref", "${{ github.event.pull_request.head.sha }}"}], else: [] + {:map, [{"uses", "actions/checkout@#{@sha}"}, {"with", {:map, ref}}]} + + 4 -> + {:map, [{"run", "make build"}]} + end + end + + defp secret, do: "${{ secrets.#{Enum.random(["API_KEY", "DEPLOY_TOKEN", "GITHUB_TOKEN"])} }}" + defp pick(range), do: Enum.random(range) + defp coin, do: chance(0.5) + defp chance(p), do: :rand.uniform() < p + + # ─── renderers ───────────────────────────────────────────────────── + + defp render(node, :flow), do: flow(node, 0) <> "\n" + defp render(node, style), do: Enum.join(block(node, 0, style), "\n") <> "\n" + + defp block({:map, []}, indent, _), do: [pad(indent) <> "{}"] + + defp block({:map, entries}, indent, style) do + Enum.flat_map(entries, fn {k, v} -> + key = pad(indent) <> scalar(k, style) <> ":" + + case v do + {:map, []} -> [key <> " {}"] + {:seq, []} -> [key <> " []"] + {_, _} -> [key | block(v, indent + 2, style)] + text -> value_lines(key, k, text, indent, style) + end + end) + end + + defp block({:seq, items}, indent, style) do + Enum.flat_map(items, fn + {:map, _} = item -> + [first | rest] = block(item, indent + 2, style) + [pad(indent) <> "- " <> String.trim_leading(first) | rest] + + text -> + [pad(indent) <> "- " <> scalar(text, style)] + end) + end + + defp value_lines(key, "run", text, indent, :literal), + do: [key <> " |", pad(indent + 2) <> text] + + defp value_lines(key, _, text, _indent, style), do: [key <> " " <> scalar(text, style)] + + defp scalar(text, :quoted), do: "'" <> String.replace(text, "'", "''") <> "'" + defp scalar(text, _), do: text + + defp flow({:map, entries}, indent) do + if entries == [] do + "{}" + else + inner = + Enum.map_join(entries, "", fn {k, v} -> + pad(indent + 2) <> flow_key(k) <> ": " <> flow(v, indent + 2) <> ",\n" + end) + + "{\n" <> inner <> pad(indent) <> "}" + end + end + + defp flow({:seq, items}, indent) do + if items == [] do + "[]" + else + inner = Enum.map_join(items, "", &(pad(indent + 2) <> flow(&1, indent + 2) <> ",\n")) + "[\n" <> inner <> pad(indent) <> "]" + end + end + + defp flow(text, _), do: inspect(text) + + # yq -o kyaml leaves a key unquoted where it can. + defp flow_key(key), do: if(key =~ ~r/\A[A-Za-z_][A-Za-z0-9_-]*\z/, do: key, else: inspect(key)) + + defp pad(n), do: String.duplicate(" ", n) +end diff --git a/test/research_extensions_test.exs b/test/research_extensions_test.exs index 6ce2bd1c..3637fb19 100644 --- a/test/research_extensions_test.exs +++ b/test/research_extensions_test.exs @@ -1078,7 +1078,7 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do write_deed( repo, ~s|(egress (job :workflow ".github/workflows/notify.yml" :job "notify" | <> - ~s|:secrets ("SMTP_PASS") :endpoints () :enforcement harden-runner-block))| + ~s|:secrets ("SMTP_PASS") :endpoints ("a.com:443" "b.com:443") :enforcement harden-runner-block))| ) findings = ResearchExtensions.re001_missing_harden_runner(repo) @@ -1281,8 +1281,9 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do assert plain =~ "`deploy`" assert plain =~ "HIDDEN" - # A merge key, `<<: *common`, inside the job's own env:. - assert [%{reason: merged}] = + # A merge key, `<<: *common`, is outside YAML 1.2 and GitHub refuses it: + # the workflow is reported as unreadable, at the key, not guessed at. + assert [%{line: 11, severity: :warn, reason: merged}] = check.(""" deploy: runs-on: ubuntu-24.04 @@ -1293,7 +1294,7 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do - run: send ${{ secrets.VISIBLE }} """) - assert merged =~ "HIDDEN" + assert merged =~ "UNSUPPORTED_MERGE_KEY" # The same declaration, without the alias, is exact. assert check.(""" @@ -1314,9 +1315,6 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do steps: - run: send ${{ secrets.SMTP_PASS }} deploy: *job - release: - <<: *job - name: release """, "notify.yml" ) @@ -1327,16 +1325,20 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do ~s|:secrets ("SMTP_PASS") :endpoints () :enforcement none))| ) - findings = ResearchExtensions.re001_missing_harden_runner(repo) - assert Enum.map(findings, & &1.line) == [6, 8] - assert Enum.all?(findings, &(&1.detail.fix =~ ~s|:secrets ("SMTP_PASS")|)) - assert Enum.any?(findings, &(&1.reason =~ "`deploy`")) - assert Enum.any?(findings, &(&1.reason =~ "`release`")) + # deploy is build, read through the alias and reported at it. + assert [%{line: 6, reason: reason, detail: %{fix: fix}}] = + ResearchExtensions.re001_missing_harden_runner(repo) + + assert reason =~ "`deploy`" + assert fix =~ ~s|:secrets ("SMTP_PASS")| File.rm_rf!(repo) end - test "a key the job sets itself wins over the same key from a merge" do - # The anchor's steps install harden-runner; the job's own steps do not. + test "a merge key makes the workflow unreadable: reported, never read in part" do + # Read as YAML 1.1, deploy's own steps: would win over the merged, + # hardened ones. GitHub reads YAML 1.2, which has no merge key, and so + # does RE001: one finding at the key, and the workflow's declarations + # are not reported stale, because they cannot be checked. repo = create_repo_with_workflow( """ @@ -1360,14 +1362,17 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do "notify.yml" ) - write_deed(repo, "") + write_deed( + repo, + ~s|(egress (job :workflow ".github/workflows/notify.yml" :job "deploy" | <> + ~s|:secrets ("VISIBLE") :endpoints () :enforcement none))| + ) - # deploy holds VISIBLE only (its env: replaces the merged one) and has - # no hardener (its steps: replace the merged ones). - assert [%{line: 16, detail: %{fix: fix}}] = + assert [%{line: 12, severity: :warn, reason: reason, detail: %{fix: fix}}] = ResearchExtensions.re001_missing_harden_runner(repo) - assert fix =~ ~s|:job "deploy" :secrets ("VISIBLE")| + assert reason =~ "UNSUPPORTED_MERGE_KEY at line 12, column 5" + assert fix =~ "`<<` merge key" File.rm_rf!(repo) end @@ -1438,10 +1443,10 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do File.rm_rf!(repo) end - test "nested anchors that multiply (the billion-laughs file) are expanded within a budget" do + test "nested anchors that multiply (the billion-laughs file) are refused within a budget" do anchors = for i <- 1..9 do - prev = if i == 1, do: "${{ secrets.SMTP_PASS }}", else: "*a#{i - 1}" + prev = if i == 1, do: ~s|"${{ secrets.SMTP_PASS }}"|, else: "*a#{i - 1}" " a#{i}: &a#{i} [#{Enum.map_join(1..10, ", ", fn _ -> prev end)}]" end @@ -1465,8 +1470,10 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do {micros, findings} = :timer.tc(fn -> ResearchExtensions.re001_missing_harden_runner(repo) end) - assert [%{detail: %{fix: fix}}] = findings - assert fix =~ ~s|:secrets ("SMTP_PASS")| + # Past kyq's node budget the workflow is refused, as kyq refuses it, and + # the refusal is a finding: a job it hides is never a silent pass. + assert [%{severity: :warn, reason: reason}] = findings + assert reason =~ "NODE_BUDGET_EXCEEDED" assert micros < 10_000_000 File.rm_rf!(repo) end @@ -1879,10 +1886,238 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do assert ResearchExtensions.re001_missing_harden_runner(repo) == [] File.rm_rf!(repo) end + + # ─── declared endpoints against the workflow ────────────────────── + + defp endpoint_findings(steps, endpoints) do + repo = + create_repo_with_workflow( + "on: push\njobs:\n ship:\n runs-on: ubuntu-latest\n steps:\n" <> steps, + "ship.yml" + ) + + write_deed( + repo, + ~s|(egress (job :workflow ".github/workflows/ship.yml" :job "ship" | <> + ~s|:secrets ("TOKEN") :endpoints (#{endpoints}) :enforcement none))| + ) + + findings = ResearchExtensions.re001_missing_harden_runner(repo) + File.rm_rf!(repo) + findings + end + + test "a host a step names literally must be declared" do + steps = """ + - run: | + # docs: https://docs.example.org/upload + curl -H "t: ${{ secrets.TOKEN }}" https://upload.example.com/v1#frag + """ + + assert [finding] = endpoint_findings(steps, "") + assert finding.severity == :warn + assert finding.line == 8 + assert finding.reason =~ ~s|names "upload.example.com:443" literally| + refute finding.reason =~ "docs.example.org" + + assert endpoint_findings(steps, ~s|"upload.example.com"|) == [] + assert endpoint_findings(steps, ~s|"*.example.com"|) == [] + assert endpoint_findings(steps, ~s|"upload.example.com:443"|) == [] + assert [_] = endpoint_findings(steps, ~s|"upload.example.com:8443"|) + # A wildcard covers subdomains, not the apex; a secret covers no literal host. + assert [_] = endpoint_findings(steps, ~s|"*.upload.example.com"|) + assert [_] = endpoint_findings(steps, ~s|"secret:TOKEN"|) + end + + # hypatia's own push-email-notify.yml lets out + # `${{ secrets.SMTP_HOST }}:${{ secrets.SMTP_PORT || '465' }}`: an entry + # whose host is known only at run time. It is one unit however it is + # spaced, and it is not a literal host to compare (it crashed the + # comparison while it was split on its spaces). + test "an allowed endpoint written with expressions is not a literal host" do + run = fn allowed, endpoints -> + workflow = + Enum.join( + [ + "on: push", + "jobs:", + " ship:", + " runs-on: ubuntu-latest", + " steps:", + " - uses: step-security/harden-runner@v2", + " with:", + " egress-policy: block", + " allowed-endpoints: >" + ] ++ + Enum.map(allowed, &(" " <> &1)) ++ + [~S| - run: send --token "${{ secrets.TOKEN }}"|], + "\n" + ) <> "\n" + + repo = create_repo_with_workflow(workflow, "ship.yml") + + write_deed( + repo, + ~s|(egress (job :workflow ".github/workflows/ship.yml" :job "ship" | <> + ~s|:secrets ("SMTP_HOST" "SMTP_PORT" "TOKEN") :endpoints (#{endpoints}) | <> + ~s|:enforcement harden-runner-block))| + ) + + # The deed must be readable, or a hardened job passes vacuously. + assert {:ok, _, [_]} = Hypatia.Deed.egress_declarations(repo) + findings = ResearchExtensions.re001_missing_harden_runner(repo) + File.rm_rf!(repo) + findings + end + + smtp = "${{ secrets.SMTP_HOST }}:${{ secrets.SMTP_PORT || '465' }}" + + assert run.(["github.com:443", smtp], ~s|"secret:SMTP_HOST"|) == [] + + # A literal host beside the expression is still held to the deed. + assert [finding] = + run.(["github.com:443", "relay.example.net:587", smtp], ~s|"secret:SMTP_HOST"|) + + assert finding.reason =~ "relay.example.net:587" + + assert run.( + ["github.com:443", "relay.example.net:587", smtp], + ~s|"secret:SMTP_HOST" "relay.example.net:587"| + ) == [] + + # GitHub's own hosts are outside the comparison on both sides: a deed + # may list them (hypatia_chora.deed does) and is not held to them. + assert run.( + ["github.com:443", smtp], + ~s|"github.com:443" "api.github.com:443" "secret:SMTP_HOST"| + ) == + [] + end + + test "an ssh remote is port 22, and GitHub's own hosts are never declared" do + steps = """ + - run: git push git@gitlab.com:o/x.git && git push https://github.com/o/x + env: + KEY: ${{ secrets.TOKEN }} + - uses: actions/checkout@v4 + with: + repository: https://raw.githubusercontent.com/o/x + """ + + assert [finding] = endpoint_findings(steps, "") + assert finding.reason =~ ~s|"gitlab.com:22"| + refute finding.reason =~ "github.com" + refute finding.reason =~ "githubusercontent" + assert endpoint_findings(steps, ~s|"gitlab.com:22"|) == [] + assert [_] = endpoint_findings(steps, ~s|"gitlab.com:443"|) + end + + test "harden-runner's allowed-endpoints and the declaration must agree" do + steps = fn allowed -> + """ + - uses: step-security/harden-runner@v2 + with: + egress-policy: block + allowed-endpoints: > + #{allowed} + - run: deploy --token ${{ secrets.TOKEN }} + """ + end + + agree = steps.("api.github.com:443 hex.pm:443 repo.hex.pm:443") + assert endpoint_findings(agree, ~s|"hex.pm" "*.hex.pm:443"|) == [] + + assert [finding] = endpoint_findings(agree, ~s|"hex.pm"|) + assert finding.reason =~ ~s|lets out undeclared "repo.hex.pm:443"| + + assert [finding] = endpoint_findings(steps.("hex.pm:443"), ~s|"hex.pm" "cdn.example.com"|) + assert finding.reason =~ ~s|does not allow declared "cdn.example.com"| + end end # ─── RE002 ────────────────────────────────────────────────────────── + # The three shapes Codex raised on #975 after it merged, each one a line + # reader's misreading of YAML. Read from the parsed model they cannot occur. + describe "re001_missing_harden_runner/1 on the #975 post-merge shapes" do + @sha "1234567890abcdef1234567890abcdef12345678" + + # A hardened job whose harden-runner step carries `hardener_lines` (step + # properties, given at the step's own column) and a block declaration. + defp hardened_repo(hardener_lines) do + workflow = + Enum.join( + [ + "jobs:", + " notify:", + " runs-on: ubuntu-24.04", + " steps:", + " - uses: step-security/harden-runner@#{@sha}" + ] ++ + Enum.map(hardener_lines, &(" " <> &1)) ++ + [~S| - run: curl -u "$U:${{ secrets.SMTP_PASS }}" https://mail.example.com|], + "\n" + ) <> "\n" + + repo = create_repo_with_workflow(workflow, "notify.yml") + + write_deed( + repo, + ~s|(egress :policy "standards ADR-009" (job :workflow ".github/workflows/notify.yml" | <> + ~s|:job "notify" :secrets ("SMTP_PASS") :endpoints ("mail.example.com:443") | <> + ~s|:enforcement harden-runner-block))| + ) + + repo + end + + test "a `<<: [*defaults]` merge is not guessed at: the workflow is reported unreadable" do + repo = + create_repo_with_workflow( + """ + x-defaults: &defaults + runs-on: ubuntu-24.04 + env: + TOKEN: ${{ secrets.DEPLOY_TOKEN }} + jobs: + deploy: + <<: [*defaults] + steps: + - run: ./deploy.sh + """, + "deploy.yml" + ) + + assert [finding] = ResearchExtensions.re001_missing_harden_runner(repo) + assert finding.severity == :warn + assert finding.line == 7 + assert finding.reason =~ "UNSUPPORTED_MERGE_KEY" + File.rm_rf!(repo) + end + + test "text in a block scalar beside the hardener is not its input" do + repo = hardened_repo(["name: |", " with:", " egress-policy: block"]) + + # harden-runner runs its default, audit: the block claim is false. + assert [finding] = ResearchExtensions.re001_missing_harden_runner(repo) + assert finding.reason =~ ":enforcement harden-runner-block" + File.rm_rf!(repo) + end + + test "a folded egress-policy is read as its value" do + repo = + hardened_repo([ + "with:", + " egress-policy: >-", + " block", + " allowed-endpoints: mail.example.com:443" + ]) + + assert ResearchExtensions.re001_missing_harden_runner(repo) == [] + File.rm_rf!(repo) + end + end + describe "re002_harden_runner_audit_mode/1" do test "flags harden-runner in audit mode on push trigger" do repo = @@ -1923,6 +2158,64 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do assert ResearchExtensions.re002_harden_runner_audit_mode(repo) == [] File.rm_rf!(repo) end + + test "matches the action owner in any case, as RE001 does" do + repo = + create_repo_with_workflow(""" + on: [push] + jobs: + x: + runs-on: ubuntu-latest + steps: + - uses: Step-Security/Harden-Runner@1234567890abcdef1234567890abcdef12345678 + with: + egress-policy: audit + """) + + assert [%{rule: "RE002"}] = ResearchExtensions.re002_harden_runner_audit_mode(repo) + File.rm_rf!(repo) + end + + test "a hardener with no egress-policy runs harden-runner's default, audit" do + repo = + create_repo_with_workflow(""" + on: {release: {types: [published]}} + jobs: + x: + runs-on: ubuntu-latest + steps: + - uses: "step-security/harden-runner@1234567890abcdef1234567890abcdef12345678" + """) + + assert [%{reason: reason}] = ResearchExtensions.re002_harden_runner_audit_mode(repo) + assert reason =~ "its default" + File.rm_rf!(repo) + end + + test "only a real hardener step and a real push or release trigger count" do + repo = + create_repo_with_workflow(""" + on: + pull_request: + branches: [main] + jobs: + push: + runs-on: ubuntu-latest + steps: + - uses: step-security/harden-runner@1234567890abcdef1234567890abcdef12345678 + with: + egress-policy: audit + release: + runs-on: ubuntu-latest + steps: + - run: | + echo "uses: step-security/harden-runner@x" + echo "egress-policy: audit" + """) + + assert ResearchExtensions.re002_harden_runner_audit_mode(repo) == [] + File.rm_rf!(repo) + end end # ─── RE003 ────────────────────────────────────────────────────────── diff --git a/test/workflow_test.exs b/test/workflow_test.exs new file mode 100644 index 00000000..f3b0b7b2 --- /dev/null +++ b/test/workflow_test.exs @@ -0,0 +1,172 @@ +# SPDX-License-Identifier: MPL-2.0 +defmodule Hypatia.WorkflowTest do + use ExUnit.Case, async: true + + alias Hypatia.Workflow + alias Hypatia.Workflow.{Job, Step} + + @block """ + name: ci + on: + push: + branches: [main] + pull_request: {} + env: + GLOBAL: ${{ secrets.TOP }} + permissions: + contents: read + jobs: + build: + runs-on: ubuntu-24.04 + if: github.event_name == 'push' + env: + KEY: ${{ secrets.API_KEY }} + steps: + - uses: actions/checkout@v4 + with: + ref: main + - name: build + run: >- + make + all + env: + LOCAL: x + if: success() + call: + uses: o/r/.github/workflows/w.yml@v1 + """ + + @flow """ + { + name: "ci", + on: {push: {branches: ["main"]}, pull_request: {}}, + env: {GLOBAL: "${{ secrets.TOP }}"}, + permissions: {contents: "read"}, + jobs: { + build: { + runs-on: "ubuntu-24.04", + if: "github.event_name == 'push'", + env: {KEY: "${{ secrets.API_KEY }}"}, + steps: [ + {uses: "actions/checkout@v4", with: {ref: "main"}}, + {name: "build", run: "make all", env: {LOCAL: "x"}, if: "success()"}, + ], + }, + call: {uses: "o/r/.github/workflows/w.yml@v1"}, + }, + } + """ + + test "reads a workflow's jobs and steps, with values as YAML gives them" do + assert {:ok, %Workflow{path: "ci.yml"} = wf} = Workflow.parse(@block, "ci.yml") + assert wf.triggers == ["push", "pull_request"] + assert [{"GLOBAL", _}] = for(e <- Workflow.entries(wf.env), do: {e.key.value, e}) + assert Workflow.text(Hypatia.Kyaml.get(wf.permissions, "contents")) == "read" + + assert [%Job{id: "build"} = build, %Job{id: "call"} = call] = wf.jobs + assert build.line == 11 + assert Workflow.text(build.runs_on) == "ubuntu-24.04" + assert build.if == "github.event_name == 'push'" + assert call.uses == "o/r/.github/workflows/w.yml@v1" + assert call.runs_on == nil + + assert [%Step{} = checkout, %Step{} = make] = build.steps + assert checkout.uses == "actions/checkout@v4" + assert Workflow.input(checkout, "ref") == "main" + assert checkout.run == nil + assert {checkout.line, make.line} == {17, 20} + # A folded block scalar is folded and chomped: `>-` joins the lines. + assert make.run == "make all" + assert make.run_style == :block + assert make.if == "success()" + assert [%{key: %{value: "LOCAL"}}] = Workflow.entries(make.env) + end + + test "block and flow layouts give the same model, apart from lines" do + assert {:ok, block} = Workflow.parse(@block) + assert {:ok, flow} = Workflow.parse(@flow) + assert shape(block) == shape(flow) + end + + defp shape(%Workflow{} = wf) do + {wf.triggers, env_names(wf.env), + for job <- wf.jobs do + {job.id, Workflow.text(job.runs_on), job.uses, job.if, env_names(job.env), + for step <- job.steps do + {step.uses, step.run, step.if, Workflow.input(step, "ref"), env_names(step.env)} + end} + end} + end + + defp env_names(env), do: for(e <- Workflow.entries(env), do: e.key.value) + + test "every string under a node keeps its own source line, through block scalars and aliases" do + yaml = """ + x-script: &script | + echo one + echo ${{ secrets.TWO }} + jobs: + a: + runs-on: ubuntu-24.04 + steps: + - run: *script + """ + + assert {:ok, wf} = Workflow.parse(yaml) + [%Job{steps: [step]}] = wf.jobs + # The step's run is the anchored script, read through the alias... + assert step.run == "echo one\necho ${{ secrets.TWO }}\n" + # ...and every byte of it is reported at the alias, line 8. + assert [{value, line_of}] = Workflow.strings(step.node) + assert value == step.run + assert line_of.(0) == 8 and line_of.(byte_size(value) - 1) == 8 + + # The same scalar read where it is written maps each line to its own. + anchor = Hypatia.Kyaml.get(wf.doc, "x-script") + assert [{_, own_line}] = Workflow.strings(anchor) + assert own_line.(0) == 2 + assert own_line.(byte_size("echo one\n")) == 3 + end + + test "`on:` is read as events in its three forms" do + for {on, events} <- [ + {"push", ["push"]}, + {"[push, release]", ["push", "release"]}, + {"{workflow_dispatch: {}, schedule: [{cron: '0 0 * * *'}]}", + ["workflow_dispatch", "schedule"]} + ] do + assert {:ok, wf} = Workflow.parse("on: #{on}\njobs: {}\n") + assert wf.triggers == events, on + end + end + + test "an empty stream is no workflow" do + assert Workflow.parse("") == {:ok, nil} + assert Workflow.parse("# only a comment\n") == {:ok, nil} + end + + test "what the reader refuses is an error at its location, never a guess" do + merge = """ + x: &d + runs-on: ubuntu-24.04 + jobs: + a: + <<: [*d] + """ + + assert {:error, %Hypatia.Kyaml.Error{code: "UNSUPPORTED_MERGE_KEY", line: 5}} = + Workflow.parse(merge) + + # The anchor bomb: past kyq's node budget the workflow is refused whole. + bomb = + ["a: &a [x, x, x, x, x, x, x, x, x, x]"] ++ + for( + i <- ?b..?h, + do: "#{<>}: &#{<>} [#{List.duplicate("*#{<>}", 10) |> Enum.join(", ")}]" + ) ++ + ["jobs: {}"] + + assert {:error, %Hypatia.Kyaml.Error{code: "NODE_BUDGET_EXCEEDED", line: 1}} = + Workflow.parse(Enum.join(bomb, "\n") <> "\n") + end +end From 3562e82197bb2c24668c857580bb8efc76a9feb0 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:35:37 +0000 Subject: [PATCH 02/14] Prove RE001's egress decision and the KYAML alias budget; hold the code to both src/Hypatia/ABI/Egress.idr models RE001's acceptance of a secret-bearing job (standards ADR-009) as a decidable type, Clean, and proves: an audit hardener never satisfies a block claim; a declaration lists exactly the secrets the job reads; a key computed at run time is never declared; a bare job fails; a claimed enforcement needs a hardener. Three expected rejections and a positive control (which evaluates decClean) run in scripts/check-verdicts.sh. verification/proofs/idris2/KyamlBudget.idr models within_budget?/2 step for step and proves it sound (a total within the limit is the expanded size), complete (a document within the limit passes) and bounded (2 * (limit + 1) + 2 steps when no alias names an alias, however far the aliases expand). The Elixir code is held to both models: test/egress_decision_mirror_test.exs runs RE001 on all 240 cases of a small domain and requires agreement with decClean (three mutants killed); test/kyaml_test.exs compares within_budget?/2 with the model's size on 154 trees at every limit (an alias-dropping mutant killed). PROOF-STATUS rows record what is PROVEN, TESTED, OPEN (endpoint comparison) and ASSUMED (GitHub reads workflows as YAML 1.2 Core does). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- .claude/CLAUDE.md | 1 + .github/workflows/ci.yml | 1 + CHANGELOG.adoc | 20 ++ scripts/check-verdicts.sh | 2 +- src/Hypatia/ABI/Egress.idr | 147 +++++++++++ src/abi/hypatia-abi.ipkg | 1 + test/egress_decision_mirror_test.exs | 172 +++++++++++++ test/kyaml_test.exs | 38 +++ tests/accept/DeclaredJobIsClean.idr | 42 ++++ tests/reject/AuditPassesAsBlock.idr | 26 ++ tests/reject/DynamicKeyDeclared.idr | 25 ++ tests/reject/UndeclaredSecretPasses.idr | 23 ++ verification/PROOF-STATUS.adoc | 87 +++++++ verification/proofs/idris2/KyamlBudget.idr | 268 +++++++++++++++++++++ 14 files changed, 852 insertions(+), 1 deletion(-) create mode 100644 src/Hypatia/ABI/Egress.idr create mode 100644 test/egress_decision_mirror_test.exs create mode 100644 tests/accept/DeclaredJobIsClean.idr create mode 100644 tests/reject/AuditPassesAsBlock.idr create mode 100644 tests/reject/DynamicKeyDeclared.idr create mode 100644 tests/reject/UndeclaredSecretPasses.idr create mode 100644 verification/proofs/idris2/KyamlBudget.idr diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 476acedf..269522e2 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -177,6 +177,7 @@ Training pipeline reads outcomes/*.jsonl for ESN (confidence time series) and pa | `RuleEngine.idr` | Rule-evaluation types | | `Verdict.idr` | Verdict records (HYP-01): support = Pattern / Observed n / Mechanical re-check; `Sound` only from a confirming re-check. Gate: `scripts/check-verdicts.sh` (+ `tests/reject/`, `tests/accept/`) | | `Retraction.idr` | Quarantine as retraction (HYP-01): a token survives iff its support thins into what remains; a finding survives through one of its tokens. Transcribed from residual-evidence-types `Revision.agda` @ 97244f5 | +| `Egress.idr` | RE001's decision on egress declarations (standards ADR-009): `Clean` is decidable (`decClean`); an audit hardener never passes a block claim; a declaration lists exactly the secrets read; a run-time key is never declared. Mirror: `test/egress_decision_mirror_test.exs` | **Build system:** `src/abi/hypatia-abi.ipkg` (compile), `verify/hypatia-verify.ipkg` (proofs), `pack.toml` (Pack package manager). The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles** — that is the diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8072daa8..41569ed5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -359,6 +359,7 @@ jobs: test/research_extensions_test.exs \ test/research_extensions_equivalence_test.exs \ test/workflow_test.exs \ + test/egress_decision_mirror_test.exs \ test/deed_test.exs \ test/kyaml_test.exs \ test/kyaml_conformance_test.exs diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 3eb59451..4b1ff5d8 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -81,6 +81,26 @@ there and are fixed with tests: an `allowed-endpoints` entry written with an expression crashed it (hypatia's own `push-email-notify.yml`), and a deed listing GitHub hosts drew 12 false findings on hypatia. +The decision and the alias budget are proved, and the code is held to the +proofs (verification/PROOF-STATUS.adoc, "Egress declarations and the KYAML +reader"): + +* `src/Hypatia/ABI/Egress.idr` models RE001's acceptance of a job as a + decidable type and proves that an audit hardener never satisfies a block + claim, that a declaration lists exactly the secrets read, and that a key + computed at run time is never declared. Three expected rejections and a + positive control run in `scripts/check-verdicts.sh`. + `test/egress_decision_mirror_test.exs` runs RE001 on all 240 cases of a + small domain and requires it to agree with the proved decision. +* `verification/proofs/idris2/KyamlBudget.idr` models `within_budget?/2` + and proves that it passes exactly the documents whose expanded size is + within the limit, in at most 2 · (limit + 1) + 2 steps however far the + aliases expand. `test/kyaml_test.exs` holds the Elixir count to the + model on 154 trees at every limit. + +The reader as a whole is tested, not proved, and endpoints are not +modelled; both are recorded as such. + ==== RE001 accepts a deed egress declaration; the job token no longer counts (2026-10-27) The estate-wide decision on `step-security/harden-runner` (standards ADR-009) is diff --git a/scripts/check-verdicts.sh b/scripts/check-verdicts.sh index ba896bcd..45494978 100755 --- a/scripts/check-verdicts.sh +++ b/scripts/check-verdicts.sh @@ -40,7 +40,7 @@ mkdir -p "$logs" export IDRIS2_PATH="$PWD/build/abi/ttc${IDRIS2_PATH:+:$IDRIS2_PATH}" # 2. No escape hatch in the modules the rejections are about. -for module in src/Hypatia/ABI/Verdict.idr src/Hypatia/ABI/Retraction.idr; do +for module in src/Hypatia/ABI/Verdict.idr src/Hypatia/ABI/Retraction.idr src/Hypatia/ABI/Egress.idr; do if grep -nE 'believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry|admit|native_decide|Admitted|unsafeCoerce|Obj\.magic' \ "$module"; then echo "ERROR: escape-hatch marker in $module" >&2 diff --git a/src/Hypatia/ABI/Egress.idr b/src/Hypatia/ABI/Egress.idr new file mode 100644 index 00000000..3af53279 --- /dev/null +++ b/src/Hypatia/ABI/Egress.idr @@ -0,0 +1,147 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Egress declarations (standards ADR-009) and RE001's decision on them. +-- +-- A job that reads a real secret is acceptable to RE001 in exactly two ways: +-- it runs `step-security/harden-runner` and declares nothing, or the repo deed +-- declares it, and the declaration is true of the workflow: +-- +-- * it lists exactly the secrets the job reads (no key is computed at run +-- time, which no list can name); +-- * the enforcement it claims holds: `none` claims nothing, +-- `harden-runner-audit` needs a hardener in any mode, and +-- `harden-runner-block` needs one whose `egress-policy` is `block`. +-- +-- `Clean job decl` is that acceptance, as a type: a value of it is the +-- evidence. The theorems below are the properties the Elixir rule +-- (lib/rules/research_extensions.ex, re001_missing_harden_runner/1) is built +-- to have; tests/reject/ holds the shapes the type must refuse, and +-- test/egress_decision_mirror_test.exs holds the Elixir rule to this decision +-- on every case of a small domain. Endpoint comparison is outside this model. + +module Hypatia.ABI.Egress + +-- Re-exported: the decision procedure below is public, and a caller can +-- evaluate it (tests/accept/DeclaredJobIsClean.idr does) only with the +-- membership and string-equality definitions it unfolds to in scope. +import public Data.List.Elem +import public Data.List.Quantifiers +import public Decidable.Equality + +%default total + +||| A harden-runner step's `egress-policy` (harden-runner's default is audit). +public export +data Policy = Audit | Block + +||| The `:enforcement` a declaration claims (egress.abnf). +public export +data Enforcement = None | HardenRunnerAudit | HardenRunnerBlock + +||| A job as RE001 reads it: the secrets it reads, whether a key is computed +||| at run time (`secrets[env.X]`, `toJSON(secrets)`), and its hardener. +public export +record Job where + constructor MkJob + secrets : List String + dynamic : Bool + hardener : Maybe Policy + +||| A deed declaration for the job. +public export +record Decl where + constructor MkDecl + declared : List String + enforcement : Enforcement + +||| Two lists name the same secrets. +public export +SameSecrets : List String -> List String -> Type +SameSecrets xs ys = (All (\x => Elem x ys) xs, All (\y => Elem y xs) ys) + +||| A claimed enforcement holds of the job's hardener. +public export +data Holds : Enforcement -> Maybe Policy -> Type where + ClaimsNothing : Holds None h + AnyHardener : Holds HardenRunnerAudit (Just p) + Blocking : Holds HardenRunnerBlock (Just Block) + +||| RE001 accepts the job with this declaration (or with none). +public export +data Clean : Job -> Maybe Decl -> Type where + ||| Hardened, and nothing declared. + Hardened : Clean (MkJob s d (Just p)) Nothing + ||| Declared, and the declaration is true. + Declared : SameSecrets s ds -> Holds e h -> Clean (MkJob s False h) (Just (MkDecl ds e)) + +-- ─── Decidability: RE001 is a decision procedure ─────────────────────── + +public export +decElems : (xs, ys : List String) -> Dec (All (\x => Elem x ys) xs) +decElems xs ys = all (\x => isElem x ys) xs + +public export +decSame : (xs, ys : List String) -> Dec (SameSecrets xs ys) +decSame xs ys with (decElems xs ys) + _ | No no = No (\(a, _) => no a) + _ | Yes a with (decElems ys xs) + _ | Yes b = Yes (a, b) + _ | No no = No (\(_, b) => no b) + +public export +decHolds : (e : Enforcement) -> (h : Maybe Policy) -> Dec (Holds e h) +decHolds None h = Yes ClaimsNothing +decHolds HardenRunnerAudit (Just p) = Yes AnyHardener +decHolds HardenRunnerAudit Nothing = No (\case ClaimsNothing impossible) +decHolds HardenRunnerBlock (Just Block) = Yes Blocking +decHolds HardenRunnerBlock (Just Audit) = No (\case ClaimsNothing impossible) +decHolds HardenRunnerBlock Nothing = No (\case ClaimsNothing impossible) + +||| RE001's verdict on a job and its declaration is decidable. +public export +decClean : (j : Job) -> (d : Maybe Decl) -> Dec (Clean j d) +decClean (MkJob s dyn (Just p)) Nothing = Yes Hardened +decClean (MkJob s dyn Nothing) Nothing = No (\case Hardened impossible) +decClean (MkJob s True h) (Just (MkDecl ds e)) = No (\case Hardened impossible) +decClean (MkJob s False h) (Just (MkDecl ds e)) with (decSame s ds) + _ | No no = No (\(Declared same _) => no same) + _ | Yes same with (decHolds e h) + _ | Yes holds = Yes (Declared same holds) + _ | No no = No (\(Declared _ holds) => no holds) + +-- ─── The properties RE001 is built to have ───────────────────────────── + +||| An audit-mode hardener never satisfies a block claim, whatever the +||| secrets (the #975 shape: a hardener that audits must not pass as one +||| that blocks). +export +auditNeverBlock : Clean (MkJob s dyn (Just Audit)) (Just (MkDecl ds HardenRunnerBlock)) -> Void +auditNeverBlock (Declared _ holds) = case holds of {} + +||| Every secret the job reads is declared. +export +readSecretDeclared : Clean (MkJob s dyn h) (Just (MkDecl ds e)) -> Elem x s -> Elem x ds +readSecretDeclared (Declared (inDs, _) _) el = indexAll el inDs + +||| Every declared secret is one the job reads (a declaration does not +||| over-claim). +export +declaredSecretRead : Clean (MkJob s dyn h) (Just (MkDecl ds e)) -> Elem y ds -> Elem y s +declaredSecretRead (Declared (_, inS) _) el = indexAll el inS + +||| A key computed at run time is never covered by a declaration. +export +dynamicNeverDeclared : Clean (MkJob s True h) (Just d) -> Void +dynamicNeverDeclared Hardened impossible +dynamicNeverDeclared (Declared _ _) impossible + +||| A secret-bearing job with neither a hardener nor a declaration fails. +export +bareJobFails : Clean (MkJob s dyn Nothing) Nothing -> Void +bareJobFails Hardened impossible + +||| A claim of enforcement needs a hardener to hold. +export +claimNeedsHardener : Clean (MkJob s dyn Nothing) (Just (MkDecl ds e)) -> Not (e = None) -> Void +claimNeedsHardener (Declared _ ClaimsNothing) notNone = notNone Refl diff --git a/src/abi/hypatia-abi.ipkg b/src/abi/hypatia-abi.ipkg index 7a8964a9..b0a99171 100644 --- a/src/abi/hypatia-abi.ipkg +++ b/src/abi/hypatia-abi.ipkg @@ -24,6 +24,7 @@ modules = Hypatia.ABI.Types , Hypatia.ABI.RuleEngine , Hypatia.ABI.Verdict , Hypatia.ABI.Retraction + , Hypatia.ABI.Egress builddir = "../../build/abi" diff --git a/test/egress_decision_mirror_test.exs b/test/egress_decision_mirror_test.exs new file mode 100644 index 00000000..a8328687 --- /dev/null +++ b/test/egress_decision_mirror_test.exs @@ -0,0 +1,172 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +defmodule Hypatia.EgressDecisionMirrorTest do + @moduledoc """ + Holds RE001 to the decision proved in `src/Hypatia/ABI/Egress.idr`. + + `decClean` there decides whether RE001 accepts a secret-bearing job with a + deed declaration (or with none). `clean?/2` below is that function written + out clause for clause. Every case of a small domain is generated as a real + workflow and deed, RE001 is run on it, and RE001 must report nothing exactly + when `clean?/2` says the job is clean: + + * the job reads one or two secrets, by name, and possibly also by a key + computed at run time; + * it has no hardener, or harden-runner with `egress-policy` unset, + `audit` or `block`; + * it is undeclared, or declared with any non-empty subset of the two + secrets (egress.abnf refuses an empty list) and each of the three + enforcements. + + Endpoints are outside the model, so the cases name no host and declare + none. + """ + use ExUnit.Case, async: true + + alias Hypatia.Rules.ResearchExtensions + + @secrets ["ALPHA", "BETA"] + + # ─── Egress.idr's decClean, clause for clause ────────────────────── + + # decClean (MkJob s dyn (Just p)) Nothing = Yes Hardened + # decClean (MkJob s dyn Nothing) Nothing = No + defp clean?(job, nil), do: job.hardener != nil + # decClean (MkJob s True h) (Just _) = No + defp clean?(%{dynamic: true}, _decl), do: false + # decClean (MkJob s False h) (Just (MkDecl ds e)) = decSame s ds && decHolds e h + defp clean?(job, decl), + do: + MapSet.new(job.secrets) == MapSet.new(decl.secrets) and + holds?(decl.enforcement, job.hardener) + + # decHolds: None holds of anything; HardenRunnerAudit of any hardener; + # HardenRunnerBlock only of a hardener whose policy is Block. + defp holds?(:none, _), do: true + defp holds?(:audit, hardener), do: hardener != nil + defp holds?(:block, hardener), do: hardener == :block + + # ─── The domain ────────────────────────────────────────────────── + + defp subsets(xs), do: Enum.reduce(xs, [[]], fn x, acc -> acc ++ Enum.map(acc, &(&1 ++ [x])) end) + + defp jobs do + for secrets <- subsets(@secrets), + secrets != [], + dynamic <- [false, true], + hardener <- [nil, :default, :audit, :block], + do: %{secrets: secrets, dynamic: dynamic, hardener: hardener} + end + + defp decls do + [nil] ++ + for secrets <- subsets(@secrets), + # egress.abnf refuses an empty `:secrets ()`. + secrets != [], + enforcement <- [:none, :audit, :block], + do: %{secrets: secrets, enforcement: enforcement} + end + + # harden-runner's default policy is audit (Egress.idr's Policy). + defp policy(:default), do: :audit + defp policy(other), do: other + + # ─── The case as files ─────────────────────────────────────────── + + defp workflow(job) do + hardener = + case job.hardener do + nil -> + [] + + :default -> + [" - uses: step-security/harden-runner@v2"] + + p -> + [ + " - uses: step-security/harden-runner@v2", + " with:", + " egress-policy: #{p}" + ] + end + + reads = Enum.map(job.secrets, &" - run: send ${{ secrets.#{&1} }}") + dynamic = if job.dynamic, do: [" - run: send ${{ secrets[env.NAME] }}"], else: [] + + Enum.join( + ["jobs:", " notify:", " runs-on: ubuntu-24.04", " steps:"] ++ + hardener ++ reads ++ dynamic, + "\n" + ) <> "\n" + end + + @enforcement %{none: "none", audit: "harden-runner-audit", block: "harden-runner-block"} + + defp deed(nil), do: "" + + defp deed(decl) do + secrets = Enum.map_join(decl.secrets, " ", &~s|"#{&1}"|) + + ~s|(egress (job :workflow ".github/workflows/notify.yml" :job "notify" | <> + ~s|:secrets (#{secrets}) :endpoints () :enforcement #{@enforcement[decl.enforcement]}))| + end + + defp re001(job, decl, n) do + repo = + Path.join(System.tmp_dir!(), "egress_mirror_#{System.unique_integer([:positive])}_#{n}") + + File.rm_rf!(repo) + File.mkdir_p!(Path.join([repo, ".github", "workflows"])) + File.write!(Path.join([repo, ".github", "workflows", "notify.yml"]), workflow(job)) + + File.write!(Path.join(repo, "x_chora.deed"), """ + ;; SPDX-License-Identifier: CC-BY-SA-4.0 + (repo-deed :schema-version "1.0.0" :canonical-name "x" + :repo-uuid #u5"github.com/o/x" :beholding-chora #u5"estate/chora" + #{deed(decl)}) + """) + + try do + # The deed must say what the case says, or the comparison is vacuous. + declared = + case Hypatia.Deed.egress_declarations(repo) do + {:ok, _, jobs} -> length(jobs) + :none -> 0 + end + + assert declared == if(decl, do: 1, else: 0) + ResearchExtensions.re001_missing_harden_runner(repo) + after + File.rm_rf!(repo) + end + end + + test "RE001 reports a job exactly when Egress.idr's decClean refuses it" do + cases = for job <- jobs(), decl <- decls(), do: {job, decl} + # 3 secret sets x 2 x 4 hardeners, each with no declaration or 3 x 3. + assert length(cases) == 24 * 10 + + mismatches = + cases + |> Enum.with_index() + |> Enum.flat_map(fn {{job, decl}, n} -> + model_job = %{job | hardener: job.hardener && policy(job.hardener)} + expected_clean = clean?(model_job, decl) + findings = re001(job, decl, n) + + if findings == [] == expected_clean, + do: [], + else: [{job, decl, expected_clean, Enum.map(findings, & &1.reason)}] + end) + + assert mismatches == [] + + # Both verdicts occur, so neither side is constant. + verdicts = + for {job, decl} <- cases, + do: clean?(%{job | hardener: job.hardener && policy(job.hardener)}, decl) + + assert Enum.count(verdicts, & &1) > 0 and Enum.count(verdicts, &(!&1)) > 0 + end +end diff --git a/test/kyaml_test.exs b/test/kyaml_test.exs index 7b339c66..84e6725c 100644 --- a/test/kyaml_test.exs +++ b/test/kyaml_test.exs @@ -70,6 +70,44 @@ defmodule Hypatia.KyamlTest do refute Kyaml.within_budget?(doc, 1) end + # verification/proofs/idris2/KyamlBudget.idr proves, of a model of this + # count, that a total within the limit is the expanded size and that a + # document within the limit is passed. This holds the Elixir count to that + # model's `size` on every tree of a small domain: scalars, sequences, + # mappings, and aliases (to a non-alias, as the reader allows) sharing a + # subtree. + test "within_budget?/2 passes exactly the trees whose expanded size is within the limit" do + leaf = %{kind: :string, value: "x"} + seq = &%{kind: :seq, items: &1} + map = fn values -> %{kind: :map, entries: Enum.map(values, &%{key: leaf, value: &1})} end + ali = &%{kind: :alias, target: &1} + + size = fn + size, %{kind: :alias, target: t} -> size.(size, t) + size, %{kind: :seq, items: items} -> 1 + Enum.sum(Enum.map(items, &size.(size, &1))) + size, %{kind: :map, entries: es} -> 1 + Enum.sum(Enum.map(es, &size.(size, &1.value))) + _, _ -> 1 + end + + grow = fn trees -> + non_alias = Enum.reject(trees, &(&1.kind == :alias)) + lists = [[]] ++ for(a <- trees, do: [a]) ++ for(a <- trees, b <- trees, do: [a, b]) + trees ++ Enum.map(non_alias, ali) ++ Enum.map(lists, seq) ++ Enum.map(lists, map) + end + + trees = [leaf] |> grow.() |> grow.() |> Enum.uniq() + assert length(trees) > 150 + + mismatches = + for t <- trees, + n = size.(size, t), + limit <- 0..(n + 1), + Kyaml.within_budget?(t, limit) != n <= limit, + do: {t, limit} + + assert mismatches == [] + end + test "within_budget?/2 stops counting at the limit (the billion-laughs document)" do anchors = for i <- 1..9 do diff --git a/tests/accept/DeclaredJobIsClean.idr b/tests/accept/DeclaredJobIsClean.idr new file mode 100644 index 00000000..945ae72e --- /dev/null +++ b/tests/accept/DeclaredJobIsClean.idr @@ -0,0 +1,42 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- POSITIVE CONTROL (ADR-009 egress). The counterpart of the three egress +-- rejections: hypatia's own push-email-notify job, declared in +-- hypatia_chora.deed with the secrets it reads and harden-runner-block, run +-- with a blocking hardener, is accepted; and the decision procedure says so +-- by evaluation. test/egress_decision_mirror_test.exs runs the Elixir rule +-- on the same decision. + +module DeclaredJobIsClean + +import Data.List.Elem +import Data.List.Quantifiers +import Decidable.Decidable +import Hypatia.ABI.Egress + +%default total + +notify : Job +notify = MkJob ["SMTP_HOST", "SMTP_PASS", "SMTP_PORT", "SMTP_USER"] False (Just Block) + +declaration : Decl +declaration = MkDecl ["SMTP_HOST", "SMTP_PORT", "SMTP_USER", "SMTP_PASS"] HardenRunnerBlock + +-- The order of the list does not matter: each read secret is found in the +-- declaration, and each declared one among the reads. +clean : Clean DeclaredJobIsClean.notify (Just DeclaredJobIsClean.declaration) +clean = Declared ([Here, There (There (There Here)), There Here, There (There Here)], + [Here, There (There Here), There (There (There Here)), There Here]) + Blocking + +-- The decision procedure agrees, by evaluation. +decides : isYes (decClean DeclaredJobIsClean.notify (Just DeclaredJobIsClean.declaration)) = True +decides = Refl + +-- And it refuses the same job running its hardener in audit mode. +auditing : Job +auditing = MkJob ["SMTP_HOST", "SMTP_PASS", "SMTP_PORT", "SMTP_USER"] False (Just Audit) + +refusesAudit : isYes (decClean DeclaredJobIsClean.auditing (Just DeclaredJobIsClean.declaration)) = False +refusesAudit = Refl diff --git a/tests/reject/AuditPassesAsBlock.idr b/tests/reject/AuditPassesAsBlock.idr new file mode 100644 index 00000000..7c319516 --- /dev/null +++ b/tests/reject/AuditPassesAsBlock.idr @@ -0,0 +1,26 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- EXPECTED REJECTION (ADR-009 egress). scripts/check-verdicts.sh passes only +-- if Idris2 refuses this module, and only at the declaration `invalid`. +-- +-- Must fail: a hardener that only audits is offered as satisfying a +-- `harden-runner-block` claim. `Blocking` is indexed by `Just Block`, so it +-- does not unify with the job's `Just Audit` (the #975 shape, where a +-- `name: |` text was read as the hardener's input). +-- +-- EXPECT: Mismatch between: Block and Audit. + +module AuditPassesAsBlock + +import Data.List.Elem +import Data.List.Quantifiers +import Hypatia.ABI.Egress + +%default total + +same : SameSecrets ["SMTP_PASS"] ["SMTP_PASS"] +same = ([Here], [Here]) + +invalid : Clean (MkJob ["SMTP_PASS"] False (Just Audit)) (Just (MkDecl ["SMTP_PASS"] HardenRunnerBlock)) +invalid = Declared same Blocking diff --git a/tests/reject/DynamicKeyDeclared.idr b/tests/reject/DynamicKeyDeclared.idr new file mode 100644 index 00000000..bc5cb3ca --- /dev/null +++ b/tests/reject/DynamicKeyDeclared.idr @@ -0,0 +1,25 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- EXPECTED REJECTION (ADR-009 egress). scripts/check-verdicts.sh passes only +-- if Idris2 refuses this module, and only at the declaration `invalid`. +-- +-- Must fail: the job computes a secret's key at run time (`secrets[env.X]`), +-- which no fixed list can name, yet a declaration is offered as covering it. +-- `Declared` is indexed by a job whose `dynamic` is `False`. +-- +-- EXPECT: Mismatch between: False and True. + +module DynamicKeyDeclared + +import Data.List.Elem +import Data.List.Quantifiers +import Hypatia.ABI.Egress + +%default total + +same : SameSecrets ["DEPLOY_KEY"] ["DEPLOY_KEY"] +same = ([Here], [Here]) + +invalid : Clean (MkJob ["DEPLOY_KEY"] True (Just Block)) (Just (MkDecl ["DEPLOY_KEY"] None)) +invalid = Declared same ClaimsNothing diff --git a/tests/reject/UndeclaredSecretPasses.idr b/tests/reject/UndeclaredSecretPasses.idr new file mode 100644 index 00000000..e829095a --- /dev/null +++ b/tests/reject/UndeclaredSecretPasses.idr @@ -0,0 +1,23 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- EXPECTED REJECTION (ADR-009 egress). scripts/check-verdicts.sh passes only +-- if Idris2 refuses this module, and only at the declaration `invalid`. +-- +-- Must fail: the job reads TOKEN, which the declaration does not list. The +-- only membership offered for it points at the declared SMTP_PASS, which is a +-- different secret, so the evidence that every read secret is declared +-- cannot be built. +-- +-- EXPECT: Mismatch between: "SMTP_PASS" and "TOKEN". + +module UndeclaredSecretPasses + +import Data.List.Elem +import Data.List.Quantifiers +import Hypatia.ABI.Egress + +%default total + +invalid : Clean (MkJob ["SMTP_PASS", "TOKEN"] False (Just Block)) (Just (MkDecl ["SMTP_PASS"] None)) +invalid = Declared ([Here, Here], [Here]) ClaimsNothing diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index ea95851c..abaf4cf3 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -294,6 +294,87 @@ the Signalbox criterion has no Signalbox repository to apply to |TESTED (Signalbox: OPEN) |=== +==== Egress declarations and the KYAML reader (2026-11-09, standards ADR-009, #971) + +RE001 accepts a secret-bearing job that runs harden-runner or that the repo +deed declares truthfully. The decision is modelled and proved in Idris2, +and the Elixir rule is held to the model case by case. The workflow reader +under it (`+Hypatia.Kyaml+`, kyq's KYAML reader ported) has its alias +budget modelled and proved; the reader as a whole is tested, not proved. +Gates: `+scripts/check-verdicts.sh+` (the ABI package and the fixtures), +the `+idris2 --check+` loop over `+verification/proofs/idris2/+`, and the +Elixir suite. + +[width="100%",cols="28%,14%,42%,16%",options="header",] +|=== +|File |Language |Claim |Status +|`+src/Hypatia/ABI/Egress.idr+` |Idris2 |`+Clean+` is RE001's +acceptance of a job with a declaration or none, and it is decidable +(`+decClean+`). An audit-mode hardener never satisfies a block claim +(`+auditNeverBlock+`); a declaration lists exactly the secrets read +(`+readSecretDeclared+`, `+declaredSecretRead+`); a key computed at run +time is never declared (`+dynamicNeverDeclared+`); a job with neither a +hardener nor a declaration fails (`+bareJobFails+`); a claimed +enforcement needs a hardener (`+claimNeedsHardener+`). Endpoints are +outside the model |PROVEN + +|`+tests/reject/AuditPassesAsBlock.idr+` |Idris2 |Expected rejection: a +job whose hardener audits is refused as `+Clean+` under a block claim, +at `+invalid+` |TESTED + +|`+tests/reject/UndeclaredSecretPasses.idr+` |Idris2 |Expected +rejection: a declaration that omits a secret the job reads is refused, +at `+invalid+` |TESTED + +|`+tests/reject/DynamicKeyDeclared.idr+` |Idris2 |Expected rejection: a +job reading a key computed at run time is refused as declared, at +`+invalid+` |TESTED + +|`+tests/accept/DeclaredJobIsClean.idr+` |Idris2 |Positive control: a +truthful declaration is `+Clean+` (`+clean+`), the decision procedure +says so by evaluation (`+decides+`), and refuses the same declaration +for an auditing job (`+refusesAudit+`) |TESTED + +|Runtime mirror, lib/rules/research_extensions.ex |Elixir |RE001 reports +a job exactly when `decClean` refuses it, on all 240 cases of a small +domain (one or two secrets, a run-time key or none, four hardener +settings, no declaration or nine): test/egress_decision_mirror_test.exs, +with the deed parse asserted per case and three mutants killed (two in +the transcription, one in RE001's block check) |TESTED + +|Endpoint comparison, lib/rules/research_extensions.ex |Elixir |Declared +endpoints agree with the hosts a job names and with its hardener's +`allowed-endpoints`: test/research_extensions_test.exs. Not modelled +|OPEN + +|`+verification/proofs/idris2/KyamlBudget.idr+` |Idris2 |A model of +`within_budget?/2` step for step (`+count+`, `+stepCount+`). A total +within the limit is the document's exact size with every alias read +through (`+countSound+`, `+withinBudgetSound+`); a document within the +limit is passed (`+countAtMost+`, `+withinBudgetComplete+`); with no +alias naming an alias, the count answers within 2 · (limit + 1) + 2 +steps however far the aliases expand (`+countBounded+`) |PROVEN + +|Runtime mirror, lib/hypatia/kyaml.ex |Elixir |`within_budget?/2` passes +exactly the trees whose expanded size is within the limit, on 154 trees +(scalars, sequences, mappings, shared aliases) at every limit from 0 to +size + 1: test/kyaml_test.exs, with a mutant that stops expanding aliases +killed; the billion-laughs document is refused in under 5 s |TESTED + +|Refusal, not guessing, lib/hypatia/kyaml.ex |Elixir |`parse/1` returns +`{:ok, docs}` or a located `{:error, %Error{}}`: on kyq's 46-case +conformance corpus (test/kyaml_conformance_test.exs), against kyq's own +parse of its fixtures and this repository's workflows (`kyq_differential`, +at the pinned `KYQ_REF`), and on the YAML test suite, where no invalid +stream is accepted and every valid stream read matches its `in.json` +(test/kyaml_yaml_test_suite_test.exs). Bounded by those corpora; no +totality proof |TESTED + +|lib/hypatia/workflow.ex |Elixir |GitHub Actions reads a workflow file as +YAML 1.2 Core reads it, for the shapes KYAML admits. GitHub's parser is +third-party and is not re-proved |ASSUMED +|=== + === Properties Proven ==== 1. Confidence Bounds (`+ConfidenceBounds.idr+`) @@ -454,6 +535,12 @@ AGDA-VERIFIED (receipt above); fix text and runtime refinement excluded |Neural ensemble aggregation |`+NeuralConsensus.idr+` |Full (bounds + min-lower-bound) +|RE001 egress decision (ADR-009) |`+Egress.idr+` |Decision proved; +Elixir held to it on a small domain; endpoints not modelled + +|KYAML alias budget |`+KyamlBudget.idr+` |Model proved; Elixir held to +it on a small domain; the reader as a whole is tested, not proved + |VCL parser totality |`+ParserTotality.lean+` |Full (FROM-clause subset) |VCL query correctness |- |Partial diff --git a/verification/proofs/idris2/KyamlBudget.idr b/verification/proofs/idris2/KyamlBudget.idr new file mode 100644 index 00000000..cebab381 --- /dev/null +++ b/verification/proofs/idris2/KyamlBudget.idr @@ -0,0 +1,268 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Hypatia.Kyaml's node budget (`within_budget?/2`, lib/hypatia/kyaml.ex): +-- the count that refuses a document whose aliases expand past kyq's +-- NODE_BUDGET (the "billion laughs" document), modelled step for step. +-- +-- count(_, n, limit) when n > limit -> n +-- count([], n, _) -> n +-- count([alias | rest], n, limit) -> count([target | rest], n, limit) +-- count([map | rest], n, limit) -> count(values ++ rest, n + 1, limit) +-- count([seq | rest], n, limit) -> count(items ++ rest, n + 1, limit) +-- count([_ | rest], n, limit) -> count(rest, n + 1, limit) +-- +-- within_budget?(node, limit) = count([node], 0, limit) <= limit +-- +-- A mapping is modelled by its values (the count never visits a key), so a +-- map and a sequence are both `Coll`. An alias holds its target, so a +-- shared subtree is counted once per alias, as the Elixir code counts it. +-- The model takes an explicit number of steps (`fuel`); `Nothing` means +-- the steps ran out. +-- +-- Theorems: +-- +-- * `withinBudgetSound`: a total within the limit is the exact size of +-- the document with every alias read through. `within_budget?` never +-- passes a document that expands past the limit. +-- * `withinBudgetComplete`: a document whose expanded size is within the +-- limit is passed, with that size. +-- * `countBounded`: when no alias names another alias (the reader refuses +-- an anchored alias, ALIAS_DECORATED), the count answers within +-- 2 * (limit + 1) + 2 steps, however far the aliases expand. This is the +-- bound on work that makes the anchor bomb cheap to refuse. +-- +-- This is a model of the algorithm, not a refinement proof of the Elixir +-- function. The function is held to the model by test/kyaml_test.exs and +-- test/workflow_test.exs (the anchor bomb refused at its first line). + +module KyamlBudget + +import public Data.Nat +import Data.Maybe + +%default total + +||| A node of a parsed document: a scalar, a collection (a sequence's items +||| or a mapping's values), or an alias to an earlier node. +public export +data Node = Leaf | Coll (List Node) | Alias Node + +mutual + ||| The size of a node with every alias read through. + public export + size : Node -> Nat + size Leaf = 1 + size (Coll cs) = S (sizes cs) + size (Alias t) = size t + + public export + sizes : List Node -> Nat + sizes [] = 0 + sizes (x :: xs) = size x + sizes xs + +mutual + ||| `count/3`, one step per call. + public export + count : (fuel : Nat) -> (limit : Nat) -> (stack : List Node) -> (n : Nat) -> Maybe Nat + count Z _ _ _ = Nothing + count (S f) limit stack n = stepCount f limit stack n (lte n limit) + + ||| One clause of `count/3`, given whether the total so far is within the limit. + public export + stepCount : Nat -> Nat -> List Node -> Nat -> Bool -> Maybe Nat + stepCount f limit stack n False = Just n + stepCount f limit [] n True = Just n + stepCount f limit (Leaf :: r) n True = count f limit r (S n) + stepCount f limit (Coll cs :: r) n True = count f limit (cs ++ r) (S n) + stepCount f limit (Alias t :: r) n True = count f limit (t :: r) n + +-- ─── What the count reports ──────────────────────────────────────────── + +justInj : Just a = Just b -> a = b +justInj Refl = Refl + +lteTrans : LTE a b -> LTE b c -> LTE a c +lteTrans LTEZero _ = LTEZero +lteTrans (LTESucc x) (LTESucc y) = LTESucc (lteTrans x y) + +sizesAppend : (xs, ys : List Node) -> sizes (xs ++ ys) = sizes xs + sizes ys +sizesAppend [] ys = Refl +sizesAppend (x :: xs) ys = + rewrite sizesAppend xs ys in plusAssociative (size x) (sizes xs) (sizes ys) + +||| A total that failed the limit check does not fit under the limit. +overLimit : (n, limit : Nat) -> lte n limit = False -> LTE n limit -> Void +overLimit Z _ prf _ = absurd prf +overLimit (S n) Z _ bad = absurd bad +overLimit (S n) (S limit) prf (LTESucc le) = overLimit n limit prf le + +||| A total within the limit is what was counted so far plus the expanded +||| size of everything still on the stack. +export +countSound : (f, limit, n : Nat) -> (stack : List Node) -> + count f limit stack n = Just k -> LTE k limit -> + k = n + sizes stack +countSound Z _ _ _ prf _ = absurd prf +countSound (S f) limit n stack prf within with (lte n limit) proof check + countSound (S f) limit n [] prf within | True = + rewrite plusZeroRightNeutral n in sym (justInj prf) + countSound (S f) limit n (Leaf :: r) prf within | True = + rewrite countSound f limit (S n) r prf within in + plusSuccRightSucc n (sizes r) + countSound (S f) limit n (Coll cs :: r) prf within | True = + rewrite countSound f limit (S n) (cs ++ r) prf within in + rewrite sizesAppend cs r in + plusSuccRightSucc n (sizes cs + sizes r) + countSound (S f) limit n (Alias t :: r) prf within | True = + countSound f limit n (t :: r) prf within + countSound (S f) limit n stack prf within | False = + absurd (overLimit n limit check (rewrite justInj prf in within)) + +||| Whatever the count reports never exceeds the full total. +export +countAtMost : (f, limit, n : Nat) -> (stack : List Node) -> + count f limit stack n = Just k -> LTE k (n + sizes stack) +countAtMost Z _ _ _ prf = absurd prf +countAtMost (S f) limit n stack prf with (lte n limit) proof check + countAtMost (S f) limit n [] prf | True = + rewrite sym (justInj prf) in lteAddRight n + countAtMost (S f) limit n (Leaf :: r) prf | True = + rewrite sym (plusSuccRightSucc n (sizes r)) in countAtMost f limit (S n) r prf + countAtMost (S f) limit n (Coll cs :: r) prf | True = + rewrite sym (plusSuccRightSucc n (sizes cs + sizes r)) in + rewrite sym (sizesAppend cs r) in + countAtMost f limit (S n) (cs ++ r) prf + countAtMost (S f) limit n (Alias t :: r) prf | True = + countAtMost f limit n (t :: r) prf + countAtMost (S f) limit n stack prf | False = + rewrite sym (justInj prf) in lteAddRight n + +||| `within_budget?`: a total within the limit is the document's exact +||| expanded size. +export +withinBudgetSound : (f, limit : Nat) -> (doc : Node) -> + count f limit [doc] 0 = Just k -> LTE k limit -> + k = size doc +withinBudgetSound f limit doc prf within = + rewrite countSound f limit 0 [doc] prf within in plusZeroRightNeutral (size doc) + +||| `within_budget?`: a document that expands to no more than the limit is +||| passed, and its total is its size. +export +withinBudgetComplete : (f, limit : Nat) -> (doc : Node) -> + LTE (size doc) limit -> + count f limit [doc] 0 = Just k -> + (LTE k limit, k = size doc) +withinBudgetComplete f limit doc small prf = + let atMost = replace {p = LTE k} (plusZeroRightNeutral (size doc)) + (countAtMost f limit 0 [doc] prf) + within = lteTrans atMost small + in (within, withinBudgetSound f limit doc prf within) + +-- ─── Bounded work ────────────────────────────────────────────────────── + +||| A node that is not an alias. +public export +data NotAlias : Node -> Type where + LeafIsNot : NotAlias Leaf + CollIsNot : NotAlias (Coll cs) + +mutual + ||| No alias names another alias, at any depth (the reader's ALIAS_DECORATED). + public export + data NoChain : Node -> Type where + LeafOk : NoChain Leaf + CollOk : Each cs -> NoChain (Coll cs) + AliasOk : NotAlias t -> NoChain t -> NoChain (Alias t) + + ||| Every node of a list. + public export + data Each : List Node -> Type where + Nil : Each [] + (::) : NoChain x -> Each xs -> Each (x :: xs) + +eachAppend : Each xs -> Each ys -> Each (xs ++ ys) +eachAppend [] ys = ys +eachAppend (x :: xs) ys = x :: eachAppend xs ys + +||| One extra step is owed while an alias sits on top of the stack. +public export +aliasOnTop : List Node -> Nat +aliasOnTop (Alias _ :: _) = 1 +aliasOnTop _ = 0 + +aliasOnTopBit : (s : List Node) -> LTE (aliasOnTop s) 1 +aliasOnTopBit (Alias _ :: _) = LTESucc LTEZero +aliasOnTopBit [] = LTEZero +aliasOnTopBit (Leaf :: _) = LTEZero +aliasOnTopBit (Coll _ :: _) = LTEZero + +notAliasOnTop : NotAlias t -> aliasOnTop (t :: r) = 0 +notAliasOnTop LeafIsNot = Refl +notAliasOnTop CollIsNot = Refl + +||| The steps owed with `m` counts left before the limit is passed. +public export +steps : (m : Nat) -> List Node -> Nat +steps m stack = S (m + m + aliasOnTop stack) + +lteSuccFalse : (l : Nat) -> lte (S l) l = False +lteSuccFalse Z = Refl +lteSuccFalse (S l) = lteSuccFalse l + +||| With no counts left, the total is past the limit. +noRoom : (n, limit : Nat) -> n + 0 = S limit -> lte n limit = True -> Void +noRoom n limit room check = + let nIs = trans (sym (plusZeroRightNeutral n)) room + isFalse : (lte n limit = False) = rewrite nIs in lteSuccFalse limit + in absurd (trans (sym check) isFalse) + +||| A counting step pays for itself and for an alias it may expose. +afterCount : (m, a, f : Nat) -> LTE a 1 -> LTE (S m + S m + 0) f -> + LTE (S (m + m + a)) f +afterCount m a f bit enough = + lteTrans (LTESucc (replace {p = LTE (m + m + a)} (plusCommutative (m + m) 1) + (plusLteMonotoneLeft (m + m) a 1 bit))) + (replace {p = \x => LTE x f} + (trans (plusZeroRightNeutral (S m + S m)) (cong S (sym (plusSuccRightSucc m m)))) + enough) + +||| An alias step pays for itself and leaves no alias on top. +afterAlias : (m, f : Nat) -> LTE (m + m + 1) f -> LTE (S (m + m + 0)) f +afterAlias m f enough = + rewrite plusZeroRightNeutral (m + m) in + replace {p = \x => LTE x f} (plusCommutative (m + m) 1) enough + +||| With `m` counts left (`n + m = S limit`), the count answers within +||| `steps m stack` steps. +countFinishes : (m, n, limit : Nat) -> n + m = S limit -> + (stack : List Node) -> Each stack -> + (f : Nat) -> LTE (steps m stack) f -> + IsJust (count f limit stack n) +countFinishes m n limit room stack ok Z enough = absurd enough +countFinishes m n limit room stack ok (S f) enough with (lte n limit) proof check + countFinishes m n limit room [] ok (S f) enough | True = ItIsJust + countFinishes Z n limit room (_ :: _) ok (S f) enough | True = + absurd (noRoom n limit room check) + countFinishes (S m) n limit room (Leaf :: r) (_ :: ok) (S f) enough | True = + countFinishes m (S n) limit (trans (plusSuccRightSucc n m) room) r ok f + (afterCount m (aliasOnTop r) f (aliasOnTopBit r) (fromLteSucc enough)) + countFinishes (S m) n limit room (Coll cs :: r) (CollOk inner :: ok) (S f) enough | True = + countFinishes m (S n) limit (trans (plusSuccRightSucc n m) room) (cs ++ r) + (eachAppend inner ok) f + (afterCount m (aliasOnTop (cs ++ r)) f (aliasOnTopBit (cs ++ r)) (fromLteSucc enough)) + countFinishes m n limit room (Alias t :: r) (AliasOk notAlias inner :: ok) (S f) enough | True = + countFinishes m n limit room (t :: r) (inner :: ok) f + (rewrite notAliasOnTop {r} notAlias in afterAlias m f (fromLteSucc enough)) + countFinishes m n limit room stack ok (S f) enough | False = ItIsJust + +||| `within_budget?` on a document without alias chains answers within +||| 2 * (limit + 1) + 2 steps, however far its aliases expand. +export +countBounded : (limit : Nat) -> (doc : Node) -> NoChain doc -> + IsJust (count (S (S limit + S limit + 1)) limit [doc] 0) +countBounded limit doc ok = + countFinishes (S limit) 0 limit Refl [doc] [ok] (S (S limit + S limit + 1)) + (LTESucc (plusLteMonotoneLeft (S limit + S limit) (aliasOnTop [doc]) 1 + (aliasOnTopBit [doc]))) From 697ff016a275b6e663699f7b702cd509afe9d5fa Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:43:00 +0000 Subject: [PATCH 03/14] =?UTF-8?q?Write=20Proof=20Witness=20Grades=20as=20P?= =?UTF-8?q?ROOF-POLICY=20=C2=A78=20requires?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The ledger cited the Mathesis architecture brief's grade ladder and wrote bare "Grade 3". PROOF-POLICY §8 (owner ruling 2026-11-04) supersedes that ladder and forbids a bare grade in a ledger: a grade is written PWG-3, PWG-2i, PWG-2ii or PWG-1, applies to theory (Agda) proofs only, and is not a status. The LogtalkMigration.agda receipt is now "PROVEN, PWG-3" in PROOF-STATUS.adoc, verification/README.adoc and docs/rules/logtalk-migration.adoc. No claim is raised or lowered. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- docs/rules/logtalk-migration.adoc | 25 +++++++++++-------------- verification/PROOF-STATUS.adoc | 31 ++++++++++++++++--------------- verification/README.adoc | 2 +- 3 files changed, 28 insertions(+), 30 deletions(-) diff --git a/docs/rules/logtalk-migration.adoc b/docs/rules/logtalk-migration.adoc index f30a980e..a2add596 100644 --- a/docs/rules/logtalk-migration.adoc +++ b/docs/rules/logtalk-migration.adoc @@ -583,16 +583,13 @@ evidence, not a standards-gate receipt. [[proofing]] == Proofing: policy, grades, and exact statuses -Proofing follows hyperpolymath/mathesis' -`estate-mathematical-architecture` (§§5–6) for grades and -metadatastician/standards `3-practice/PROOF-POLICY.adoc` for evidence -discipline; everything else follows the standards repo. In Mathesis' -ladder, *Grade 3* means the statement is formulated in Agda and -type-checks under the strict profile; Grade 2 additionally requires -translation into independent foundational system(s); Grade 1 -additionally requires those witnesses to compile in headless isolated -CI through verified checker APIs. Statuses are recorded exactly -(Open / Claimed / AGDA-PENDING / Grade 3 / …), never as a percentage, +Proofing follows metadatastician/standards `3-practice/PROOF-POLICY.adoc`: +§5 for status tokens and §8 for Proof Witness Grades (owner ruling +2026-11-04, which supersedes the ladder of the Mathesis architecture +brief). `PWG-3` means the Agda proof is checked under the §2.1 +invocation; `PWG-2i` adds one counted Rocq or Lean recheck leg and +`PWG-2ii` both; `PWG-1` adds a current per-commit receipt for every +witness. Statuses and grades are recorded exactly, never as a percentage, and a checked model never silently becomes a runtime-refinement or reconciliation claim. @@ -609,7 +606,7 @@ exactly |`verification/proofs/agda/LogtalkMigration.agda` (`categoriesAgree`, `severitiesAgree`, `autoFixableAgrees`, `fixPresenceAgrees`, `prevention*`, `catchAll*Low`) -|*Grade 3 — AGDA-VERIFIED.* Receipt recorded in +|*PROVEN, `PWG-3`.* Receipt recorded in `verification/PROOF-STATUS.adoc`: official pinned Agda 2.8.0.2 Linux release (builtins only, no stdlib), invocation `agda --safe --without-K --cubical-compatible LogtalkMigration.agda`, success in @@ -617,7 +614,7 @@ Verify Proofs run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e source SHA-256 bbd18e2747c84e2eda7ff5a778a2df7f8960a1ef47b1c253f316b9d97b9902a0. The `agda strict-profile check` job fails hard (never skips) on every -relevant change. No Grade 2/1, Rocq/Lean reconciliation, or Elixir +relevant change. No `PWG-2i`, `PWG-2ii` or `PWG-1`, Rocq/Lean reconciliation, or Elixir runtime-refinement claim is made. |VeriSimDB connector field preservation @@ -706,7 +703,7 @@ sibling repositories from this branch): coordinated. ✓ (landing: siblings) * Repository guard against new active `.lgt` files / Logtalk output settings, exact-path shrink-only allowlist, wired into CI. ✓ -* Proofing graded honestly: finite correspondence at Mathesis - *Grade 3 / AGDA-VERIFIED* on the recorded strict-profile Agda +* Proofing graded honestly: finite correspondence PROVEN at + `PWG-3` on the recorded strict-profile Agda receipt; Idris statement supersession recorded and re-checked; no claim inflated beyond its evidence. ✓ diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index abaf4cf3..21f863f2 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -27,15 +27,16 @@ neurosymbolic CI/CD platform. * Canonical estate policy: https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[Proof and Verification Policy]. This file is a proof inventory, not an independent alternative policy. -* Proof *grades* follow hyperpolymath/mathesis, - `+estate-mathematical-architecture+` §§5–6: *Grade 3* is an Agda proof - formulated and type-checking under the strict profile; *Grade 2* - requires translation(s) into independent foundational system(s); - *Grade 1* additionally requires those translated witnesses to compile - in headless, isolated CI via verified checker APIs. A target grade is - not a status. This inventory records exact statuses (Open / Claimed / - `+AGDA-PENDING+` / `+AGDA-VERIFIED+` / Grade 3 …) and never flattens - them into a confidence percentage. +* Proof Witness Grades follow PROOF-POLICY §8 (owner ruling 2026-11-04, + which supersedes the grade ladder of the Mathesis architecture brief): + `PWG-3` is an Agda proof checked under the §2.1 invocation; `PWG-2i` adds + one counted Rocq or Lean recheck leg, `PWG-2ii` both; `PWG-1` adds a + current per-commit receipt for every witness. A grade is always written + with its `PWG-` prefix. Grades apply to theory (Agda) proofs only: + Idris2, Lean-only and TLA+ engineering proofs carry the §5 status + tokens (PROVEN / PROVEN-WITH-AXIOMS / TESTED / ASSUMED / OPEN) and no + grade. A grade is not a status, and this inventory never flattens + either into a confidence percentage. * A checked model proves its stated proposition only. In particular it does not prove runtime refinement of Elixir/BEAM code; such claims need their own correspondence evidence and tests. @@ -170,7 +171,7 @@ JSONL for violations. See commit history. Finite, implementation-independent table correspondence for the retired ECHIDNA `+security_learning.lgt+` alert semantics versus `+Hypatia.Rules.SecurityErrors+`. Per the estate verifier mapping this -is Agda territory; per Mathesis this is now *Grade 3* on the +is Agda territory; under PROOF-POLICY §8 this is `PWG-3` on the strict-profile receipt recorded in the row below (checker version, library discipline, exact invocation, result, source digest, and verification commit). Fix *strings* and Elixir @@ -190,10 +191,10 @@ entries; the two ledgered non-equalities stated exactly former severity catch-all members explicit (`+catchAllSastLow+`, `+catchAllCiTestsLow+`, `+catchAllUnmaintainedLow+`). Source SHA-256 (at authoring): bbd18e2747c84e2eda7ff5a778a2df7f8960a1ef47b1c253f316b9d97b9902a0. -|Grade 3 — AGDA-VERIFIED. Receipt: official pinned Agda 2.8.0.2 Linux +|PROVEN, `PWG-3`. Receipt: official pinned Agda 2.8.0.2 Linux release, builtins only/no stdlib; invocation `agda --safe --without-K --cubical-compatible LogtalkMigration.agda`; success in Verify Proofs -run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331. No Grade 2/1, +run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331. No `PWG-2i`, `PWG-2ii` or `PWG-1`, reconciliation, or runtime-refinement claim. |=== @@ -459,7 +460,7 @@ rejected ==== 8. Logtalk Migration Correspondence (`+LogtalkMigration.agda+`) -Status for all of P8: *Grade 3 — AGDA-VERIFIED* on the strict-profile +Status for all of P8: *PROVEN, `PWG-3`* on the strict-profile receipt in the inventory row above (Agda 2.8.0.2, Verify Proofs run 41328302925, job 124912804344, commit 4018290eaa3265b82209e2a45b6917a4bb0a0331). This grades the finite model only. @@ -529,8 +530,8 @@ model only. superseded 2026-11-01) |Logtalk → Elixir alert-table correspondence -|`+LogtalkMigration.agda+` |Finite model only — Grade 3 / -AGDA-VERIFIED (receipt above); fix text and runtime refinement excluded +|`+LogtalkMigration.agda+` |Finite model only — PROVEN, `PWG-3` +(receipt above); fix text and runtime refinement excluded |Neural ensemble aggregation |`+NeuralConsensus.idr+` |Full (bounds + min-lower-bound) diff --git a/verification/README.adoc b/verification/README.adoc index 6cb675c1..471a7c59 100644 --- a/verification/README.adoc +++ b/verification/README.adoc @@ -9,7 +9,7 @@ Idris2, Lean 4, TLA+ and Agda proof sources for Hypatia's type-level guarantees. normative ABI in `src/Hypatia/ABI/` * `proofs/lean4/`, `proofs/tlaplus/` — Lean 4 and TLA+ proofs * `proofs/agda/` — Agda correspondence model for the Logtalk → Elixir - rule migration (`LogtalkMigration.agda`; Mathesis Grade 3 receipt in + rule migration (`LogtalkMigration.agda`; `PWG-3` receipt in `PROOF-STATUS.adoc`) * `PROOF-STATUS.adoc` — Current proof completion status From 7529763d337281d4831c8620084f060dcc23abda Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:04:40 +0000 Subject: [PATCH 04/14] CHANGELOG: blank line before the #971 entry heading, so AsciiDoc renders it Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- CHANGELOG.adoc | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 4b1ff5d8..3bdaf110 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -30,6 +30,7 @@ sequence is read (its harden-runner step counts), and a step opened by `-` and a comment keeps its `run:`. WH014 reads each job's steps through the same reader. On the hypatia, echidna and standards trees, WH013, WH014 and RE001 report exactly what they did before. + ==== One parsed workflow model; RE001 and RE002 read it (#971) (2026-11-09) `Hypatia.Workflow` is #971's model: each workflow is parsed once by From 5bef2ca670a793ba9abc04ec5930396accb52f6b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:29:29 +0000 Subject: [PATCH 05/14] Kyaml: refuse an alias that carries a property from the line above `b: &b` followed by ` *a` was read as an anchor on an alias. The bare property's next-line value is the node itself, so it is ALIAS_DECORATED exactly as `b: &b *a` is. Accepting it let aliases chain, and a chain costs within_budget?/2 no count per link: KyamlBudget.idr's work bound assumes no alias names an alias (NoChain), which this restores for every document the reader accepts. Same fix as metadatastician/kyq#22. Tests: three refusals (mapping value, tag, root) fail on the previous reader; a bare anchor followed by a sibling alias still reads. Parity with kyq: 488 of 488 files; the YAML test suite still passes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- lib/hypatia/kyaml.ex | 22 ++++++++++++++++------ test/kyaml_test.exs | 10 ++++++++++ 2 files changed, 26 insertions(+), 6 deletions(-) diff --git a/lib/hypatia/kyaml.ex b/lib/hypatia/kyaml.ex index 783edfe5..1cf1c704 100644 --- a/lib/hypatia/kyaml.ex +++ b/lib/hypatia/kyaml.ex @@ -914,7 +914,7 @@ defmodule Hypatia.Kyaml do {anchor, tag, s} = node_properties(s, at, anchor0, tag0, &skip_blanks/1) bounds = {indent, line_indent, seq_at} - case continued_properties(s, anchor, tag, context, bounds) do + case continued_properties(s, at, anchor, tag, context, bounds) do {:continue, s} -> parse_inline_node(s, indent, path, context, line_indent, {anchor, tag}, seq_at) @@ -927,16 +927,26 @@ defmodule Hypatia.Kyaml do # properties on the next line (`a: &x` then ` !!str v`): they are the same # node's, so they go through the same one-anchor, one-tag check rather than # starting a fresh node that the outer properties would then overwrite. - defp continued_properties(s, anchor, tag, context, {indent, _, _} = bounds) do + # + # An alias on that next line is the node itself (`a: &b` then ` *c`), so + # it carries the anchor or tag as surely as `a: &b *c` does, and is + # refused the same way. Left alone it would register `b` as an alias of + # `c`, and chains of such aliases cost the node budget nothing per link. + defp continued_properties(s, at, anchor, tag, context, {indent, _, _} = bounds) do if (anchor != nil or tag != nil) and (eof?(s) or peek(s) in [?\n, ?#]) do next = skip_gap(s) inside? = - if context == :root, - do: not enclosing_line?(next, bounds), - else: next.col - 1 > indent + not eof?(next) and + if(context == :root, + do: not enclosing_line?(next, bounds), + else: next.col - 1 > indent + ) + + if inside? and peek(next) == ?*, + do: throw_error("ALIAS_DECORATED", "an alias may not carry an anchor or a tag", at) - if not eof?(next) and peek(next) in [?&, ?!] and not property_key?(next) and inside?, + if inside? and peek(next) in [?&, ?!] and not property_key?(next), do: {:continue, next}, else: :none else diff --git a/test/kyaml_test.exs b/test/kyaml_test.exs index 84e6725c..be829d81 100644 --- a/test/kyaml_test.exs +++ b/test/kyaml_test.exs @@ -207,6 +207,16 @@ defmodule Hypatia.KyamlTest do {"anchored-first-key-refused", "&k a: 1\n", {:error, "KEY_PROPERTY", 1, 1, ""}}, {"flow-tagged-key-refused", "x: {!!str a: 1}\n", {:error, "KEY_PROPERTY", 1, 5, ""}}, {"flow-alias-decorated", "a: &a 1\nb: [!!int *a]\n", {:error, "ALIAS_DECORATED", 2, 5, ""}}, + # A bare property's value on the next line is the node itself: an alias + # there carries the property as surely as on the same line, and would + # otherwise chain aliases past the node budget's per-step count. + {"alias-decorated-next-line", "a: &a [x]\nb: &b\n *a\n", + {:error, "ALIAS_DECORATED", 2, 4, ""}}, + {"alias-tagged-next-line", "a: &a x\nb: !!str\n *a\n", + {:error, "ALIAS_DECORATED", 2, 4, ""}}, + {"root-alias-decorated-next-line", "&b\n*a\n", {:error, "ALIAS_DECORATED", 1, 1, ""}}, + {"bare-anchor-then-sibling-alias", "a: &a x\nb: &b\nc: *a\n", + {:ok, %{"a" => "x", "b" => nil, "c" => "x"}}}, # The printable set (YAML 1.2 c-printable) is checked over the whole # stream, so the error stands at the character, wherever it is. {"control-character-in-plain", "a: x\u0001y\n", {:error, "CONTROL_CHARACTER", 1, 5, ""}}, From 46cb0a11c1e6d9721f5475841c6fc7f0f8523e6d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:39:07 +0000 Subject: [PATCH 06/14] Kyaml: next-line values measured from their parent; complete ns-plain-first The same two fixes as metadatastician/kyq#22, so the readers stay equal: - A flow collection or block scalar on the line after its key is measured from the block node holding it, as on the key's line: `a:` / ` [x,` / ` y]` and `a:` / ` |` / ` x` now read as YAML reads them. - `[`, `{`, `|` and `>` cannot start a plain scalar, so a later mapping key like `[b]` or `|b` is PLAIN_INDICATOR rather than a string YAML would not produce. Six tests; five fail on the previous reader. Parity with kyq: 488 of 488 files; the YAML test suite still passes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- lib/hypatia/kyaml.ex | 45 ++++++++++++++++++++++++++++---------------- test/kyaml_test.exs | 11 +++++++++++ 2 files changed, 40 insertions(+), 16 deletions(-) diff --git a/lib/hypatia/kyaml.ex b/lib/hypatia/kyaml.ex index 1cf1c704..4b52b59b 100644 --- a/lib/hypatia/kyaml.ex +++ b/lib/hypatia/kyaml.ex @@ -598,14 +598,19 @@ defmodule Hypatia.Kyaml do # `seq_at` is the indentation of the mapping whose value this is, when a # block sequence may sit at that same indentation (YAML 1.2 compact # sequence under a mapping key); otherwise nil. - defp parse_block(s, indent, path, line_indent \\ nil, seq_at \\ nil) do + # + # `floor` is the indentation of the block node that holds this one: a flow + # collection's lines and a block scalar's content are indented past it + # (YAML 1.2 s-flow-line-prefix, s-indent). It defaults to `line_indent`. + defp parse_block(s, indent, path, line_indent \\ nil, seq_at \\ nil, floor \\ nil) do line_indent = line_indent || indent + floor = floor || line_indent cond do eof?(s) -> {null_node(loc(s)), s} seq_entry?(s) -> parse_seq(s, indent, path) map_entry?(s) -> parse_map(s, indent, path) - true -> parse_inline_node(s, indent, path, :root, line_indent, {nil, nil}, seq_at) + true -> parse_inline_node(s, indent, path, :root, line_indent, {nil, nil}, seq_at, floor) end end @@ -839,7 +844,9 @@ defmodule Hypatia.Kyaml do s.col - 1 > parent_indent -> seq_at = if allow_same_indent_seq, do: parent_indent, else: nil - parse_block(s, s.col - 1, path, nil, seq_at) + # A value on the following line is measured from its parent, not from + # its own column, as it would be on the key's line. + parse_block(s, s.col - 1, path, nil, seq_at, parent_indent) allow_same_indent_seq and s.col - 1 == parent_indent and seq_entry?(s) -> parse_seq(s, parent_indent, path) @@ -907,16 +914,18 @@ defmodule Hypatia.Kyaml do context, line_indent, props \\ {nil, nil}, - seq_at \\ nil + seq_at \\ nil, + floor \\ nil ) do + floor = floor || line_indent at = loc(s) {anchor0, tag0} = props {anchor, tag, s} = node_properties(s, at, anchor0, tag0, &skip_blanks/1) - bounds = {indent, line_indent, seq_at} + bounds = {indent, line_indent, seq_at, floor} case continued_properties(s, at, anchor, tag, context, bounds) do {:continue, s} -> - parse_inline_node(s, indent, path, context, line_indent, {anchor, tag}, seq_at) + parse_inline_node(s, indent, path, context, line_indent, {anchor, tag}, seq_at, floor) :none -> parse_inline_content(s, at, anchor, tag, path, context, bounds) @@ -932,7 +941,7 @@ defmodule Hypatia.Kyaml do # it carries the anchor or tag as surely as `a: &b *c` does, and is # refused the same way. Left alone it would register `b` as an alias of # `c`, and chains of such aliases cost the node budget nothing per link. - defp continued_properties(s, at, anchor, tag, context, {indent, _, _} = bounds) do + defp continued_properties(s, at, anchor, tag, context, {indent, _, _, _} = bounds) do if (anchor != nil or tag != nil) and (eof?(s) or peek(s) in [?\n, ?#]) do next = skip_gap(s) @@ -960,13 +969,13 @@ defmodule Hypatia.Kyaml do # root `line_indent` is -1, so every line belongs to the node. A sequence # entry at `seq_at` is the node's own compact sequence (`k:` then ` &a` # then `- x`, yaml-test-suite SKE5). - defp enclosing_line?(s, {indent, line_indent, seq_at}) do + defp enclosing_line?(s, {indent, line_indent, seq_at, _floor}) do s.col - 1 < indent and s.col - 1 <= line_indent and not (seq_at == s.col - 1 and seq_entry?(s)) end defp parse_inline_content(s, at, anchor, tag, path, context, bounds) do - {indent, line_indent, _} = bounds + {indent, _line_indent, _, floor} = bounds if peek(s) == ?* do if anchor != nil or tag != nil, @@ -991,14 +1000,14 @@ defmodule Hypatia.Kyaml do parse_nested_value(s, indent, context == :map_value, path) end - # Content must be indented past the line that carries the indicator. + # Content must be indented past the block node holding the scalar. peek(s) in [?|, ?>] -> - parse_block_scalar(s, line_indent, at) + parse_block_scalar(s, floor, at) # Each line of a flow collection must be indented past the block # node that holds it (YAML 1.2 s-flow-line-prefix). peek(s) in [?{, ?[] -> - {node, s} = parse_flow_node(%{s | flow_min: line_indent + 1}, path) + {node, s} = parse_flow_node(%{s | flow_min: floor + 1}, path) {node, expect_end_of_line(%{s | flow_min: nil})} peek(s) in [?', ?"] -> @@ -1209,9 +1218,11 @@ defmodule Hypatia.Kyaml do defp scalar_from_raw(raw, at, style) do # A plain scalar may not start with an indicator (YAML 1.2 ns-plain-first): - # `@`, `` ` `` and `%` ever, and `-`, `?` or `:` unless a safe character - # follows, so `a: - item` is not the string "- item" (`-1` and `-x` are - # plain scalars). + # `@`, `` ` ``, `%`, `[`, `{`, `|`, `>`, `,`, `]` and `}` ever, and `-`, + # `?` or `:` unless a safe character follows, so `a: - item` is not the + # string "- item" (`-1` and `-x` are plain scalars). A later mapping key + # such as `[b]` or `|b` reaches here as text, and YAML does not read it + # as that string. if plain_indicator_start?(raw), do: throw_error( @@ -1225,7 +1236,9 @@ defmodule Hypatia.Kyaml do %{kind: kind, value: value, raw: raw, loc: at, style: style, segments: []} end - defp plain_indicator_start?(<>) when c in [?@, ?`, ?%, ?,, ?], ?}], do: true + defp plain_indicator_start?(<>) + when c in [?@, ?`, ?%, ?,, ?[, ?], ?{, ?}, ?|, ?>], + do: true defp plain_indicator_start?(<>) when c in [?-, ??, ?:], do: rest == "" or String.first(rest) in [" ", "\t"] diff --git a/test/kyaml_test.exs b/test/kyaml_test.exs index be829d81..785afcd8 100644 --- a/test/kyaml_test.exs +++ b/test/kyaml_test.exs @@ -215,6 +215,17 @@ defmodule Hypatia.KyamlTest do {"alias-tagged-next-line", "a: &a x\nb: !!str\n *a\n", {:error, "ALIAS_DECORATED", 2, 4, ""}}, {"root-alias-decorated-next-line", "&b\n*a\n", {:error, "ALIAS_DECORATED", 1, 1, ""}}, + # A flow collection or block scalar on the line after its key is + # measured from the key's block, not from its own column. + {"next-line-flow-continues-at-own-column", "a:\n [x,\n y]\n", + {:ok, %{"a" => ["x", "y"]}}}, + {"next-line-flow-under-parent-refused", "a:\n [x,\ny]\n", + {:error, "BAD_INDENT", 3, 1, ""}}, + {"next-line-block-scalar-at-own-column", "a:\n |\n x\n", {:ok, %{"a" => "x\n"}}}, + # ns-plain-first: a later key starting with an indicator is not that string. + {"indicator-flow-key-refused", "a: 1\n[b]: 2\n", {:error, "PLAIN_INDICATOR", 2, 1, ""}}, + {"indicator-block-key-refused", "a: 1\n|b: 1\n", {:error, "PLAIN_INDICATOR", 2, 1, ""}}, + {"indicator-in-flow-refused", "x: [>a]\n", {:error, "PLAIN_INDICATOR", 1, 5, ""}}, {"bare-anchor-then-sibling-alias", "a: &a x\nb: &b\nc: *a\n", {:ok, %{"a" => "x", "b" => nil, "c" => "x"}}}, # The printable set (YAML 1.2 c-printable) is checked over the whole From 9c4c9dddaa486375d0024fd6cd6ce33b5c475fd0 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:37:44 +0000 Subject: [PATCH 07/14] KyamlBudget: say what completeness assumes and what the bound counts withinBudgetComplete takes the count returning as a premise: with too little fuel the model returns Nothing, so on its own it cannot show a document is accepted. Yet the header, PROOF-STATUS and the CHANGELOG said an in-budget document "is passed". countBounded bounds calls of count/3, not the work inside one (a mapping's values are copied onto the stack) or allocation, but was described as "the bound on work". withinBudgetPasses composes the two under NoChain, which the reader now guarantees (5bef2ca): an in-budget document is passed with its size, given the fuel countBounded allows, with no premise on the count returning. The prose in the header, the PROOF-STATUS row and the CHANGELOG now says exactly that, and that the bound counts calls. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- CHANGELOG.adoc | 10 +++-- verification/PROOF-STATUS.adoc | 12 ++++-- verification/proofs/idris2/KyamlBudget.idr | 44 ++++++++++++++++++---- 3 files changed, 51 insertions(+), 15 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 3bdaf110..1043611d 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -94,10 +94,12 @@ reader"): `test/egress_decision_mirror_test.exs` runs RE001 on all 240 cases of a small domain and requires it to agree with the proved decision. * `verification/proofs/idris2/KyamlBudget.idr` models `within_budget?/2` - and proves that it passes exactly the documents whose expanded size is - within the limit, in at most 2 · (limit + 1) + 2 steps however far the - aliases expand. `test/kyaml_test.exs` holds the Elixir count to the - model on 154 trees at every limit. + and proves that, on a document in which no alias names another alias + (which the reader guarantees), it passes exactly the documents whose + expanded size is within the limit, in at most 2 · (limit + 1) + 2 calls + of `count/3` however far the aliases expand. The bound counts calls, not + the work inside one or allocation. `test/kyaml_test.exs` holds the + Elixir count to the model on 154 trees at every limit. The reader as a whole is tested, not proved, and endpoints are not modelled; both are recorded as such. diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index 21f863f2..d739b190 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -351,10 +351,14 @@ endpoints agree with the hosts a job names and with its hardener's |`+verification/proofs/idris2/KyamlBudget.idr+` |Idris2 |A model of `within_budget?/2` step for step (`+count+`, `+stepCount+`). A total within the limit is the document's exact size with every alias read -through (`+countSound+`, `+withinBudgetSound+`); a document within the -limit is passed (`+countAtMost+`, `+withinBudgetComplete+`); with no -alias naming an alias, the count answers within 2 · (limit + 1) + 2 -steps however far the aliases expand (`+countBounded+`) |PROVEN +through (`+countSound+`, `+withinBudgetSound+`); if the count returns, a +document within the limit is passed (`+countAtMost+`, +`+withinBudgetComplete+`); with no alias naming an alias, the count +answers within 2 · (limit + 1) + 2 calls of `count/3` however far the +aliases expand (`+countBounded+`; the bound counts calls, not the work +inside one or allocation); composed, such a document within the limit is +passed with no premise on the count returning (`+withinBudgetPasses+`) +|PROVEN |Runtime mirror, lib/hypatia/kyaml.ex |Elixir |`within_budget?/2` passes exactly the trees whose expanded size is within the limit, on 154 trees diff --git a/verification/proofs/idris2/KyamlBudget.idr b/verification/proofs/idris2/KyamlBudget.idr index cebab381..574eef77 100644 --- a/verification/proofs/idris2/KyamlBudget.idr +++ b/verification/proofs/idris2/KyamlBudget.idr @@ -25,12 +25,20 @@ -- * `withinBudgetSound`: a total within the limit is the exact size of -- the document with every alias read through. `within_budget?` never -- passes a document that expands past the limit. --- * `withinBudgetComplete`: a document whose expanded size is within the --- limit is passed, with that size. +-- * `withinBudgetComplete`: when the count returns a total, a document +-- whose expanded size is within the limit is passed, with that size. +-- It assumes the count returned; it does not show that it does (with +-- too little fuel it returns `Nothing`). -- * `countBounded`: when no alias names another alias (the reader refuses -- an anchored alias, ALIAS_DECORATED), the count answers within --- 2 * (limit + 1) + 2 steps, however far the aliases expand. This is the --- bound on work that makes the anchor bomb cheap to refuse. +-- 2 * (limit + 1) + 2 calls of `count/3`, however far the aliases +-- expand. That bounds the calls, the work that grows with alias +-- expansion; it does not bound the work inside a call (copying a +-- collection's children onto the stack) or allocation. +-- * `withinBudgetPasses`: the two composed. On a document with no alias +-- chain, given the calls `countBounded` allows, a document whose +-- expanded size is within the limit is passed, with that size; nothing +-- is assumed about the count returning. -- -- This is a model of the algorithm, not a refinement proof of the Elixir -- function. The function is held to the model by test/kyaml_test.exs and @@ -147,8 +155,9 @@ withinBudgetSound : (f, limit : Nat) -> (doc : Node) -> withinBudgetSound f limit doc prf within = rewrite countSound f limit 0 [doc] prf within in plusZeroRightNeutral (size doc) -||| `within_budget?`: a document that expands to no more than the limit is -||| passed, and its total is its size. +||| `within_budget?`: if the count returns a total, a document that expands +||| to no more than the limit is passed, and its total is its size. The +||| count returning is a premise here; `withinBudgetPasses` discharges it. export withinBudgetComplete : (f, limit : Nat) -> (doc : Node) -> LTE (size doc) limit -> @@ -258,7 +267,9 @@ countFinishes m n limit room stack ok (S f) enough with (lte n limit) proof chec countFinishes m n limit room stack ok (S f) enough | False = ItIsJust ||| `within_budget?` on a document without alias chains answers within -||| 2 * (limit + 1) + 2 steps, however far its aliases expand. +||| 2 * (limit + 1) + 2 calls of `count/3` (units of fuel), +||| however far its aliases expand. The work inside a call is not +||| counted. export countBounded : (limit : Nat) -> (doc : Node) -> NoChain doc -> IsJust (count (S (S limit + S limit + 1)) limit [doc] 0) @@ -266,3 +277,22 @@ countBounded limit doc ok = countFinishes (S limit) 0 limit Refl [doc] [ok] (S (S limit + S limit + 1)) (LTESucc (plusLteMonotoneLeft (S limit + S limit) (aliasOnTop [doc]) 1 (aliasOnTopBit [doc]))) + +-- ─── Completeness without a premise on the count ─────────────────────── + +isJustValue : (m : Maybe a) -> IsJust m -> (k ** m = Just k) +isJustValue (Just k) ItIsJust = (k ** Refl) + +||| `within_budget?` on a document without alias chains, given the steps +||| `countBounded` allows: a document whose expanded size is within the +||| limit is passed, and its total is its size. Unlike +||| `withinBudgetComplete`, nothing is assumed about the count returning: +||| `countBounded` supplies that. +export +withinBudgetPasses : (limit : Nat) -> (doc : Node) -> NoChain doc -> + LTE (size doc) limit -> + count (S (S limit + S limit + 1)) limit [doc] 0 = Just (size doc) +withinBudgetPasses limit doc ok small with (isJustValue _ (countBounded limit doc ok)) + withinBudgetPasses limit doc ok small | (k ** prf) = + rewrite sym (snd (withinBudgetComplete (S (S limit + S limit + 1)) + limit doc small prf)) in prf From 19a60c6b6e961578f7dfdc1387e66078985dad80 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:38:38 +0000 Subject: [PATCH 08/14] Proof labels: PWG-3 in the Agda header and the ECHIDNA issue packet MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR moved the proof documents to PROOF-POLICY §8's terms, but two texts it points at still used the retired Mathesis ladder: the header of LogtalkMigration.agda ("Grade 3 target ... AGDA-PENDING") and the issue packet prepared for ECHIDNA ("Mathesis Grade 3 / AGDA-VERIFIED", "Grade 2/1"). §8 asks for the PWG- prefix, never a bare "Grade 3", and the recorded status is PROVEN, PWG-3. The Agda change is to the comment header only; no definition or theorem changes. The header no longer states a status of its own: it names the target and points at the receipt in PROOF-STATUS.adoc, so it cannot go stale again. The file's SHA-256 changes, so the next Verify Proofs run records a new receipt; the recorded one is for commit 4018290 and stays true for it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- .../rules/migration/echidna-security-learning-issue.md | 2 +- verification/proofs/agda/LogtalkMigration.agda | 10 +++++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/docs/rules/migration/echidna-security-learning-issue.md b/docs/rules/migration/echidna-security-learning-issue.md index 5454c7b1..437a1f4c 100644 --- a/docs/rules/migration/echidna-security-learning-issue.md +++ b/docs/rules/migration/echidna-security-learning-issue.md @@ -33,7 +33,7 @@ Deliberate divergences, all ledgered in Hypatia `docs/rules/logtalk-migration.ad - `BranchProtectionID` prevention is `scorecard-enforcer.yml` (long-standing Elixir value), not the Logtalk `branch-protection-enforcer.yml`; `CodeReviewID` gained a prevention mapping with no Logtalk counterpart. - Wholly unknown alert ids get severity `:info` in Elixir rather than the Logtalk catch-all `low`; all 18 known ids agree exactly. -Proof status, stated exactly: the finite table correspondence is modelled in Hypatia `verification/proofs/agda/LogtalkMigration.agda` and is **Mathesis Grade 3 / AGDA-VERIFIED** on a strict-profile receipt (Agda 2.8.0.2, `agda --safe --without-K --cubical-compatible`, Hypatia Verify Proofs run 41328302925 at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331; full receipt in Hypatia `verification/PROOF-STATUS.adoc`). Elixir behaviour is pinned by ExUnit tests in the same PR's CI. The Agda model grades the finite table correspondence only — no runtime-refinement or Grade 2/1 claim is being sold here. +Proof status, stated exactly: the finite table correspondence is modelled in Hypatia `verification/proofs/agda/LogtalkMigration.agda` and is **PROVEN, `PWG-3`** (metadatastician/standards `3-practice/PROOF-POLICY.adoc` §5 and §8) on a strict-profile receipt (Agda 2.8.0.2, `agda --safe --without-K --cubical-compatible`, Hypatia Verify Proofs run 41328302925 at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331; full receipt in Hypatia `verification/PROOF-STATUS.adoc`). Elixir behaviour is pinned by ExUnit tests in the same PR's CI. The Agda model grades the finite table correspondence only — no runtime-refinement, `PWG-2i`, `PWG-2ii` or `PWG-1` claim is being sold here. ## Requested changes in ECHIDNA diff --git a/verification/proofs/agda/LogtalkMigration.agda b/verification/proofs/agda/LogtalkMigration.agda index e06f803f..a0549419 100644 --- a/verification/proofs/agda/LogtalkMigration.agda +++ b/verification/proofs/agda/LogtalkMigration.agda @@ -25,9 +25,13 @@ -- docs/rules/logtalk-migration.adoc. Elixir runtime behaviour is -- pinned by ExUnit tests, not by this file. -- --- Intended Mathesis grade: Grade 3 target. It becomes Grade 3 only when --- the strict command in verification/PROOF-STATUS.adoc has a recorded --- successful receipt; until then its status is AGDA-PENDING. +-- Status and grade (standards PROOF-POLICY §5 and §8): the target is +-- `PROVEN`, `PWG-3`, which holds only while the strict command in +-- verification/PROOF-STATUS.adoc has a recorded successful receipt. The +-- current status and the receipt are recorded there, not here. The grade +-- covers this finite model only: there is no Rocq or Lean leg, so no +-- recheck correspondence state (§2.2) applies, and no runtime-refinement +-- claim is made. -- No postulates, no unsafe options, no standard-library dependency. module LogtalkMigration where From 0f0ae37ba3d001631daaaa97a3176992b6710429 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:47:00 +0000 Subject: [PATCH 09/14] RE001/RE002: close the review misses in the new endpoint comparison The endpoint comparison and the parsed-model RE002 are new in this PR, so each miss below is this PR's; every one has a test that fails on 5bef2ca. Endpoint comparison (RE001): * `[a-z0-9.-]*githubusercontent.com` took notgithubusercontent.com for GitHub, so a lookalike host escaped both comparisons. A subdomain now needs its dot. * `HTTPS://host` was not read as a URL; the scheme is now matched in any case, as clients do. * A literal IPv4 host (`https://10.0.0.5/upload`) was never compared. It is now, loopback aside. Single-label names (localhost, service containers) stay out: they are not egress, and flagging them would report most service-container workflows. * `https://h:${{ vars.PORT }}/x` was taken as port 443, a false finding when the deed declares the real port. A port written as an expression is now unknown. * The scp pattern refused `git@gitlab.com:123team/x.git` (digit-led path) yet took `owner@example.com: failed` for a remote to port 22. It now needs a path, which may start with a digit but is not a port. * A `#` inside shell quotes (`git commit -m "fix #12" && git push URL`) was taken to open a comment, hiding the URL after it. * `allowed-endpoints: smtp.example.com:${{ vars.PORT }}` was dropped whole, so an undeclared literal host passed. The host is kept, with its port unknown. * An allowed entry with no port lets out every port, but a deed listing only :443 was taken to cover it. It is now held to a declaration without a port (allowed -> declared only). RE002: * A job whose `if:` admits only pull_request was reported for the default audit policy (new with this PR's default detection). The job gate RE001 uses now narrows RE002's protected triggers too. * A workflow the KYAML reader refuses was skipped silently unless it named secrets, though the line reader found its `audit`. RE002 now reports such a workflow as unreadable (:warn) when it names harden-runner. Workflow: a step of an aliased job, or an aliased step, was reported at the anchor's line (the line reader reported the alias). Anything read through an alias now stays under it (child/2, entries/1, items/1). Coverage only: the egress mirror adds the dynamic-only job (280 cases, was 240; PROOF-STATUS and CHANGELOG updated), the equivalence harness compares a declared job's endpoint findings across the four layouts, and RE002 has a push workflow with hardener text only in a run block. On the six-repository differential RE001 and RE002 give the same 6 findings before and after. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- CHANGELOG.adoc | 19 +- lib/hypatia/workflow.ex | 68 ++--- lib/rules/research_extensions.ex | 178 +++++++++---- test/egress_decision_mirror_test.exs | 12 +- test/research_extensions_equivalence_test.exs | 50 +++- test/research_extensions_test.exs | 246 ++++++++++++++++++ verification/PROOF-STATUS.adoc | 4 +- 7 files changed, 494 insertions(+), 83 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 1043611d..7d5b41be 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -69,6 +69,23 @@ model instead of scanning lines (WH013 and WH014 follow, and any case, its own `with: egress-policy`. A step with no policy runs harden-runner's default, `audit`, and is now reported. The trigger is a `push` or `release` key of `on:`, not a `push:` anywhere in the file. +* **Review fixes on #1036**, each with a test that fails without it. The + endpoint comparison no longer takes `notgithubusercontent.com` for a + GitHub host; reads a URL's scheme in any case (`HTTPS://`); compares a + literal IPv4 host (loopback aside; a single-label name such as + `localhost` or a service container is still not egress); treats a URL + port written as an expression as unknown instead of the scheme's default; + reads `git@gitlab.com:123team/x.git` as a remote but + `owner@example.com: failed` as prose; ignores a `#` inside shell quotes + (`git commit -m "fix #12" && git push …`) when looking for comments; + keeps the literal host of an allowed entry whose port is an expression; + and holds an allowed entry with no port (every port) to a declaration + with none. RE002 skips a job whose `if:` admits only events other than + `push` and `release`, and reports a workflow the reader refuses if it + names harden-runner (the line reader used to find its `audit` there). + A job or step read through an alias is reported at the alias again, not + at the anchor. On the six repositories above, RE001 and RE002 give the + same 6 findings before and after. The `code_safety/elixir_atom_from_user` description was backwards: it named `String.to_existing_atom` as the danger. It now names `String.to_atom`. The @@ -91,7 +108,7 @@ reader"): claim, that a declaration lists exactly the secrets read, and that a key computed at run time is never declared. Three expected rejections and a positive control run in `scripts/check-verdicts.sh`. - `test/egress_decision_mirror_test.exs` runs RE001 on all 240 cases of a + `test/egress_decision_mirror_test.exs` runs RE001 on all 280 cases of a small domain and requires it to agree with the proved decision. * `verification/proofs/idris2/KyamlBudget.idr` models `within_budget?/2` and proves that, on a document in which no alias names another alias diff --git a/lib/hypatia/workflow.ex b/lib/hypatia/workflow.ex index 4f9535bd..4a968a32 100644 --- a/lib/hypatia/workflow.ex +++ b/lib/hypatia/workflow.ex @@ -100,38 +100,46 @@ defmodule Hypatia.Workflow do end end + # A job or step read through an alias (`b: *a`, `- *step`) keeps the alias + # around everything read from it (`child/2`, `entries/1`, `items/1`), so a + # rule reports what it finds there at the alias, not at the anchor. defp job(%{key: key, value: value}) do - node = Kyaml.deref(value) - %Job{ id: key.value, line: elem(key.loc, 0), node: value, - runs_on: Kyaml.get(node, "runs-on"), - uses: text(Kyaml.get(node, "uses")), - if: text(Kyaml.get(node, "if")), - env: Kyaml.get(node, "env"), - permissions: Kyaml.get(node, "permissions"), - steps: for(item <- items(Kyaml.get(node, "steps")), do: step(item)) + runs_on: child(value, "runs-on"), + uses: text(child(value, "uses")), + if: text(child(value, "if")), + env: child(value, "env"), + permissions: child(value, "permissions"), + steps: for(item <- items(child(value, "steps")), do: step(item)) } end defp step(item) do - node = Kyaml.deref(item) - run = Kyaml.get(node, "run") + run = child(item, "run") %Step{ line: elem(item.loc, 0), - node: node, - uses: text(Kyaml.get(node, "uses")), + node: item, + uses: text(child(item, "uses")), run: text(run), run_style: run && Kyaml.deref(run)[:style], - with: Kyaml.get(node, "with"), - env: Kyaml.get(node, "env"), - if: text(Kyaml.get(node, "if")) + with: child(item, "with"), + env: child(item, "env"), + if: text(child(item, "if")) } end + # `Kyaml.get/2`, with the value kept under the alias it was read through. + defp child(%{kind: :alias} = alias, key), do: under(alias, child(alias.target, key)) + defp child(node, key), do: Kyaml.get(node, key) + + # `node`, read through `alias`: reported at the alias, as `strings/1` reports it. + defp under(_alias, nil), do: nil + defp under(alias, node), do: %{alias | target: node} + @doc """ The events of the workflow's `on:`: `on: push`, a list, or the keys of a mapping (`on: {push: {paths: […]}}` names one event). @@ -148,21 +156,23 @@ defmodule Hypatia.Workflow do @doc "A step input's value (`with: {egress-policy: block}`), or nil." def input(%Step{with: with}, name), do: with |> Kyaml.get(name) |> text() - @doc "The entries of a mapping node (through an alias); [] for anything else." - def entries(node) do - case node && Kyaml.deref(node) do - %{kind: :map, entries: entries} -> entries - _ -> [] - end - end + @doc """ + The entries of a mapping node; [] for anything else. Through an alias, + each value stays under the alias, so it is reported at the alias. + """ + def entries(%{kind: :alias} = alias), + do: for(entry <- entries(alias.target), do: %{entry | value: under(alias, entry.value)}) - @doc "The items of a sequence node (through an alias); [] for anything else." - def items(node) do - case node && Kyaml.deref(node) do - %{kind: :seq, items: items} -> items - _ -> [] - end - end + def entries(%{kind: :map, entries: entries}), do: entries + def entries(_), do: [] + + @doc """ + The items of a sequence node; [] for anything else. Through an alias, + each item stays under the alias, so it is reported at the alias. + """ + def items(%{kind: :alias} = alias), do: for(item <- items(alias.target), do: under(alias, item)) + def items(%{kind: :seq, items: items}), do: items + def items(_), do: [] @doc """ A scalar's text, whatever it resolved to (`egress-policy: block`, `ref: 1`): diff --git a/lib/rules/research_extensions.ex b/lib/rules/research_extensions.ex index a882d75e..48915770 100644 --- a/lib/rules/research_extensions.ex +++ b/lib/rules/research_extensions.ex @@ -241,13 +241,16 @@ defmodule Hypatia.Rules.ResearchExtensions do An unreadable deed or clause declares nothing, and the finding says why. `:endpoints` are compared with what the workflow shows, as `:warn` findings: - * a host outside GitHub that a step names literally (a URL, or a - `git@host:` remote; not in a `#` comment) must be covered by a declared - endpoint, where `*.x` covers the subdomains of x and an endpoint without a - port covers every port; + * a host outside GitHub that a step names literally (a domain name or an + IPv4 address other than loopback, in a URL or a `git@host:path` + remote; not in a `#` comment outside quotes) must be covered by a + declared endpoint, where `*.x` covers the subdomains of x and an + endpoint without a port covers every port; a port written as an + expression is unknown, and any port of the host covers it; * when the job's harden-runner step lists `allowed-endpoints`, every host - outside GitHub on it must be declared, and every declared literal host - must be on it. + outside GitHub on it must be declared (an entry without a port lets out + every port, so only a declaration without one covers it), and every + declared literal host must be on it. What an action or a variable reaches at run time is not modelled: that needs run-time observation. @@ -294,7 +297,11 @@ defmodule Hypatia.Rules.ResearchExtensions do # A workflow that names secrets but cannot be read is reported. Its # declarations cannot be checked, so they are not reported stale. - unreadable = for {:unreadable, rel, error, true} <- workflows, do: {rel, error} + unreadable = + for {:unreadable, rel, error, bytes} <- workflows, + Regex.match?(~r/secrets/i, bytes), + do: {rel, error} + unread = MapSet.new(for {:unreadable, rel, _, _} <- workflows, do: rel) job_findings = @@ -358,7 +365,7 @@ defmodule Hypatia.Rules.ResearchExtensions do # The workflows of a repo as RE001 reads them: the parsed model # (Hypatia.Workflow, over kyq's KYAML reader). A workflow the reader refuses - # is {:unreadable, …}, with whether it names secrets at all. + # is {:unreadable, rel, error, bytes}. defp re001_workflows(repo_path) do for path <- workflow_files(repo_path) do rel = Path.relative_to(path, repo_path) @@ -366,7 +373,7 @@ defmodule Hypatia.Rules.ResearchExtensions do case Workflow.parse(bytes, rel) do {:ok, workflow} -> {:ok, rel, workflow} - {:error, error} -> {:unreadable, rel, error, Regex.match?(~r/secrets/i, bytes)} + {:error, error} -> {:unreadable, rel, error, bytes} end end end @@ -730,11 +737,21 @@ defmodule Hypatia.Rules.ResearchExtensions do # An endpoint held in a secret or variable (`secret:`, `var:`) covers no # literal host: a host written in the workflow is declared as itself. - # GitHub's own endpoints, which :endpoints leaves out (ADR-009). - @github_hosts ~r/\A(?:github\.com|[a-z0-9.-]+\.github\.com|[a-z0-9.-]*githubusercontent\.com|ghcr\.io|[a-z0-9.-]+\.githubassets\.com|github\.io|[a-z0-9.-]+\.github\.io)\z/ - - @url_host ~r<\b(https?|wss?|ssh|git|ftps?)://(?:[^@/\s"'`]+@)?([A-Za-z0-9](?:[A-Za-z0-9.-]*[A-Za-z0-9])?\.[A-Za-z]{2,})(?::(\d{1,5}))?> - @scp_host ~r/(?i + # A `user@host:path` remote. The path is not blank (`a@example.com: failed` + # is prose) and not a port (`user:pass@host:5432/db` is a URL's userinfo), + # though it may start with a digit (`git@gitlab.com:123team/x.git`). + @scp_host ~r/(? 80, "ws" => 80, @@ -753,11 +770,15 @@ defmodule Hypatia.Rules.ResearchExtensions do not in_shell_comment?(text, at), host = String.downcase(host), not Regex.match?(@github_hosts, host), + not loopback?(host), do: {host, port, line_of.(at)} end + defp loopback?(host), do: Regex.match?(~r/\A(?:127\.|0\.0\.0\.0\z)/, host) + # Is offset `at` inside a `#` comment: after a `#` that starts the line or - # follows a blank? (A URL fragment, `/#x`, is not one.) + # follows a blank, outside quotes? (A URL fragment, `/#x`, is not one, nor + # is the `#` of `git commit -m "fix #12"`.) defp in_shell_comment?(text, at) do line_start = case :binary.matches(binary_part(text, 0, at), "\n") do @@ -765,33 +786,56 @@ defmodule Hypatia.Rules.ResearchExtensions do matches -> matches |> List.last() |> elem(0) |> Kernel.+(1) end - Regex.match?(~r/(?:\A|\s)#/, binary_part(text, line_start, at - line_start)) + comment_opens?(binary_part(text, line_start, at - line_start), nil, true) end + # Walks one line: `quote` is the open quote character or nil, `word_start?` + # whether the next character starts a word. A backslash escapes the next + # character outside single quotes, as the shell reads it. + defp comment_opens?(<<>>, _quote, _word_start?), do: false + defp comment_opens?(<>, nil, true), do: true + + defp comment_opens?(<>, nil, _) when c in [?', ?"], + do: comment_opens?(rest, c, false) + + defp comment_opens?(<>, quote, _) when quote != ?', + do: comment_opens?(rest, quote, false) + + defp comment_opens?(<>, c, _), do: comment_opens?(rest, nil, false) + + defp comment_opens?(<>, quote, _), + do: comment_opens?(rest, quote, quote == nil and c in [?\s, ?\t]) + + # A port written as an expression is unknown (nil), not the scheme's default. defp url_hosts(text) do - for [{at, _}, {s, sl}, {h, hl}, port] <- - Regex.scan(@url_host, text, return: :index, capture: :all) |> Enum.map(&pad_port/1) do + for [{at, _}, {s, sl}, {h, hl} | port] <- Regex.scan(@url_host, text, return: :index) do scheme = String.downcase(binary_part(text, s, sl)) - port = if port, do: String.to_integer(binary_part(text, elem(port, 0), elem(port, 1))) - {binary_part(text, h, hl), port || @default_port[scheme], at} + + port = + case port do + [{p, pl} | _] when p >= 0 -> String.to_integer(binary_part(text, p, pl)) + [_, {e, _}] when e >= 0 -> nil + _ -> @default_port[scheme] + end + + {binary_part(text, h, hl), port, at} end end - defp pad_port([all, scheme, host]), do: [all, scheme, host, nil] - defp pad_port([all, scheme, host, {_, 0}]), do: [all, scheme, host, nil] - defp pad_port(match), do: match - defp scp_hosts(text) do for [{at, _}, {h, hl}] <- Regex.scan(@scp_host, text, return: :index), do: {binary_part(text, h, hl), 22, at} end # The literal entries of a harden-runner step's `allowed-endpoints` input - # (`host:port`, separated by spaces, newlines or commas); nil when the step - # sets none. An entry written with an expression + # (`host:port`, separated by spaces, newlines or commas) as {host, port}; + # nil when the step sets none. An entry written without a port lets out + # every port (`:any`). An entry whose host is an expression # (`${{ secrets.SMTP_HOST }}:${{ secrets.SMTP_PORT }}`) names its host only # at run time, as a declared `secret:` or `var:` endpoint does, so it is - # not a literal entry. An expression is one unit however it is spaced. + # not a literal entry; a literal host with an expression for its port + # (`smtp.example.com:${{ vars.PORT }}`) is, with its port unknown (nil). + # An expression is one unit however it is spaced. defp harden_runner_allowed(step) do case Workflow.input(step, "allowed-endpoints") do nil -> @@ -801,10 +845,18 @@ defmodule Hypatia.Rules.ResearchExtensions do text |> String.replace(@expression, "\0") |> String.split(~r/[\s,]+/, trim: true) - |> Enum.reject(&String.contains?(&1, "\0")) + |> Enum.flat_map(fn entry -> + case String.split(entry, ":\0") do + [host, ""] -> host |> literal_endpoint() |> List.wrap() + _ -> entry |> literal_endpoint() |> List.wrap() |> Enum.map(&any_port/1) + end + end) end end + defp any_port({host, nil}), do: {host, :any} + defp any_port(endpoint), do: endpoint + # A literal endpoint as {host pattern, port or nil}: `host` or # `host:digits`. Anything else (secret:, var:, an expression) is nil. defp literal_endpoint(endpoint) do @@ -815,9 +867,11 @@ defmodule Hypatia.Rules.ResearchExtensions do end end - # Does a declared {pattern, port} cover a host and port? `*.x` covers the + # Does a {pattern, port} cover a host and port? `*.x` covers the # subdomains of x (as harden-runner reads it), not x itself; an endpoint - # without a port covers every port. + # without a port (nil or `:any`) covers every port. A port known only at + # run time (nil) is covered by any port of the host; every port (`:any`) + # only by an endpoint without a port. defp covers?({pattern, want}, host, port) do host_ok = case pattern do @@ -825,7 +879,7 @@ defmodule Hypatia.Rules.ResearchExtensions do _ -> pattern == host end - host_ok and (want == nil or port == nil or want == port) + host_ok and (want in [nil, :any] or port == nil or want == port) end defp re001_endpoint_findings(job, deed_file, decl) do @@ -847,12 +901,7 @@ defmodule Hypatia.Rules.ResearchExtensions do defp allowed_endpoint_findings(%{allowed_endpoints: nil}, _deed_file, _declared), do: [] defp allowed_endpoint_findings(job, deed_file, declared) do - allowed = - job.allowed_endpoints - |> Enum.map(&literal_endpoint/1) - |> Enum.reject(fn endpoint -> - endpoint == nil or Regex.match?(@github_hosts, elem(endpoint, 0)) - end) + allowed = Enum.reject(job.allowed_endpoints, &Regex.match?(@github_hosts, elem(&1, 0))) # What the hardener lets out must be declared. A declared literal host # must be let out, or block mode stops the job; a declared wildcard is a @@ -874,7 +923,7 @@ defmodule Hypatia.Rules.ResearchExtensions do end end - defp endpoint_text({host, nil}), do: "\"#{host}\"" + defp endpoint_text({host, port}) when port in [nil, :any], do: "\"#{host}\"" defp endpoint_text({host, port}), do: "\"#{host}:#{port}\"" defp re001_unnamed_endpoints(job, deed_file, uncovered) do @@ -966,13 +1015,29 @@ defmodule Hypatia.Rules.ResearchExtensions do case, as RE001 accepts it), its policy is that step's own `with: egress-policy`, and a step with no policy runs harden-runner's default, `audit`. The trigger is a `push` or `release` event in the - workflow's `on:`. A workflow that cannot be read is RE001's to report. + workflow's `on:`, narrowed by a job `if:` that admits only listed events + (as RE001 narrows untrusted events): a job that runs only on + `pull_request` is not on a protected-branch trigger. - Severity: `:high`. Action: `:report`. + A workflow that cannot be read and names `harden-runner` is reported as + unreadable (`:warn`): its hardener cannot be checked, and a silent skip + would read as a pass. + + Severity: `:high` (`:warn` for an unreadable workflow). Action: `:report`. """ def re002_harden_runner_audit_mode(repo_path) do - for {:ok, rel, %Workflow{} = workflow} <- re001_workflows(repo_path), - Enum.any?(workflow.triggers, &(&1 in ["push", "release"])), + workflows = re001_workflows(repo_path) + + unreadable = + for {:unreadable, rel, error, bytes} <- workflows, + Regex.match?(~r/harden-runner/i, bytes), + do: re002_unreadable(rel, error) + + unreadable ++ re002_audit_findings(workflows) + end + + defp re002_audit_findings(workflows) do + for {:ok, rel, %Workflow{} = workflow} <- workflows, audit = audit_hardeners(workflow), audit != [] do defaulted? = Enum.all?(audit, &(&1 == :default)) @@ -995,10 +1060,33 @@ defmodule Hypatia.Rules.ResearchExtensions do end end - # The audit-mode harden-runner steps of a workflow's jobs: `:explicit` for - # `egress-policy: audit`, `:default` for a step that sets no policy. - defp audit_hardeners(%Workflow{jobs: jobs}) do + defp re002_unreadable(rel, error) do + %{ + rule: "RE002", + file: rel, + severity: :warn, + line: error.line, + reason: + "#{rel} could not be read as KYAML (#{error.code} at line #{error.line}, column " <> + "#{error.column}: #{error.message}), so RE002 cannot check its harden-runner policy", + action: :report, + detail: %{ + fix: + "Rewrite the construct the reader names in the KYAML subset (kyq " <> + "docs/KYAML_SPEC.adoc; standards YAML-POLICY)." + } + } + end + + # The audit-mode harden-runner steps of the jobs that run on a protected + # trigger (`push` or `release`): `:explicit` for `egress-policy: audit`, + # `:default` for a step that sets no policy. + defp audit_hardeners(%Workflow{jobs: jobs, triggers: triggers}) do + protected = Enum.filter(triggers, &(&1 in ["push", "release"])) + for job <- jobs, + gate <- [job_event_gate(job)], + Enum.any?(protected, &(gate == nil or &1 in gate)), step <- job.steps, harden_runner_step?(step), harden_runner_policy(step) == "audit" do diff --git a/test/egress_decision_mirror_test.exs b/test/egress_decision_mirror_test.exs index a8328687..ed1bc087 100644 --- a/test/egress_decision_mirror_test.exs +++ b/test/egress_decision_mirror_test.exs @@ -11,8 +11,8 @@ defmodule Hypatia.EgressDecisionMirrorTest do workflow and deed, RE001 is run on it, and RE001 must report nothing exactly when `clean?/2` says the job is clean: - * the job reads one or two secrets, by name, and possibly also by a key - computed at run time; + * the job reads one or two secrets by name, a key computed at run + time, or both; * it has no hardener, or harden-runner with `egress-policy` unset, `audit` or `block`; * it is undeclared, or declared with any non-empty subset of the two @@ -53,8 +53,9 @@ defmodule Hypatia.EgressDecisionMirrorTest do defp jobs do for secrets <- subsets(@secrets), - secrets != [], dynamic <- [false, true], + # A job that reads only a computed key is in scope too. + secrets != [] or dynamic, hardener <- [nil, :default, :audit, :block], do: %{secrets: secrets, dynamic: dynamic, hardener: hardener} end @@ -144,8 +145,9 @@ defmodule Hypatia.EgressDecisionMirrorTest do test "RE001 reports a job exactly when Egress.idr's decClean refuses it" do cases = for job <- jobs(), decl <- decls(), do: {job, decl} - # 3 secret sets x 2 x 4 hardeners, each with no declaration or 3 x 3. - assert length(cases) == 24 * 10 + # (3 secret sets x 2, plus the dynamic-only job) x 4 hardeners, each + # with no declaration or 3 x 3. + assert length(cases) == 28 * 10 mismatches = cases diff --git a/test/research_extensions_equivalence_test.exs b/test/research_extensions_equivalence_test.exs index 33ce9ef3..db91a9b1 100644 --- a/test/research_extensions_equivalence_test.exs +++ b/test/research_extensions_equivalence_test.exs @@ -65,13 +65,61 @@ defmodule Hypatia.Rules.ResearchExtensionsEquivalenceTest do assert {"RE002", :high} in rules end + # The random workflows carry no deed, so the endpoint comparison is held + # to the same rule here on one declared job: a host a step names, and a + # hardener's allow-list that disagrees with the declaration. + test "declared endpoints compare the same however the workflow is written" do + hardener = + {:map, + [ + {"uses", "step-security/harden-runner@#{@sha}"}, + {"with", + {:map, + [{"egress-policy", "block"}, {"allowed-endpoints", "hex.pm:443 repo.hex.pm:443"}]}} + ]} + + upload = + {:map, + [ + {"run", "curl https://upload.example.com/v1"}, + {"env", {:map, [{"K", "${{ secrets.API_KEY }}"}]}} + ]} + + job = {:map, [{"runs-on", "ubuntu-latest"}, {"steps", {:seq, [hardener, upload]}}]} + workflow = {:map, [{"on", {:seq, ["push"]}}, {"jobs", {:map, [{"ship", job}]}}]} + + deed = + ~s|(egress (job :workflow ".github/workflows/w.yml" :job "ship" | <> + ~s|:secrets ("API_KEY") :endpoints ("hex.pm:443") :enforcement harden-runner-block))| + + [{_, expected} | rest] = + for style <- [:block, :flow, :quoted, :literal], + do: {style, findings(render(workflow, style), deed)} + + reasons = Enum.map(expected, & &1.reason) + # strip_lines/1 drops every `:digits`, ports included. + assert Enum.any?(reasons, &(&1 =~ ~s|names "upload.example.com" literally|)) + assert Enum.any?(reasons, &(&1 =~ ~s|lets out undeclared "repo.hex.pm"|)) + + for {style, got} <- rest, do: assert(got == expected, "#{style} differs from block") + end + # ─── findings, line-free ──────────────────────────────────────────── - defp findings(yaml) do + defp findings(yaml, deed \\ nil) do dir = Path.join(System.tmp_dir!(), "hyp-equiv-#{System.unique_integer([:positive])}") File.mkdir_p!(Path.join(dir, ".github/workflows")) File.write!(Path.join(dir, ".github/workflows/w.yml"), yaml) + if deed do + File.write!(Path.join(dir, "x_chora.deed"), """ + ;; SPDX-License-Identifier: CC-BY-SA-4.0 + (repo-deed :schema-version "1.0.0" :canonical-name "x" + :repo-uuid #u5"github.com/o/x" :beholding-chora #u5"estate/chora" + #{deed}) + """) + end + try do (ResearchExtensions.re001_missing_harden_runner(dir) ++ ResearchExtensions.re002_harden_runner_audit_mode(dir)) diff --git a/test/research_extensions_test.exs b/test/research_extensions_test.exs index 3637fb19..3de0c4dd 100644 --- a/test/research_extensions_test.exs +++ b/test/research_extensions_test.exs @@ -2033,6 +2033,174 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do assert [finding] = endpoint_findings(steps.("hex.pm:443"), ~s|"hex.pm" "cdn.example.com"|) assert finding.reason =~ ~s|does not allow declared "cdn.example.com"| end + + # A literal host with an expression for its port is still a literal host; + # an entry with no port lets out every port, which a deed listing one + # port does not declare. + test "allowed-endpoints: a run-time port keeps its host; no port means every port" do + steps = fn allowed -> + """ + - uses: step-security/harden-runner@v2 + with: + egress-policy: block + allowed-endpoints: > + #{allowed} + - run: deploy --token ${{ secrets.TOKEN }} + """ + end + + dynamic = steps.("smtp.example.com:${{ vars.SMTP_PORT }}") + assert [finding] = endpoint_findings(dynamic, "") + assert finding.reason =~ ~s|lets out undeclared "smtp.example.com"| + assert endpoint_findings(dynamic, ~s|"smtp.example.com:465"|) == [] + + portless = steps.("api.example.com") + assert [finding] = endpoint_findings(portless, ~s|"api.example.com:443"|) + assert finding.reason =~ ~s|lets out undeclared "api.example.com"| + assert endpoint_findings(portless, ~s|"api.example.com"|) == [] + end + + test "GitHub's own hosts are whole domains, not suffixes" do + steps = """ + - run: curl https://notgithubusercontent.com/x https://raw.githubusercontent.com/y + env: + K: ${{ secrets.TOKEN }} + """ + + assert [finding] = endpoint_findings(steps, "") + assert finding.reason =~ ~s|names "notgithubusercontent.com:443" literally| + refute finding.reason =~ "raw.githubusercontent.com" + + allowed = """ + - uses: step-security/harden-runner@v2 + with: + egress-policy: block + allowed-endpoints: notgithubusercontent.com:443 githubusercontent.com:443 + - run: deploy --token ${{ secrets.TOKEN }} + """ + + assert [finding] = endpoint_findings(allowed, "") + assert finding.reason =~ ~s|lets out undeclared "notgithubusercontent.com:443"| + refute finding.reason =~ ~s|"githubusercontent.com:443"| + end + + test "a URL is read with its scheme in any case, and a literal IPv4 host is a host" do + steps = """ + - run: | + curl HTTPS://upload.example.com/x https://10.0.0.5/upload + curl http://127.0.0.1:8080/health http://localhost:9000 http://postgres:5432 + env: + K: ${{ secrets.TOKEN }} + """ + + assert [finding] = endpoint_findings(steps, "") + assert finding.reason =~ ~s|"upload.example.com:443"| + assert finding.reason =~ ~s|"10.0.0.5:443"| + # Loopback and single-label names (service containers) are not egress. + refute finding.reason =~ "127.0.0.1" + refute finding.reason =~ "localhost" + refute finding.reason =~ "postgres" + assert endpoint_findings(steps, ~s|"upload.example.com:443" "10.0.0.5:443"|) == [] + end + + test "a URL port written as an expression is unknown, not the scheme's default" do + steps = """ + - run: curl https://api.example.com:${{ vars.PORT }}/upload + env: + K: ${{ secrets.TOKEN }} + """ + + assert endpoint_findings(steps, ~s|"api.example.com:8443"|) == [] + assert [finding] = endpoint_findings(steps, "") + assert finding.reason =~ ~s|names "api.example.com" literally| + end + + test "an scp remote has a path, which may start with a digit" do + remote = fn line -> + """ + - run: | + #{line} + env: + K: ${{ secrets.TOKEN }} + """ + end + + assert [finding] = endpoint_findings(remote.("git push git@gitlab.com:123team/x.git"), "") + assert finding.reason =~ ~s|"gitlab.com:22"| + + # Prose with an address and a colon is no remote. + assert endpoint_findings(remote.(~s|echo "owner@example.com: deployment failed"|), "") == + [] + + # A URL's userinfo before a port is the URL's, not an scp remote. + assert endpoint_findings( + remote.("psql postgres://u:pass@db.example.com:5432/x"), + ~s|"db.example.com:5432"| + ) == [] + end + + test "a quoted # opens no shell comment" do + steps = """ + - run: | + git commit -m "fix #12" && git push https://gitlab.example.com/o/x.git + echo 'a # b' https://up.example.com # https://c.example.org + env: + K: ${{ secrets.TOKEN }} + """ + + assert [finding] = endpoint_findings(steps, "") + assert finding.reason =~ ~s|"gitlab.example.com:443"| + assert finding.reason =~ ~s|"up.example.com:443"| + refute finding.reason =~ "c.example.org" + end + end + + # What is read through an alias is reported at the alias (the old line + # reader did so); the parsed model reported the anchor. + describe "re001_missing_harden_runner/1 through an alias" do + test "a job or a step read through an alias is reported at the alias" do + job_alias = """ + on: push + jobs: + a: &j + runs-on: ubuntu-latest + steps: + - run: npm ci + env: + K: ${{ secrets.TOKEN }} + b: *j + """ + + step_alias = """ + on: push + jobs: + a: + runs-on: ubuntu-latest + steps: + - &s + run: npm ci + env: + K: ${{ secrets.TOKEN }} + b: + runs-on: ubuntu-latest + steps: + - *s + """ + + for {yaml, lines} <- [ + {job_alias, %{"a" => 8, "b" => 9}}, + {step_alias, %{"a" => 9, "b" => 13}} + ] do + repo = create_repo_with_workflow(yaml) + findings = ResearchExtensions.re001_missing_harden_runner(repo) + File.rm_rf!(repo) + + job_of = fn f -> hd(Regex.run(~r/job `(\w+)`/, f.reason, capture: :all_but_first)) end + assert Map.new(findings, &{job_of.(&1), &1.line}) == lines + + assert Enum.all?(findings, &(&1.severity == :high)) + end + end end # ─── RE002 ────────────────────────────────────────────────────────── @@ -2216,6 +2384,84 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do assert ResearchExtensions.re002_harden_runner_audit_mode(repo) == [] File.rm_rf!(repo) end + + # The fixture above is also held back by its pull_request trigger; on push + # only the step test stands between the text and a finding. + test "hardener text in a run block on push is not a hardener" do + repo = + create_repo_with_workflow(""" + on: [push] + jobs: + build: + runs-on: ubuntu-latest + steps: + - run: | + echo "uses: step-security/harden-runner@x" + echo "egress-policy: audit" + """) + + assert ResearchExtensions.re002_harden_runner_audit_mode(repo) == [] + File.rm_rf!(repo) + end + + # A job whose `if:` admits only pull_request never runs on push: its + # hardener, defaulted or explicit, is not on a protected trigger. + test "a job gated away from push and release is not on a protected trigger" do + run = fn gate, policy -> + repo = + create_repo_with_workflow(""" + on: + push: + pull_request: + jobs: + x: + if: github.event_name == '#{gate}' + runs-on: ubuntu-latest + steps: + - uses: step-security/harden-runner@1234567890abcdef1234567890abcdef12345678 + #{policy} + """) + + findings = ResearchExtensions.re002_harden_runner_audit_mode(repo) + File.rm_rf!(repo) + findings + end + + explicit = " with: {egress-policy: audit}" + + assert run.("pull_request", "") == [] + assert run.("pull_request", explicit) == [] + assert [%{severity: :high}] = run.("push", "") + assert [%{severity: :high}] = run.("push", explicit) + end + + # The line reader found `egress-policy: audit` in any file; a workflow + # the KYAML reader refuses must not now pass silently. + test "an unreadable workflow that names harden-runner is reported" do + repo = + create_repo_with_workflow(""" + on: push + base: &b {k: 1} + m: + <<: *b + jobs: + x: + runs-on: ubuntu-latest + steps: + - uses: step-security/harden-runner@1234567890abcdef1234567890abcdef12345678 + with: + egress-policy: audit + """) + + assert [finding] = ResearchExtensions.re002_harden_runner_audit_mode(repo) + assert finding.severity == :warn + assert finding.line == 4 + assert finding.reason =~ "UNSUPPORTED_MERGE_KEY" + assert finding.reason =~ "RE002 cannot check" + # It names no secret, so RE001 has nothing to report. + assert ResearchExtensions.re001_missing_harden_runner(repo) == [] + File.rm_rf!(repo) + end end # ─── RE003 ────────────────────────────────────────────────────────── diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index d739b190..7e78b2b7 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -337,8 +337,8 @@ says so by evaluation (`+decides+`), and refuses the same declaration for an auditing job (`+refusesAudit+`) |TESTED |Runtime mirror, lib/rules/research_extensions.ex |Elixir |RE001 reports -a job exactly when `decClean` refuses it, on all 240 cases of a small -domain (one or two secrets, a run-time key or none, four hardener +a job exactly when `decClean` refuses it, on all 280 cases of a small +domain (one or two secrets by name, a run-time key, or both; four hardener settings, no declaration or nine): test/egress_decision_mirror_test.exs, with the deed parse asserted per case and three mutants killed (two in the transcription, one in RE001's block check) |TESTED From 34acb64b8498c2d667c493c59e33a222d01d6aac Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:50:32 +0000 Subject: [PATCH 10/14] RE001/RE002: read egress-policy trimmed, as the action does harden-runner reads its inputs through core.getInput, which trims surrounding white space. A literal block (`egress-policy: |` then `block`) is therefore the policy `block`, but the model's value was "block\n": RE001 rejected a truthful harden-runner-block declaration and RE002 missed a literal-block `audit` on push. Two tests; both fail on 0f0ae37. (CodeRabbit on #1036; main read the header `|` instead.) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- CHANGELOG.adoc | 3 ++- lib/rules/research_extensions.ex | 11 +++++++++-- test/research_extensions_test.exs | 32 +++++++++++++++++++++++++++++++ 3 files changed, 43 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 7d5b41be..52a4b76d 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -56,7 +56,8 @@ model instead of scanning lines (WH013 and WH014 follow, and each with a test that fails on the line reader: `<<: [*defaults]` is refused and reported, not misplaced; text in a `name: |` block beside the hardener is not its input, so an audit hardener no longer passes for a - block one; a folded `egress-policy: >-` is read as its value. + block one; a folded `egress-policy: >-` is read as its value, and a + literal block is trimmed as the action's `core.getInput` trims it. * **Declared endpoints are checked** against the workflow (`:warn`): a host outside GitHub that a step names literally (a URL or a `git@host:` remote, shell comments aside) must be covered by the job's `:endpoints`, and diff --git a/lib/rules/research_extensions.ex b/lib/rules/research_extensions.ex index 48915770..075aa5fe 100644 --- a/lib/rules/research_extensions.ex +++ b/lib/rules/research_extensions.ex @@ -581,8 +581,15 @@ defmodule Hypatia.Rules.ResearchExtensions do end # The egress-policy input of a harden-runner step; harden-runner defaults to - # audit when none is set. - defp harden_runner_policy(step), do: Workflow.input(step, "egress-policy") || "audit" + # audit when none is set. Actions read inputs through core.getInput, which + # trims surrounding white space, so a literal block (`egress-policy: |` + # then `block`) is the policy `block`, not "block\n". + defp harden_runner_policy(step) do + case Workflow.input(step, "egress-policy") do + nil -> "audit" + policy -> String.trim(policy) + end + end # What the job runs next to its credential, for a finding's reason. defp exposure_note(%{exposures: []}), do: "" diff --git a/test/research_extensions_test.exs b/test/research_extensions_test.exs index 3de0c4dd..d715ab2c 100644 --- a/test/research_extensions_test.exs +++ b/test/research_extensions_test.exs @@ -2284,9 +2284,41 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do assert ResearchExtensions.re001_missing_harden_runner(repo) == [] File.rm_rf!(repo) end + + test "a literal-block egress-policy is read as the action reads it, trimmed" do + repo = + hardened_repo([ + "with:", + " egress-policy: |", + " block", + " allowed-endpoints: mail.example.com:443" + ]) + + assert ResearchExtensions.re001_missing_harden_runner(repo) == [] + File.rm_rf!(repo) + end end describe "re002_harden_runner_audit_mode/1" do + test "a literal-block audit policy on push is still audit" do + repo = + create_repo_with_workflow(""" + on: [push] + jobs: + x: + runs-on: ubuntu-latest + steps: + - uses: step-security/harden-runner@1234567890abcdef1234567890abcdef12345678 + with: + egress-policy: | + audit + - run: build + """) + + assert [%{severity: :high}] = ResearchExtensions.re002_harden_runner_audit_mode(repo) + File.rm_rf!(repo) + end + test "flags harden-runner in audit mode on push trigger" do repo = create_repo_with_workflow(""" From eef60a65715d67ecffca18c7b83a7ffb38e9a3be Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:54:11 +0000 Subject: [PATCH 11/14] RE001: hosts in the job's or the workflow's env are named too A literal endpoint in job- or workflow-level env (UPLOAD_URL: https://upload.example.com, used as $UPLOAD_URL) reaches every step, but the endpoint scan walked only the step nodes, so a declaration with empty :endpoints passed. Both env nodes are now scanned. Test fails on 0f0ae37; RE001/RE002 output over the six snapshot repositories is unchanged. (Codex on #1036.) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- lib/rules/research_extensions.ex | 9 ++++++--- test/research_extensions_test.exs | 31 +++++++++++++++++++++++++++++++ 2 files changed, 37 insertions(+), 3 deletions(-) diff --git a/lib/rules/research_extensions.ex b/lib/rules/research_extensions.ex index 075aa5fe..2aeb5523 100644 --- a/lib/rules/research_extensions.ex +++ b/lib/rules/research_extensions.ex @@ -461,7 +461,10 @@ defmodule Hypatia.Rules.ResearchExtensions do hardened?: harden_step != nil, harden_policy: harden_step && harden_runner_policy(harden_step), allowed_endpoints: harden_step && harden_runner_allowed(harden_step), - named_hosts: Enum.flat_map(steps, &named_hosts/1), + # A literal endpoint in the job's or the workflow's `env:` reaches every + # step (`$UPLOAD_URL`), so it is named as surely as one in a step. + named_hosts: + Enum.flat_map([workflow.env, job.env | Enum.map(steps, & &1.node)], &named_hosts/1), exposures: re001_exposures(steps, job_untrusted_events), shared?: shared_line != nil } @@ -771,8 +774,8 @@ defmodule Hypatia.Rules.ResearchExtensions do } # The hosts outside GitHub one step names literally, as {host, port, line}. - defp named_hosts(step) do - for {text, line_of} <- Workflow.strings(step.node), + defp named_hosts(node) do + for {text, line_of} <- Workflow.strings(node), {host, port, at} <- url_hosts(text) ++ scp_hosts(text), not in_shell_comment?(text, at), host = String.downcase(host), diff --git a/test/research_extensions_test.exs b/test/research_extensions_test.exs index d715ab2c..8d707fbe 100644 --- a/test/research_extensions_test.exs +++ b/test/research_extensions_test.exs @@ -2153,6 +2153,37 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do assert finding.reason =~ ~s|"up.example.com:443"| refute finding.reason =~ "c.example.org" end + + test "a host in the job's or the workflow's env is named by every step" do + repo = + create_repo_with_workflow( + """ + on: push + env: + MIRROR: git@mirror.example.org:o/x.git + jobs: + ship: + runs-on: ubuntu-latest + env: + UPLOAD_URL: https://upload.example.com/v1 + steps: + - run: | + curl -H "t: ${{ secrets.TOKEN }}" "$UPLOAD_URL" && git push "$MIRROR" + """, + "ship.yml" + ) + + write_deed( + repo, + ~s|(egress (job :workflow ".github/workflows/ship.yml" :job "ship" | <> + ~s|:secrets ("TOKEN") :endpoints () :enforcement none))| + ) + + assert [finding] = ResearchExtensions.re001_missing_harden_runner(repo) + assert finding.reason =~ ~s|"upload.example.com:443"| + assert finding.reason =~ ~s|"mirror.example.org:22"| + File.rm_rf!(repo) + end end # What is read through an alias is reported at the alias (the old line From dd28f3c81eb788be40007d570207e72ede4a832b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:12:01 +0000 Subject: [PATCH 12/14] RE001: tighten endpoint discovery and the port comparison; parse once in scan MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex's review of eef60a6, each fix with a test that fails on it: - A deed endpoint without a port claims every port, as an allowed entry without one does, so it is let out only by an allowed entry without a port: "api.example.com" is not covered by `api.example.com:443`. - A workflow `env:` value the job sets again is not the job's, so its host is not required in the deed. - A step's `name`, `id` and `if` name no endpoint: the runner never connects to them. - Database and broker URLs (postgres, mysql/mariadb, redis/rediss, mongodb, mongodb+srv, AMQP, MQTT, LDAP, SMTP, SFTP) are read at their scheme's default port; mongodb+srv's port is the SRV record's, so unknown. - A `#` after a control or redirection operator (`done;# …`, `a&&#…`) opens a shell comment, as the shell reads it. - scan/2 reads each workflow once for RE001 and RE002 (a test holds scan's RE001/RE002 output to the entry points'). The "must agree" test now declares hex.pm:443, not a portless hex.pm. RE001/RE002 on the six repositories, and on their live default branches, give the same findings before and after. CHANGELOG notes eef60a6's env hosts too. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- CHANGELOG.adoc | 9 ++- lib/rules/research_extensions.ex | 80 ++++++++++++++---- test/research_extensions_test.exs | 129 +++++++++++++++++++++++++++++- 3 files changed, 198 insertions(+), 20 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 52a4b76d..a32e0315 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -81,7 +81,14 @@ model instead of scanning lines (WH013 and WH014 follow, and (`git commit -m "fix #12" && git push …`) when looking for comments; keeps the literal host of an allowed entry whose port is an expression; and holds an allowed entry with no port (every port) to a declaration - with none. RE002 skips a job whose `if:` admits only events other than + with none, and a declaration with no port to an allowed entry with none. + Hosts are now also read from the job's and the workflow's `env:` (a + workflow value the job sets again is not the job's), but not from a + step's `name`, `id` or `if`; database and broker URLs + (`postgres://`, `rediss://`, `mongodb+srv://`, AMQP, MQTT, LDAP, SMTP, + SFTP) are read at their scheme's default port; and a `#` after a shell + control operator (`done;# …`) opens a comment. `scan/2` parses each + workflow once for RE001 and RE002. RE002 skips a job whose `if:` admits only events other than `push` and `release`, and reports a workflow the reader refuses if it names harden-runner (the line reader used to find its `audit` there). A job or step read through an alias is reported at the alias again, not diff --git a/lib/rules/research_extensions.ex b/lib/rules/research_extensions.ex index 2aeb5523..404ac3e4 100644 --- a/lib/rules/research_extensions.ex +++ b/lib/rules/research_extensions.ex @@ -284,7 +284,12 @@ defmodule Hypatia.Rules.ResearchExtensions do Severity: `:high` or `:warn`, as above (`:warn` for an unreadable workflow). Action: `:report`. """ - def re001_missing_harden_runner(repo_path) do + def re001_missing_harden_runner(repo_path), + do: re001_findings(repo_path, re001_workflows(repo_path)) + + # RE001 over workflows already read, so that scan/2 reads each once for + # RE001 and RE002. + defp re001_findings(repo_path, workflows) do {deed_file, declared, deed_note} = case Hypatia.Deed.egress_declarations(repo_path) do {:ok, file, jobs} -> {file, Map.new(jobs, &{{&1.workflow, &1.job}, &1}), nil} @@ -292,7 +297,6 @@ defmodule Hypatia.Rules.ResearchExtensions do {:error, file, reason} -> {file, %{}, "the repo deed declares nothing (#{reason})"} end - workflows = re001_workflows(repo_path) jobs = for {:ok, rel, doc} <- workflows, job <- re001_jobs(rel, doc), do: job # A workflow that names secrets but cannot be read is reported. Its @@ -462,9 +466,13 @@ defmodule Hypatia.Rules.ResearchExtensions do harden_policy: harden_step && harden_runner_policy(harden_step), allowed_endpoints: harden_step && harden_runner_allowed(harden_step), # A literal endpoint in the job's or the workflow's `env:` reaches every - # step (`$UPLOAD_URL`), so it is named as surely as one in a step. + # step (`$UPLOAD_URL`), so it is named as surely as one in a step, + # unless the job sets the same variable itself. named_hosts: - Enum.flat_map([workflow.env, job.env | Enum.map(steps, & &1.node)], &named_hosts/1), + Enum.flat_map( + job_env_entries(workflow.env, job.env) ++ Enum.flat_map(steps, &step_entries/1), + &named_hosts(&1.value) + ), exposures: re001_exposures(steps, job_untrusted_events), shared?: shared_line != nil } @@ -757,7 +765,8 @@ defmodule Hypatia.Rules.ResearchExtensions do @host ~S"[A-Za-z0-9](?:[A-Za-z0-9.-]*[A-Za-z0-9])?\.[A-Za-z]{2,}|(?:\d{1,3}\.){3}\d{1,3}(?![\w-]|\.\w)" # A URL's scheme (in any case, as clients read it), host, and port: digits, # or an expression (`:${{ vars.PORT }}`), whose value is known only at run time. - @url_host ~r<\b(https?|wss?|ssh|git|ftps?)://(?:[^@/\s"'`]+@)?(#{@host})(?::(\d{1,5})|(:\$\{\{))?>i + # The schemes are the web's, and the databases' and brokers' a job reaches. + @url_host ~r<\b(https?|wss?|ssh|s?ftp|ftps|git|postgres(?:ql)?|mysql|mariadb|rediss?|mongodb(?:\+srv)?|amqps?|mqtts?|ldaps?|smtps?)://(?:[^@/\s"'`]+@)?(#{@host})(?::(\d{1,5})|(:\$\{\{))?>i # A `user@host:path` remote. The path is not blank (`a@example.com: failed` # is prose) and not a port (`user:pass@host:5432/db` is a URL's userinfo), # though it may start with a digit (`git@gitlab.com:123team/x.git`). @@ -770,10 +779,41 @@ defmodule Hypatia.Rules.ResearchExtensions do "ssh" => 22, "git" => 9418, "ftp" => 21, - "ftps" => 990 + "ftps" => 990, + "sftp" => 22, + "postgres" => 5432, + "postgresql" => 5432, + "mysql" => 3306, + "mariadb" => 3306, + "redis" => 6379, + "rediss" => 6379, + "mongodb" => 27017, + # mongodb+srv: the SRV record names the port, so it is unknown (nil). + "amqp" => 5672, + "amqps" => 5671, + "mqtt" => 1883, + "mqtts" => 8883, + "ldap" => 389, + "ldaps" => 636, + "smtp" => 25, + "smtps" => 465 } - # The hosts outside GitHub one step names literally, as {host, port, line}. + # The `env:` entries a job's steps see: the job's own, and the workflow's + # that the job does not set again. + defp job_env_entries(workflow_env, job_env) do + own = Workflow.entries(job_env) + keys = MapSet.new(own, &Workflow.text(&1.key)) + Enum.reject(Workflow.entries(workflow_env), &(Workflow.text(&1.key) in keys)) ++ own + end + + # A step's entries that can reach the network: not its label (`name`, `id`) + # or its condition (`if`), which the runner never connects to. + @step_labels ~w(name id if) + defp step_entries(step), + do: Enum.reject(Workflow.entries(step.node), &(Workflow.text(&1.key) in @step_labels)) + + # The hosts outside GitHub a node names literally, as {host, port, line}. defp named_hosts(node) do for {text, line_of} <- Workflow.strings(node), {host, port, at} <- url_hosts(text) ++ scp_hosts(text), @@ -786,9 +826,10 @@ defmodule Hypatia.Rules.ResearchExtensions do defp loopback?(host), do: Regex.match?(~r/\A(?:127\.|0\.0\.0\.0\z)/, host) - # Is offset `at` inside a `#` comment: after a `#` that starts the line or - # follows a blank, outside quotes? (A URL fragment, `/#x`, is not one, nor - # is the `#` of `git commit -m "fix #12"`.) + # Is offset `at` inside a `#` comment: after a `#` that starts a word (at + # the start of the line, or after a blank or a control or redirection + # operator: `; & | ( ) < >`), outside quotes? (A URL fragment, `/#x`, is + # not one, nor is the `#` of `git commit -m "fix #12"`.) defp in_shell_comment?(text, at) do line_start = case :binary.matches(binary_part(text, 0, at), "\n") do @@ -802,6 +843,7 @@ defmodule Hypatia.Rules.ResearchExtensions do # Walks one line: `quote` is the open quote character or nil, `word_start?` # whether the next character starts a word. A backslash escapes the next # character outside single quotes, as the shell reads it. + @word_breaks [?\s, ?\t, ?;, ?&, ?|, ?(, ?), ?<, ?>] defp comment_opens?(<<>>, _quote, _word_start?), do: false defp comment_opens?(<>, nil, true), do: true @@ -814,7 +856,7 @@ defmodule Hypatia.Rules.ResearchExtensions do defp comment_opens?(<>, c, _), do: comment_opens?(rest, nil, false) defp comment_opens?(<>, quote, _), - do: comment_opens?(rest, quote, quote == nil and c in [?\s, ?\t]) + do: comment_opens?(rest, quote, quote == nil and c in @word_breaks) # A port written as an expression is unknown (nil), not the scheme's default. defp url_hosts(text) do @@ -920,10 +962,12 @@ defmodule Hypatia.Rules.ResearchExtensions do # them, and the hardener's list is not held to them. undeclared = Enum.reject(allowed, fn {h, p} -> Enum.any?(declared, &covers?(&1, h, p)) end) + # A declared endpoint without a port claims every port, so only an + # allowed entry without a port lets it out. blocked = Enum.reject(declared, fn {h, p} -> String.starts_with?(h, "*.") or Regex.match?(@github_hosts, h) or - Enum.any?(allowed, &covers?(&1, h, p)) + Enum.any?(allowed, &covers?(&1, h, p || :any)) end) if undeclared == [] and blocked == [] do @@ -1035,9 +1079,10 @@ defmodule Hypatia.Rules.ResearchExtensions do Severity: `:high` (`:warn` for an unreadable workflow). Action: `:report`. """ - def re002_harden_runner_audit_mode(repo_path) do - workflows = re001_workflows(repo_path) + def re002_harden_runner_audit_mode(repo_path), + do: re002_findings(re001_workflows(repo_path)) + defp re002_findings(workflows) do unreadable = for {:unreadable, rel, error, bytes} <- workflows, Regex.match?(~r/harden-runner/i, bytes), @@ -1706,9 +1751,12 @@ defmodule Hypatia.Rules.ResearchExtensions do standard scan-result map. """ def scan(repo_path, _opts \\ []) do + # RE001 and RE002 read the same parsed workflows. + workflows = re001_workflows(repo_path) + findings = - re001_missing_harden_runner(repo_path) ++ - re002_harden_runner_audit_mode(repo_path) ++ + re001_findings(repo_path, workflows) ++ + re002_findings(workflows) ++ re003_cache_key_poisoning(repo_path) ++ re004_container_tag_pin(repo_path) ++ re005_test_swallows_exit(repo_path) ++ diff --git a/test/research_extensions_test.exs b/test/research_extensions_test.exs index 8d707fbe..e0c51890 100644 --- a/test/research_extensions_test.exs +++ b/test/research_extensions_test.exs @@ -2025,12 +2025,14 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do end agree = steps.("api.github.com:443 hex.pm:443 repo.hex.pm:443") - assert endpoint_findings(agree, ~s|"hex.pm" "*.hex.pm:443"|) == [] + assert endpoint_findings(agree, ~s|"hex.pm:443" "*.hex.pm:443"|) == [] - assert [finding] = endpoint_findings(agree, ~s|"hex.pm"|) + assert [finding] = endpoint_findings(agree, ~s|"hex.pm:443"|) assert finding.reason =~ ~s|lets out undeclared "repo.hex.pm:443"| - assert [finding] = endpoint_findings(steps.("hex.pm:443"), ~s|"hex.pm" "cdn.example.com"|) + assert [finding] = + endpoint_findings(steps.("hex.pm:443"), ~s|"hex.pm:443" "cdn.example.com"|) + assert finding.reason =~ ~s|does not allow declared "cdn.example.com"| end @@ -2184,6 +2186,127 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do assert finding.reason =~ ~s|"mirror.example.org:22"| File.rm_rf!(repo) end + + test "a workflow env value the job overrides is not the job's" do + repo = + create_repo_with_workflow( + """ + on: push + env: + UPLOAD_URL: https://old.example.com/v1 + jobs: + ship: + runs-on: ubuntu-latest + env: + UPLOAD_URL: https://new.example.com/v1 + steps: + - run: | + curl -H "t: ${{ secrets.TOKEN }}" "$UPLOAD_URL" + """, + "ship.yml" + ) + + write_deed( + repo, + ~s|(egress (job :workflow ".github/workflows/ship.yml" :job "ship" | <> + ~s|:secrets ("TOKEN") :endpoints ("new.example.com:443") :enforcement none))| + ) + + assert ResearchExtensions.re001_missing_harden_runner(repo) == [] + File.rm_rf!(repo) + end + + test "a step's name, id and condition name no endpoint" do + steps = """ + - name: Read https://docs.example.com before deploying + id: deploy + if: ${{ !contains(github.event.head_commit.message, 'https://skip.example.com') }} + run: ./deploy --token ${{ secrets.TOKEN }} + """ + + assert endpoint_findings(steps, "") == [] + end + + test "a database or broker URL names its host, at the scheme's default port" do + steps = """ + - run: | + psql postgres://db.example.com/app + redis-cli -u rediss://cache.example.com:6380 + mongosh "mongodb+srv://cluster0.example.net/app" + env: + K: ${{ secrets.TOKEN }} + """ + + assert [finding] = endpoint_findings(steps, "") + assert finding.reason =~ ~s|"db.example.com:5432"| + assert finding.reason =~ ~s|"cache.example.com:6380"| + # An SRV record names the port, so any declared port of the host covers it. + assert finding.reason =~ ~s|"cluster0.example.net"| + + assert endpoint_findings( + steps, + ~s|"db.example.com:5432" "cache.example.com:6380" "cluster0.example.net:27017"| + ) == [] + end + + test "a # after a shell control operator opens a comment" do + steps = """ + - run: | + echo done;# curl https://comment.example.com + make&&#curl https://comment2.example.com + echo 'a;# b' https://up.example.com + env: + K: ${{ secrets.TOKEN }} + """ + + assert [finding] = endpoint_findings(steps, "") + assert finding.reason =~ ~s|"up.example.com:443"| + refute finding.reason =~ "comment" + end + + test "a declaration without a port claims every port, so one allowed port blocks it" do + steps = """ + - uses: step-security/harden-runner@v2 + with: + egress-policy: block + allowed-endpoints: api.example.com:443 + - run: deploy --token ${{ secrets.TOKEN }} + """ + + assert [finding] = endpoint_findings(steps, ~s|"api.example.com"|) + assert finding.reason =~ ~s|does not allow declared "api.example.com"| + assert endpoint_findings(steps, ~s|"api.example.com:443"|) == [] + end + end + + describe "scan/2" do + test "gives RE001 and RE002 exactly as their own entry points do" do + repo = + create_repo_with_workflow( + """ + on: push + jobs: + ship: + runs-on: ubuntu-latest + steps: + - uses: step-security/harden-runner@v2 + with: + egress-policy: audit + - run: npm ci && deploy --token ${{ secrets.TOKEN }} + """, + "ship.yml" + ) + + findings = ResearchExtensions.scan(repo).findings + re00x = Enum.filter(findings, &(&1.rule in ["RE001", "RE002"])) + + assert re00x == + ResearchExtensions.re001_missing_harden_runner(repo) ++ + ResearchExtensions.re002_harden_runner_audit_mode(repo) + + assert Enum.any?(re00x, &(&1.rule == "RE002")) + File.rm_rf!(repo) + end end # What is read through an alias is reported at the alias (the old line From 30c5e3fd8447dcb8467156a6721293436735ee12 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:21:19 +0000 Subject: [PATCH 13/14] RE001: an inherited env value reaches only the steps that do not set it again Codex on dd28f3c: a job env URL that every step overrides reaches no step, but its host was still required in the deed. Hosts are now read step by step, from the step's own entries and the workflow and job `env:` entries the step does not set again. The test fails on dd28f3c; one step that does not override still makes the job's host required. RE001/RE002 on the six repositories and their live default branches are unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDithtn5Xk5MbSPm4Px --- CHANGELOG.adoc | 3 ++- lib/rules/research_extensions.ex | 30 ++++++++++++++-------- test/research_extensions_test.exs | 42 +++++++++++++++++++++++++++++++ 3 files changed, 64 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index a32e0315..707c577a 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -83,7 +83,8 @@ model instead of scanning lines (WH013 and WH014 follow, and and holds an allowed entry with no port (every port) to a declaration with none, and a declaration with no port to an allowed entry with none. Hosts are now also read from the job's and the workflow's `env:` (a - workflow value the job sets again is not the job's), but not from a + value is not counted where the job or the step sets the same + variable again), but not from a step's `name`, `id` or `if`; database and broker URLs (`postgres://`, `rediss://`, `mongodb+srv://`, AMQP, MQTT, LDAP, SMTP, SFTP) are read at their scheme's default port; and a `#` after a shell diff --git a/lib/rules/research_extensions.ex b/lib/rules/research_extensions.ex index 404ac3e4..f89e4df2 100644 --- a/lib/rules/research_extensions.ex +++ b/lib/rules/research_extensions.ex @@ -465,14 +465,10 @@ defmodule Hypatia.Rules.ResearchExtensions do hardened?: harden_step != nil, harden_policy: harden_step && harden_runner_policy(harden_step), allowed_endpoints: harden_step && harden_runner_allowed(harden_step), - # A literal endpoint in the job's or the workflow's `env:` reaches every - # step (`$UPLOAD_URL`), so it is named as surely as one in a step, - # unless the job sets the same variable itself. - named_hosts: - Enum.flat_map( - job_env_entries(workflow.env, job.env) ++ Enum.flat_map(steps, &step_entries/1), - &named_hosts(&1.value) - ), + # A literal endpoint in the job's or the workflow's `env:` reaches a + # step (`$UPLOAD_URL`) that does not set the same variable itself, so + # it is named as surely as one in that step. + named_hosts: job_named_hosts(workflow, job, steps), exposures: re001_exposures(steps, job_untrusted_events), shared?: shared_line != nil } @@ -799,8 +795,22 @@ defmodule Hypatia.Rules.ResearchExtensions do "smtps" => 465 } - # The `env:` entries a job's steps see: the job's own, and the workflow's - # that the job does not set again. + # The hosts a job's steps name: in each step's own entries, and in the + # inherited `env:` entries the step does not set again. + defp job_named_hosts(workflow, job, steps) do + inherited = job_env_entries(workflow.env, job.env) + + steps + |> Enum.flat_map(fn step -> + own = MapSet.new(Workflow.entries(step.env), &Workflow.text(&1.key)) + Enum.reject(inherited, &(Workflow.text(&1.key) in own)) ++ step_entries(step) + end) + |> Enum.uniq() + |> Enum.flat_map(&named_hosts(&1.value)) + end + + # The `env:` entries a job passes to its steps: its own, and the + # workflow's that the job does not set again. defp job_env_entries(workflow_env, job_env) do own = Workflow.entries(job_env) keys = MapSet.new(own, &Workflow.text(&1.key)) diff --git a/test/research_extensions_test.exs b/test/research_extensions_test.exs index e0c51890..1cc24d51 100644 --- a/test/research_extensions_test.exs +++ b/test/research_extensions_test.exs @@ -2216,6 +2216,48 @@ defmodule Hypatia.Rules.ResearchExtensionsTest do File.rm_rf!(repo) end + test "a job env value every step sets again reaches no step" do + job = fn second_step -> + """ + on: push + jobs: + ship: + runs-on: ubuntu-latest + env: + UPLOAD_URL: https://old.example.com/v1 + steps: + - run: | + curl -H "t: ${{ secrets.TOKEN }}" "$UPLOAD_URL" + env: + UPLOAD_URL: https://new.example.com/v1 + #{second_step} + """ + end + + findings = fn yaml -> + repo = create_repo_with_workflow(yaml, "ship.yml") + + write_deed( + repo, + ~s|(egress (job :workflow ".github/workflows/ship.yml" :job "ship" | <> + ~s|:secrets ("TOKEN") :endpoints ("new.example.com:443") :enforcement none))| + ) + + result = ResearchExtensions.re001_missing_harden_runner(repo) + File.rm_rf!(repo) + result + end + + overridden = + " - run: echo done\n env:\n UPLOAD_URL: https://new.example.com/v2" + + assert findings.(job.(overridden)) == [] + + # One step that does not set it sees the job's value. + assert [finding] = findings.(job.(" - run: echo done")) + assert finding.reason =~ ~s|"old.example.com:443"| + end + test "a step's name, id and condition name no endpoint" do steps = """ - name: Read https://docs.example.com before deploying From 4badaf9a143c08f47d762efa8e54c76b8ad2aba4 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 9 Nov 2026 21:22:43 +0000 Subject: [PATCH 14/14] docs: clarify workflow parsing, egress checks, and Idris proofs --- lib/hypatia/workflow.ex | 29 ++++++++++++++++++---- lib/rules/research_extensions.ex | 19 ++++++++++++-- src/Hypatia/ABI/Egress.idr | 3 +++ verification/proofs/idris2/KyamlBudget.idr | 9 +++++++ 4 files changed, 53 insertions(+), 7 deletions(-) diff --git a/lib/hypatia/workflow.ex b/lib/hypatia/workflow.ex index 4a968a32..dca3bfa2 100644 --- a/lib/hypatia/workflow.ex +++ b/lib/hypatia/workflow.ex @@ -57,13 +57,21 @@ defmodule Hypatia.Workflow do @type t :: %__MODULE__{} @doc """ - Reads a workflow file. `{:ok, nil}` for an empty stream. + Reads a workflow file and returns the result of `parse/2`, with its path + stored in the model. Returns `{:ok, nil}` for an empty stream. + + Raises `File.Error` if the file cannot be read. """ def read(path), do: path |> File.read!() |> parse(path) @doc """ Parses a workflow's bytes into the model. The first document is the - workflow; `{:ok, nil}` for an empty stream. + workflow; `{:ok, nil}` for an empty stream. Returns `{:ok, workflow}` on + success, storing `path` as supplied without reading it. + + Returns `{:error, %Hypatia.Kyaml.Error{}}` for a KYAML parse error + anywhere in the stream or when the first document exceeds the expanded + node budget. """ def parse(bytes, path \\ nil) when is_binary(bytes) do case Kyaml.parse(bytes) do @@ -153,7 +161,11 @@ defmodule Hypatia.Workflow do end end - @doc "A step input's value (`with: {egress-policy: block}`), or nil." + @doc """ + A step input's scalar text (`with: {egress-policy: block}`), as returned by + `text/1`; `nil` if the input is missing or is a collection. The name matches + the resolved string key exactly. + """ def input(%Step{with: with}, name), do: with |> Kyaml.get(name) |> text() @doc """ @@ -191,11 +203,18 @@ defmodule Hypatia.Workflow do The string values under a node in document order, each with a function from a byte offset in the value to its source line. A block scalar maps each of its lines; through an alias, every offset maps to the alias's line. - The walk is bounded like the reader: past kyq's node budget a node yields - nothing more. + Returns `{value, line_of}` pairs. Offsets are zero-based bytes and source + lines are one-based. Mapping keys and non-string scalars are omitted. + Returns `[]` for `nil` or a node exceeding kyq's expanded node budget; + no partial results are returned. """ def strings(node), do: strings(node, nil) + @doc """ + Like `strings/1`, with an optional source line override. When `alias_line` + is non-nil, every returned offset mapper reports that line, including + values reached through nested aliases. + """ def strings(nil, _), do: [] def strings(node, alias_line) do diff --git a/lib/rules/research_extensions.ex b/lib/rules/research_extensions.ex index f89e4df2..31c853ce 100644 --- a/lib/rules/research_extensions.ex +++ b/lib/rules/research_extensions.ex @@ -210,7 +210,12 @@ defmodule Hypatia.Rules.ResearchExtensions do whose `(:workflow, :job)` names the job and whose `:secrets` equal the secrets it references. - An undeclared job is reported. Its **exposures** are the evidence: + A declaration is checked even when a hardener is present. Enforcement + `none` needs no hardener, `harden-runner-audit` needs a hardener in any + mode, and `harden-runner-block` needs its policy to be `block`. + + A job with neither a hardener nor a declaration is reported. Its + **exposures** are the evidence: * the workflow runs on an untrusted-input event (`pull_request_target`, `issue_comment`, `issues`, `workflow_run`, …), narrowed by a job `if:` @@ -283,6 +288,8 @@ defmodule Hypatia.Rules.ResearchExtensions do Severity: `:high` or `:warn`, as above (`:warn` for an unreadable workflow). Action: `:report`. + Returns a list of findings, or `[]` when none are found. + Raises `File.Error` if workflow directory listing or file reading fails. """ def re001_missing_harden_runner(repo_path), do: re001_findings(repo_path, re001_workflows(repo_path)) @@ -1087,7 +1094,10 @@ defmodule Hypatia.Rules.ResearchExtensions do unreadable (`:warn`): its hardener cannot be checked, and a silent skip would read as a pass. + Returns one finding per workflow with an audit-mode hardener on a + qualifying trigger, or `[]` when none are found. Severity: `:high` (`:warn` for an unreadable workflow). Action: `:report`. + Raises `File.Error` if workflow directory listing or file reading fails. """ def re002_harden_runner_audit_mode(repo_path), do: re002_findings(re001_workflows(repo_path)) @@ -1758,7 +1768,12 @@ defmodule Hypatia.Rules.ResearchExtensions do @doc """ Run every research-extension check on `repo_path` and return the - standard scan-result map. + scan-result map: `:findings`, `:total`, counts in `:by_severity`, and + recommendations in `:dispatch`. Options are currently ignored. + + Raises `File.Error` if workflow directory listing or a scanned file read + fails. RE001 and RE002 convert KYAML errors into unreadable-workflow + findings when the file names secrets or harden-runner, respectively. """ def scan(repo_path, _opts \\ []) do # RE001 and RE002 read the same parsed workflows. diff --git a/src/Hypatia/ABI/Egress.idr b/src/Hypatia/ABI/Egress.idr index 3af53279..063f8ae8 100644 --- a/src/Hypatia/ABI/Egress.idr +++ b/src/Hypatia/ABI/Egress.idr @@ -77,10 +77,12 @@ data Clean : Job -> Maybe Decl -> Type where -- ─── Decidability: RE001 is a decision procedure ─────────────────────── +||| Decides whether every element of `xs` occurs in `ys`; order and multiplicity do not matter. public export decElems : (xs, ys : List String) -> Dec (All (\x => Elem x ys) xs) decElems xs ys = all (\x => isElem x ys) xs +||| Decides mutual secret membership, ignoring order and duplicate occurrences. public export decSame : (xs, ys : List String) -> Dec (SameSecrets xs ys) decSame xs ys with (decElems xs ys) @@ -89,6 +91,7 @@ decSame xs ys with (decElems xs ys) _ | Yes b = Yes (a, b) _ | No no = No (\(_, b) => no b) +||| Decides whether the hardener satisfies the claim; `None` holds even without a hardener. public export decHolds : (e : Enforcement) -> (h : Maybe Policy) -> Dec (Holds e h) decHolds None h = Yes ClaimsNothing diff --git a/verification/proofs/idris2/KyamlBudget.idr b/verification/proofs/idris2/KyamlBudget.idr index 574eef77..9807b961 100644 --- a/verification/proofs/idris2/KyamlBudget.idr +++ b/verification/proofs/idris2/KyamlBudget.idr @@ -64,6 +64,7 @@ mutual size (Coll cs) = S (sizes cs) size (Alias t) = size t + ||| The sum of expanded node sizes, counting a shared target once per occurrence. public export sizes : List Node -> Nat sizes [] = 0 @@ -87,13 +88,16 @@ mutual -- ─── What the count reports ──────────────────────────────────────────── +||| Extracts equality of values from equality of their `Just` wrappers. justInj : Just a = Just b -> a = b justInj Refl = Refl +||| Composes two non-strict bounds. lteTrans : LTE a b -> LTE b c -> LTE a c lteTrans LTEZero _ = LTEZero lteTrans (LTESucc x) (LTESucc y) = LTESucc (lteTrans x y) +||| Expanded sizes add when two node stacks are concatenated. sizesAppend : (xs, ys : List Node) -> sizes (xs ++ ys) = sizes xs + sizes ys sizesAppend [] ys = Refl sizesAppend (x :: xs) ys = @@ -191,6 +195,7 @@ mutual Nil : Each [] (::) : NoChain x -> Each xs -> Each (x :: xs) +||| Preserves the absence of alias chains when concatenating node lists. eachAppend : Each xs -> Each ys -> Each (xs ++ ys) eachAppend [] ys = ys eachAppend (x :: xs) ys = x :: eachAppend xs ys @@ -201,12 +206,14 @@ aliasOnTop : List Node -> Nat aliasOnTop (Alias _ :: _) = 1 aliasOnTop _ = 0 +||| The extra fuel owed by the top node is at most one. aliasOnTopBit : (s : List Node) -> LTE (aliasOnTop s) 1 aliasOnTopBit (Alias _ :: _) = LTESucc LTEZero aliasOnTopBit [] = LTEZero aliasOnTopBit (Leaf :: _) = LTEZero aliasOnTopBit (Coll _ :: _) = LTEZero +||| A non-alias at the top of the stack owes no alias step. notAliasOnTop : NotAlias t -> aliasOnTop (t :: r) = 0 notAliasOnTop LeafIsNot = Refl notAliasOnTop CollIsNot = Refl @@ -216,6 +223,7 @@ public export steps : (m : Nat) -> List Node -> Nat steps m stack = S (m + m + aliasOnTop stack) +||| A successor never compares as less than or equal to its predecessor. lteSuccFalse : (l : Nat) -> lte (S l) l = False lteSuccFalse Z = Refl lteSuccFalse (S l) = lteSuccFalse l @@ -280,6 +288,7 @@ countBounded limit doc ok = -- ─── Completeness without a premise on the count ─────────────────────── +||| Extracts a value and its equality witness from evidence that a result is `Just`. isJustValue : (m : Maybe a) -> IsJust m -> (k ** m = Just k) isJustValue (Just k) ItIsJust = (k ** Refl)