Codex security-audit remediation (vlabs-docs)

.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"

.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

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.

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.

docs/operating-model-github-hf-wandb.md

@@ -19,8 +19,10 @@ Public, **synthetic / redacted** demo evidence:
 - **Hugging Face dataset** — <https://huggingface.co/datasets/verifiablelabs/vlabs-clean-gate-evidence>
 - **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"`

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.

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.

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)")

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()