From 6bf5287fdee73fddcc157fe063c45a52740fdc9d Mon Sep 17 00:00:00 2001 From: vlabs-bot Date: Fri, 10 Jul 2026 18:08:20 +0300 Subject: [PATCH] =?UTF-8?q?Codex=20security-audit=20remediation=20batch=20?= =?UTF-8?q?(2026-07-10,=20banked=20=E2=80=94=20pending=20review)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Auto-banked by takeover from Codex (hit usage limit mid-run). Test-first fixes across trust boundaries, isolation, idempotency, supply-chain. NOT yet independently reviewed/verified in CI. See per-repo diff + quality report. --- .github/dependabot.yml | 9 +++++ .github/workflows/docs-check.yml | 8 +++-- PROVENANCE.md | 9 +++-- docs/architecture-overview.md | 5 +-- docs/operating-model-github-hf-wandb.md | 8 +++-- docs/positioning.md | 2 +- docs/security-boundary.md | 9 ++--- scripts/check_docs.py | 38 +++++++++++++++++--- tests/test_check_docs.py | 46 +++++++++++++++++++++++++ 9 files changed, 112 insertions(+), 22 deletions(-) create mode 100644 .github/dependabot.yml create mode 100644 tests/test_check_docs.py diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 0000000..8b002ed --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,9 @@ +version: 2 +updates: + - package-ecosystem: "github-actions" + directory: "/" + schedule: + interval: "weekly" + open-pull-requests-limit: 5 + commit-message: + prefix: "ci" diff --git a/.github/workflows/docs-check.yml b/.github/workflows/docs-check.yml index aeb3a09..95f79a6 100644 --- a/.github/workflows/docs-check.yml +++ b/.github/workflows/docs-check.yml @@ -2,11 +2,15 @@ name: docs-check on: push: { branches: [main] } pull_request: { branches: [main] } +permissions: + contents: read jobs: check: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4 - - uses: actions/setup-python@v5 + - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + with: { persist-credentials: false } + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5.6.0 with: { python-version: "3.12" } + - run: python -m unittest discover -s tests -v - run: python scripts/check_docs.py diff --git a/PROVENANCE.md b/PROVENANCE.md index 5f25725..22b8dd2 100644 --- a/PROVENANCE.md +++ b/PROVENANCE.md @@ -1,8 +1,7 @@ # Provenance -Clean import (no history rewrite) from `verifiablelabs/verifiable-labs-envs` -at commit `a0f30dc547a73aaae8608d193f94035192404627` (main). Docs authored fresh from approved positioning; no private implementation details. +Clean import (no history rewrite) from the archived legacy workspace at commit +`a0f30dc547a73aaae8608d193f94035192404627`. Docs were authored fresh from +approved positioning; no private implementation details were imported. -The source monorepo remains canonical until the split flips; this mirror is -refreshed by the migration tooling documented in -`verifiable-labs-private/docs/ops/github-repo-split-migration.md`. +`vlabs-docs` is now canonical for the public documentation in this repository. diff --git a/docs/architecture-overview.md b/docs/architecture-overview.md index ea282db..289dbb5 100644 --- a/docs/architecture-overview.md +++ b/docs/architecture-overview.md @@ -20,5 +20,6 @@ Scenario generation, the firewall, anti-hack detection details, and the platform are private — that separation keeps the feedback clean. Selected mathematical properties behind the contamination-resistant -promotion gate are machine-verified in Lean 4. The implementation is -property-tested against the formal specification. +promotion gate are machine-verified in Lean 4. A hand-maintained Python mirror +has property tests derived from selected definitions; no mechanized +code-to-proof parity is claimed. diff --git a/docs/operating-model-github-hf-wandb.md b/docs/operating-model-github-hf-wandb.md index 1fa70ca..8d276ef 100644 --- a/docs/operating-model-github-hf-wandb.md +++ b/docs/operating-model-github-hf-wandb.md @@ -19,8 +19,10 @@ Public, **synthetic / redacted** demo evidence: - **Hugging Face dataset** — - **Weights & Biases** (entity `verifiable-labs`): [clean-generalization-gate](https://wandb.ai/verifiable-labs/clean-generalization-gate) · [contamination-firewall](https://wandb.ai/verifiable-labs/contamination-firewall) · [anti-hack-engine](https://wandb.ai/verifiable-labs/anti-hack-engine) · [scenario-compiler](https://wandb.ai/verifiable-labs/scenario-compiler) · [runpod-costs](https://wandb.ai/verifiable-labs/runpod-costs) -All published evidence is **synthetic / redacted** and is **not a training -dataset**. It contains **no** customer data, hidden evaluations, gold -answers, raw traces, private anti-hack traps, or private engine internals. +The HF/W&B demo artifacts are **synthetic / redacted** and are not a training +dataset. Separately, `vlabs-evidence/results/` contains clearly labelled real +measurements on public benchmark datasets. Neither surface contains customer +data, hidden evaluations, gold answers, raw traces, private anti-hack traps, or +private engine internals. Install the SDK: `pip install "vlabs-sdk==0.0.2"` diff --git a/docs/positioning.md b/docs/positioning.md index f80ec0e..d622b42 100644 --- a/docs/positioning.md +++ b/docs/positioning.md @@ -24,4 +24,4 @@ guarantee general intelligence. We do not claim to have a "formally verified sys We never claim to prove that a model generalizes, and we never claim to eliminate contamination. The only formal claim we make is: -> Selected mathematical properties behind the contamination-resistant promotion gate are machine-verified in Lean 4. The implementation is property-tested against the formal specification. +> Selected mathematical properties behind the contamination-resistant promotion gate are machine-verified in Lean 4. A hand-maintained Python mirror has property tests derived from selected definitions; no mechanized code-to-proof parity is claimed. diff --git a/docs/security-boundary.md b/docs/security-boundary.md index 82378eb..d799cb9 100644 --- a/docs/security-boundary.md +++ b/docs/security-boundary.md @@ -4,9 +4,10 @@ Clean feedback only stays clean if evaluation content cannot leak into training data or public corpora. The boundary is enforced as policy and code, not convention: -**Public** (Apache-2.0, on GitHub): the SDK contracts, environments, the -Lean 4 formal track and its property-tested Python mirror, the -`clean-gate` CLI, examples with synthetic data, redacted evidence. +**Public** (Apache-2.0, on GitHub): the SDK contracts, Lean 4 formal track and +its property-tested Python mirror, the `clean-gate` CLI, examples with +synthetic data, synthetic/redacted demo evidence, and labelled results from +public benchmark datasets. **Private, never published**: hidden evaluation content and gold answers, anti-hack detection details and traps, private verifier logic, the @@ -17,4 +18,4 @@ policy check (classification-aware) before anything leaves the boundary; remote actions require explicit per-service approval flags; uploads are scanned and redacted; audit events record every gate decision and export. -Selected mathematical properties behind the contamination-resistant promotion gate are machine-verified in Lean 4. The implementation is property-tested against the formal specification. +Selected mathematical properties behind the contamination-resistant promotion gate are machine-verified in Lean 4. A hand-maintained Python mirror has property tests derived from selected definitions; no mechanized code-to-proof parity is claimed. diff --git a/scripts/check_docs.py b/scripts/check_docs.py index 65a5798..0e64734 100644 --- a/scripts/check_docs.py +++ b/scripts/check_docs.py @@ -2,11 +2,19 @@ from __future__ import annotations import re -import sys from pathlib import Path +from urllib.parse import unquote ROOT = Path(__file__).resolve().parents[1] -SECRET = re.compile(r"sk-or-v1-[A-Za-z0-9]|AKIA[0-9A-Z]{16}|xox[baprs]-") +SECRET = re.compile( + r"sk-or-v1-[A-Za-z0-9_-]{16,}" + r"|sk-(?:proj-)?[A-Za-z0-9_-]{20,}" + r"|(?:AKIA|ASIA)[0-9A-Z]{16}" + r"|xox[baprs]-[A-Za-z0-9-]{10,}" + r"|gh[pousr]_[A-Za-z0-9]{36,}" + r"|AIza[0-9A-Za-z_-]{35}" + r"|-----BEGIN (?:RSA |EC |OPENSSH )?PRIVATE KEY-----" +) FORBIDDEN = re.compile( r"formally verified (system|product|api|code|service)" r"|prove[sd]? that the model generalizes" @@ -15,16 +23,36 @@ re.IGNORECASE, ) NEGATION = re.compile(r"do not|never|claims? we do not|not a claim", re.IGNORECASE) +MARKDOWN_LINK = re.compile(r"\[[^\]]*\]\(([^)\s]+)(?:\s+[^)]*)?\)") -def main() -> int: +def validate_docs(root: Path = ROOT) -> list[str]: + """Return claim, secret, and broken-local-link errors under ``root``.""" bad: list[str] = [] - for p in sorted(ROOT.rglob("*.md")): - for i, line in enumerate(p.read_text(encoding="utf-8").splitlines(), 1): + root = root.resolve() + for p in sorted(root.rglob("*.md")): + text = p.read_text(encoding="utf-8") + for i, line in enumerate(text.splitlines(), 1): if SECRET.search(line): bad.append(f"{p}:{i}: secret-shaped string") if FORBIDDEN.search(line) and not NEGATION.search(line): bad.append(f"{p}:{i}: forbidden claim: {line.strip()[:80]}") + for match in MARKDOWN_LINK.finditer(line): + target = match.group(1).strip("<>") + if ( + not target + or target.startswith(("#", "/")) + or re.match(r"^[a-z][a-z0-9+.-]*:", target, re.IGNORECASE) + ): + continue + relative = unquote(target.split("#", 1)[0].split("?", 1)[0]) + if relative and not (p.parent / relative).resolve().exists(): + bad.append(f"{p}:{i}: broken local link: {target}") + return bad + + +def main() -> int: + bad = validate_docs() for b in bad: print("FAIL:", b) print("OK: docs clean" if not bad else f"{len(bad)} violation(s)") diff --git a/tests/test_check_docs.py b/tests/test_check_docs.py new file mode 100644 index 0000000..182c7f4 --- /dev/null +++ b/tests/test_check_docs.py @@ -0,0 +1,46 @@ +from __future__ import annotations + +import importlib.util +import tempfile +import unittest +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[1] +SPEC = importlib.util.spec_from_file_location("check_docs", ROOT / "scripts" / "check_docs.py") +assert SPEC and SPEC.loader +checker = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(checker) + + +class DocsCheckTests(unittest.TestCase): + def test_broken_relative_markdown_link_is_rejected(self) -> None: + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + (root / "README.md").write_text("[missing](docs/missing.md)\n", encoding="utf-8") + errors = checker.validate_docs(root) + self.assertTrue(any("broken local link" in error for error in errors), errors) + + def test_fragment_and_external_links_are_not_treated_as_files(self) -> None: + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + (root / "README.md").write_text( + "[section](#section) [site](https://example.com) [mail](mailto:test@example.com)\n", + encoding="utf-8", + ) + self.assertEqual(checker.validate_docs(root), []) + + def test_common_secret_shapes_are_rejected(self) -> None: + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + token = "gh" + "p_" + "A" * 36 + (root / "README.md").write_text(f"credential={token}\n", encoding="utf-8") + errors = checker.validate_docs(root) + self.assertTrue(any("secret-shaped" in error for error in errors), errors) + + def test_repository_docs_validate(self) -> None: + self.assertEqual(checker.validate_docs(ROOT), []) + + +if __name__ == "__main__": + unittest.main()