From b850188b07391a7e1515b08115ad86dc78aedf52 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 2 Jun 2026 17:52:42 +0000 Subject: [PATCH 1/3] ci: harden workflows per Hypatia security-scan findings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Address the actionable, in-scope items from the advisory Hypatia scan by mirroring the canonical estate templates from sibling repos (ochrance-framework / valence-shell): - Add codeql.yml (mirrors ochrance-framework: javascript-typescript, build-mode none; SHA-pinned actions). Analyses the repo's committed JS (tools/banner/build-banner.mjs); distinct SARIF category from the advisory Hypatia scan. - Add secret-scanner.yml (calls the estate secret-scanner-reusable, SHA-pinned). - governance.yml: pin the governance-reusable workflow to a SHA instead of @main (matches mirror.yml / scorecard.yml and the sibling repos' pin), closing the unpinned-action finding. - agda.yml (check, cold-check) and hypatia-scan.yml (scan): add timeout-minutes to the real-step jobs, bounding runaway jobs below the 6-hour default. Deliberately NOT changed (documented in the PR): - timeout-minutes is NOT added to governance.yml / mirror.yml / scorecard.yml — those are reusable-workflow callers, where job-level timeout-minutes is invalid YAML; the timeout belongs in the reusable workflow (hyperpolymath/standards). - No synthetic test directory for the "no tests" finding — the Agda proof suite (All.agda / Smoke.agda / characteristic / examples, typechecked in agda.yml) is the verification suite. The Hypatia scan is advisory (non-gating) per hypatia-scan.yml. https://claude.ai/code/session_01Jxr3Wy4ngpkbc2QwjEam82 --- .github/workflows/agda.yml | 7 ++++ .github/workflows/codeql.yml | 50 ++++++++++++++++++++++++++++ .github/workflows/governance.yml | 6 +++- .github/workflows/hypatia-scan.yml | 3 ++ .github/workflows/secret-scanner.yml | 19 +++++++++++ 5 files changed, 84 insertions(+), 1 deletion(-) create mode 100644 .github/workflows/codeql.yml create mode 100644 .github/workflows/secret-scanner.yml diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml index 2381117..52aa4a8 100644 --- a/.github/workflows/agda.yml +++ b/.github/workflows/agda.yml @@ -27,6 +27,10 @@ permissions: read-all jobs: check: runs-on: ubuntu-latest + # Bound the job so a hung typecheck/clone cannot occupy a runner for + # the 6-hour default. Generous upper bound — the warm suite is a few + # minutes; a cold stdlib+suite build is well under this. + timeout-minutes: 30 steps: - name: Checkout uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -148,6 +152,9 @@ jobs: # given the documented WSL git-object-corruption risk). Runs in # parallel with `check`; both must pass. runs-on: ubuntu-latest + # Cold (--ignore-interfaces) build is the slowest path; still well + # under this bound. Caps a runaway/hung job below the 6-hour default. + timeout-minutes: 30 steps: - name: Checkout uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml new file mode 100644 index 0000000..70e8cdc --- /dev/null +++ b/.github/workflows/codeql.yml @@ -0,0 +1,50 @@ +# SPDX-License-Identifier: MPL-2.0 +name: CodeQL Security Analysis + +on: + push: + branches: [main, master] + pull_request: + branches: [main, master] + schedule: + - cron: '0 6 * * 1' + +# Estate guardrail: cancel superseded runs so re-pushes / rebased PR +# updates do not pile up queued runs against the shared account-wide +# Actions concurrency pool. Applied only to read-only check workflows +# (no publish/mutation), so cancelling a superseded run is always safe. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + analyze: + runs-on: ubuntu-latest + timeout-minutes: 30 + permissions: + contents: read + security-events: write + strategy: + fail-fast: false + matrix: + include: + - language: javascript-typescript + build-mode: none + + steps: + - name: Checkout + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + + - name: Initialize CodeQL + uses: github/codeql-action/init@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3 + with: + languages: ${{ matrix.language }} + build-mode: ${{ matrix.build-mode }} + + - name: Perform CodeQL Analysis + uses: github/codeql-action/analyze@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3 + with: + category: "/language:${{ matrix.language }}" diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index faa979b..84d1101 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -30,4 +30,8 @@ permissions: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@main + # Pinned to a SHA (not @main) per the estate supply-chain policy — + # matches the sibling repos' pin (e.g. ochrance-framework). Bump + # deliberately, never float: an unpinned reusable workflow is an + # unpinned trust boundary. mirror.yml / scorecard.yml already pin. + uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@861b5e911d9e5dcfb3c0ab3dd2a9a3c8fd0a1613 diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index dfacf3b..1ea26ad 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -43,6 +43,9 @@ jobs: scan: name: Hypatia Neurosymbolic Analysis runs-on: ubuntu-latest + # Bound the job: clone + Elixir build + scan is minutes, not hours. + # Caps a hung clone/build below the 6-hour default. + timeout-minutes: 20 steps: - name: Checkout repository diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml new file mode 100644 index 0000000..097d2af --- /dev/null +++ b/.github/workflows/secret-scanner.yml @@ -0,0 +1,19 @@ +# SPDX-License-Identifier: MPL-2.0 +name: Secret Scanner + +on: + pull_request: + push: + branches: [main] + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + scan: + uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@3e4bd4c93911750727e2e4c66dff859e00079da0 + secrets: inherit From 7d709f646632d52a7ed07879eb11cc70ec9a722c Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 2 Jun 2026 18:06:20 +0000 Subject: [PATCH 2/3] ci(codeql): add the `actions` language to the analysis matrix MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CodeQL's `actions` language analyses the GitHub Actions workflows themselves — directly relevant to this PR's workflow hardening, and closes the Hypatia `codeql_missing_actions_language` finding that the single-language (javascript-typescript) matrix triggered. https://claude.ai/code/session_01Jxr3Wy4ngpkbc2QwjEam82 --- .github/workflows/codeql.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 70e8cdc..e459e4b 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -33,6 +33,12 @@ jobs: include: - language: javascript-typescript build-mode: none + # Also analyse the GitHub Actions workflows themselves + # (CodeQL `actions` language) — directly relevant given the + # workflow-hardening in this PR, and closes the Hypatia + # `codeql_missing_actions_language` finding. + - language: actions + build-mode: none steps: - name: Checkout From 2dd684e2908f79a8cbcc4cb34f7963d2bc33ce53 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 2 Jun 2026 18:18:29 +0000 Subject: [PATCH 3/3] ci: resolve Hypatia findings at source (dependabot, scorecard perms, false-positive suppressions) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Foundational, in-repo remediation so the advisory Hypatia scan stops re-flagging known issues: Real fixes (close genuine findings): - Add .github/dependabot.yml (github-actions ecosystem, weekly) — closes the OSSF Scorecard "Dependency-Update-Tool" / DependencyUpdate finding. Scoped to github-actions only: echo-types has no Cargo/npm/mix/pip manifests, and Dependabot has no native Nix ecosystem. - scorecard.yml: grant the analysis job the permissions the scorecard-reusable contract documents (contents:read, security-events: write, id-token:write) — closes scorecard_wrapper_missing_job_permissions. Verified false positives, suppressed via the sanctioned .hypatia-ignore mechanism (code_safety rules route through ScannerSuppression): - code_safety/agda_postulate on proofs/agda/Smoke.agda (the "critical"): the rule is a naive \bpostulate\b regex with no comment stripping; the only matches are comments documenting the postulate-free discipline. The repo guardrail (check-guardrails.sh) strips comments and is the real gate; the one real postulate module is isolated and not in the trusted base. - code_safety/js_http_url_in_code on tools/banner/build-banner.mjs: the URL is the SVG XML namespace `xmlns="http://www.w3.org/2000/svg"`, a constant namespace URI, never fetched (must stay http://). Not fixable in-repo (upstream rule/standards-reusable issues; documented in the PR for follow-up): honest_completion/no_tests (Agda proof suite not recognised as tests) and workflow_audit/missing_timeout_minutes on reusable-workflow callers (timeout-minutes is invalid on `uses:` jobs; the real fix is adding timeouts inside the standards reusables and making the rule skip caller jobs). https://claude.ai/code/session_01Jxr3Wy4ngpkbc2QwjEam82 --- .github/dependabot.yml | 19 ++++++++++++++++++ .github/workflows/scorecard.yml | 11 ++++++++++- .hypatia-ignore | 35 +++++++++++++++++++++++++++++++++ 3 files changed, 64 insertions(+), 1 deletion(-) create mode 100644 .github/dependabot.yml create mode 100644 .hypatia-ignore diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 0000000..839d430 --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,19 @@ +# SPDX-License-Identifier: MPL-2.0 +# Dependabot configuration for echo-types. +# +# echo-types is an Agda proof repository with no language package +# manifests (no Cargo.toml / package.json / mix.exs / requirements). +# The relevant ecosystem is GitHub Actions — this keeps the SHA-pinned +# reusable workflows and third-party actions current, and satisfies the +# OSSF Scorecard "Dependency-Update-Tool" check. + +version: 2 +updates: + - package-ecosystem: "github-actions" + directory: "/" + schedule: + interval: "weekly" + groups: + actions: + patterns: + - "*" diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index f99d361..5256dc0 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -8,9 +8,18 @@ on: push: branches: [main] -permissions: read-all +permissions: + contents: read jobs: analysis: + # Caller-granted permissions per the scorecard-reusable contract + # (its header documents: the caller MUST grant security-events:write + # + id-token:write; contents:read lets it read the repo). Closes the + # Hypatia `scorecard_wrapper_missing_job_permissions` finding. + permissions: + contents: read + security-events: write + id-token: write uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@e0caf11508a3989574713c78f5f444f2ce5e33ef secrets: inherit diff --git a/.hypatia-ignore b/.hypatia-ignore new file mode 100644 index 0000000..505318b --- /dev/null +++ b/.hypatia-ignore @@ -0,0 +1,35 @@ +# SPDX-License-Identifier: MPL-2.0 +# +# .hypatia-ignore — per-rule scanner exemptions for echo-types. +# +# Format (one entry per line; `#` for comments): +# /: +# The path fragment is substring-matched against each finding's +# repo-relative path. Consumed by the Hypatia scanner +# (lib/hypatia/scanner_suppression.ex). Only content-pattern rule +# modules (e.g. code_safety) are routed through this suppression path; +# structural rules (workflow_audit / honest_completion / scorecard) are +# not, and must be addressed by a real fix or an upstream rule change. +# +# Each entry below is a verified FALSE POSITIVE. Real findings are not +# silenced here. + +# ── code_safety/agda_postulate on Smoke.agda — FALSE POSITIVE ────────────── +# The rule is a naive `\bpostulate\b` regex over raw file content that does +# NOT strip comments. The only "postulate" tokens in Smoke.agda are in +# COMMENTS documenting the suite's postulate-free discipline ("Zero +# postulates", "never a postulate", "no funext"); there is no `postulate` +# declaration. The repo's own guardrail tools/check-guardrails.sh strips +# comments before checking and passes — it is the real gate (a genuine +# postulate in Smoke.agda would fail it). The single real postulate in +# proofs/agda (EchoImageFactorizationPropPostulated.agda) is isolated, +# guardrail-exempt by design, and not imported by All.agda or Smoke.agda. +# Upstream fix: agda_postulate should strip comments (see PR notes). +code_safety/agda_postulate:proofs/agda/Smoke.agda + +# ── code_safety/js_http_url_in_code on build-banner.mjs — FALSE POSITIVE ─── +# The flagged `http://` is the SVG XML namespace identifier +# `xmlns="http://www.w3.org/2000/svg"` — a constant namespace URI that is +# never dereferenced over the network. It MUST remain http:// (changing it +# to https would be semantically wrong and break SVG handling). Not CWE-319. +code_safety/js_http_url_in_code:tools/banner/build-banner.mjs