diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 62980ffc..269522e2 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 @@ -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 b9115f0c..41569ed5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -357,6 +357,9 @@ 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/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 2a32f694..707c577a 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -31,6 +31,105 @@ 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, 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 + 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. +* **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, 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 + 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 + 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 + 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 +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. + +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 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 + (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. + ==== 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/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/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/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/kyaml.ex b/lib/hypatia/kyaml.ex index 783edfe5..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, 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) + 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) @@ -927,16 +936,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 @@ -950,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, @@ -981,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 [?', ?"] -> @@ -1199,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( @@ -1215,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/lib/hypatia/workflow.ex b/lib/hypatia/workflow.ex new file mode 100644 index 00000000..dca3bfa2 --- /dev/null +++ b/lib/hypatia/workflow.ex @@ -0,0 +1,255 @@ +# 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 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. 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 + {: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 + + # 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 + %Job{ + id: key.value, + line: elem(key.loc, 0), + node: value, + 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 + run = child(item, "run") + + %Step{ + line: elem(item.loc, 0), + node: item, + uses: text(child(item, "uses")), + run: text(run), + run_style: run && Kyaml.deref(run)[:style], + 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). + """ + 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 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 """ + 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)}) + + 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`): + 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. + 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 + 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..31c853ce 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)/ @@ -224,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:` @@ -253,40 +244,59 @@ 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 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 (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. + + ## 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`. + 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 + 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} @@ -294,10 +304,16 @@ 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) + 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, bytes} <- workflows, + Regex.match?(~r/secrets/i, bytes), + do: {rel, error} + + unread = MapSet.new(for {:unreadable, rel, _, _} <- workflows, do: rel) job_findings = Enum.flat_map(jobs, fn job -> @@ -338,7 +354,7 @@ defmodule Hypatia.Rules.ResearchExtensions do [] end - dynamic ++ drift ++ enforcement + dynamic ++ drift ++ enforcement ++ re001_endpoint_findings(job, deed_file, decl) end end) @@ -348,97 +364,135 @@ 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, rel, error, bytes}. + 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, 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), + # 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 + } + 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 +506,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) - - 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,9 +522,87 @@ 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. 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. @@ -620,373 +744,333 @@ 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). Each is a + # whole domain or a subdomain of one: `notgithubusercontent.com` is not. + @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/ + + # A host a workflow can name: a dotted domain name, or a literal IPv4 + # address. A single-label name (`localhost`, a service container such as + # `postgres`) is not egress and is not compared. + @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. + # 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`). + @scp_host ~r/(? 80, + "ws" => 80, + "https" => 443, + "wss" => 443, + "ssh" => 22, + "git" => 9418, + "ftp" => 21, + "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 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 - 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) - - [ - 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) + # 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)) + Enum.reject(Workflow.entries(workflow_env), &(Workflow.text(&1.key) in keys)) ++ own 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) + # 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), + 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 - 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) + 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 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 + [] -> 0 + matches -> matches |> List.last() |> elem(0) |> Kernel.+(1) + end - [head? && :head, Regex.match?(@re001_fetched_code, run) && :fetched] - |> Enum.filter(& &1) + comment_opens?(binary_part(text, line_start, at - line_start), nil, true) 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 - {_, []} -> - [] + # 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 - {_, [{run_line, _} | rest]} -> - [prefix, value] = - Regex.run(~r/^(\s*(?:-\s+)?)(?:run|"run"|'run')\s*:\s*(.*)$/, run_line, - capture: :all_but_first - ) + defp comment_opens?(<>, nil, _) when c in [?', ?"], + do: comment_opens?(rest, c, false) - key_column = String.length(prefix) + defp comment_opens?(<>, quote, _) when quote != ?', + do: comment_opens?(rest, quote, false) - # 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 comment_opens?(<>, c, _), do: comment_opens?(rest, nil, false) - Enum.map(body, &String.replace(&1, ~r/(?:^|\s)#.*$/, "")) - end - end + defp comment_opens?(<>, quote, _), + do: comment_opens?(rest, quote, quote == nil and c in @word_breaks) - # 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) + # 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) do + scheme = String.downcase(binary_part(text, s, sl)) - _ -> - false - end - end + 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 - # 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] - - [] -> - [] + {binary_part(text, h, hl), port, at} 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 + 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 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 + # The literal entries of a harden-runner step's `allowed-endpoints` input + # (`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; 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 -> + nil + + text -> + text + |> String.replace(@expression, "\0") + |> String.split(~r/[\s,]+/, trim: true) + |> 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 - # 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 any_port({host, nil}), do: {host, :any} + defp any_port(endpoint), do: endpoint - {_, [{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 + # 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 - # `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 + # 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 (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 + "*." <> suffix -> String.ends_with?(host, "." <> suffix) + _ -> pattern == host + end - defp inline_events(scalar_or_list) do - ~r/[A-Za-z_]+/ |> Regex.scan(scalar_or_list) |> List.flatten() + host_ok and (want in [nil, :any] or port == nil or want == port) 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 re001_endpoint_findings(job, deed_file, decl) do + declared = decl.endpoints |> Enum.map(&literal_endpoint/1) |> Enum.reject(&is_nil/1) - # 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 + 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) - # 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 + named = + if uncovered == [], + do: [], + else: [re001_unnamed_endpoints(job, deed_file, uncovered)] + + named ++ allowed_endpoint_findings(job, deed_file, declared) end - defp with_key_parts(line) do - case Regex.run(@with_key, line) do - [_, lead, inline] -> [lead, String.trim(inline)] - [_, lead] -> [lead, ""] + defp allowed_endpoint_findings(%{allowed_endpoints: nil}, _deed_file, _declared), do: [] + + defp allowed_endpoint_findings(job, deed_file, declared) do + 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 + # 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) + + # 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 || :any)) + end) + + 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, port}) when port in [nil, :any], 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) + + %{ + 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 - Regex.match?(~r/^'(?:[^']|'')*'$/, value) -> - value |> String.slice(1..-2//1) |> String.replace("''", "'") + 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 + ) - true -> - value - end + %{ + 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 +1081,92 @@ defmodule Hypatia.Rules.ResearchExtensions do becomes a finding when it persists on a workflow that touches protected branches (or runs on `push` to default). - Severity: `:high`. Action: `:report`. + 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:`, 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. + + 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. + + 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 - repo_path - |> workflow_files() - |> Enum.flat_map(fn path -> - content = File.read!(path) - rel = Path.relative_to(path, repo_path) + def re002_harden_runner_audit_mode(repo_path), + do: re002_findings(re001_workflows(repo_path)) - installs_harden? = Regex.match?(~r/uses:\s*step-security\/harden-runner/, content) + defp re002_findings(workflows) do + unreadable = + for {:unreadable, rel, error, bytes} <- workflows, + Regex.match?(~r/harden-runner/i, bytes), + do: re002_unreadable(rel, error) - audit_mode? = Regex.match?(~r/egress-policy:\s*audit\b/, content) + unreadable ++ re002_audit_findings(workflows) + end - 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) + defp re002_audit_findings(workflows) do + for {:ok, rel, %Workflow{} = workflow} <- workflows, + audit = audit_hardeners(workflow), + audit != [] do + defaulted? = Enum.all?(audit, &(&1 == :default)) - 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) + %{ + 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 + + 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 + if Workflow.input(step, "egress-policy"), do: :explicit, else: :default + end end # ─── RE003: cache key interpolates attacker-controlled input ───────── @@ -1637,12 +1768,20 @@ 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. + 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/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..063f8ae8 --- /dev/null +++ b/src/Hypatia/ABI/Egress.idr @@ -0,0 +1,150 @@ +-- 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 ─────────────────────── + +||| 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) + _ | No no = No (\(a, _) => no a) + _ | Yes a with (decElems ys xs) + _ | 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 +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/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/egress_decision_mirror_test.exs b/test/egress_decision_mirror_test.exs new file mode 100644 index 00000000..ed1bc087 --- /dev/null +++ b/test/egress_decision_mirror_test.exs @@ -0,0 +1,174 @@ +# 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, 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 + 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), + 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 + + 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, plus the dynamic-only job) x 4 hardeners, each + # with no declaration or 3 x 3. + assert length(cases) == 28 * 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..785afcd8 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 @@ -169,6 +207,27 @@ 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, ""}}, + # 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 # stream, so the error stands at the character, wherever it is. {"control-character-in-plain", "a: x\u0001y\n", {:error, "CONTROL_CHARACTER", 1, 5, ""}}, diff --git a/test/research_extensions_equivalence_test.exs b/test/research_extensions_equivalence_test.exs new file mode 100644 index 00000000..db91a9b1 --- /dev/null +++ b/test/research_extensions_equivalence_test.exs @@ -0,0 +1,277 @@ +# 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 + + # 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, 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)) + |> 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..1cc24d51 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,11 +1886,635 @@ 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:443" "*.hex.pm:443"|) == [] + + 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:443" "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 + + 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 + + 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 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 + 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 + # 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 ────────────────────────────────────────────────────────── + # 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 + + 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(""" @@ -1923,6 +2554,142 @@ 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 + + # 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/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 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..7e78b2b7 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. |=== @@ -294,6 +295,91 @@ 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 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 + +|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+`); 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 +(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+`) @@ -378,7 +464,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. @@ -448,12 +534,18 @@ 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) +|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/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 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 diff --git a/verification/proofs/idris2/KyamlBudget.idr b/verification/proofs/idris2/KyamlBudget.idr new file mode 100644 index 00000000..9807b961 --- /dev/null +++ b/verification/proofs/idris2/KyamlBudget.idr @@ -0,0 +1,307 @@ +-- 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`: 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 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 +-- 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 + + ||| The sum of expanded node sizes, counting a shared target once per occurrence. + 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 ──────────────────────────────────────────── + +||| 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 = + 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?`: 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 -> + 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) + +||| 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 + +||| 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 + +||| 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 + +||| 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) + +||| 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 + +||| 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 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) +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 ─────────────────────── + +||| 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) + +||| `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