|
| 1 | +# Runnable Assurance — Sentinel v2.4 Governance Artifacts |
| 2 | + |
| 3 | +This directory upgrades the Sentinel v2.4 governance artifacts from *declarative* |
| 4 | +(schemas, prose controls, policy sketches) to **executable and verifiable**. Where |
| 5 | +the master reference documents assert that a control "holds," the artifacts here |
| 6 | +*prove* it with industry-standard tooling. |
| 7 | + |
| 8 | +> Scope note. These artifacts implement the standards-grounded core (OSCAL 1.1.2, |
| 9 | +> OPA/Rego, TLA+/TLC, Circom/Groth16, FIPS 203/204/205 references). AGI/ASI |
| 10 | +> *containment* is modelled as a control-and-invariant discipline; speculative |
| 11 | +> regime fixtures (ICGC/GACP, GAIRA) remain tagged `feasibility-tier` C/D in the |
| 12 | +> OSCAL catalog and are not claimed as settled practice. |
| 13 | +
|
| 14 | +## One command |
| 15 | + |
| 16 | +```bash |
| 17 | +bash governance_artifacts/run_runnable_assurance.sh |
| 18 | +``` |
| 19 | + |
| 20 | +Runs all five checks below and fails fast on any error. |
| 21 | + |
| 22 | +## What is proven, and against which control |
| 23 | + |
| 24 | +| # | Check | Tool | Backs OSCAL control | Regime anchor | |
| 25 | +|---|-------|------|---------------------|---------------| |
| 26 | +| 1 | Release gate + credit gate + confidential-computing attestation gate (PCR_MATCH) | `opa test` (21 tests) | release-gate, `con-07`, `env-01` | SR 11-7, EU AI Act Art. 14/15, ECOA, GDPR Art. 22, DORA | |
| 27 | +| 2 | Containment one-way ratchet & terminal-actuation quorum | TLA+ `tlc2.TLC` | `con-04`, `con-07` | EU AI Act Art. 14, DORA resilience testing | |
| 28 | +| 3 | Attested admission — no T0 workload runs without fresh valid attestation; TCB rollback / PCR drift force eviction | TLA+ `tlc2.TLC` | `env-01` | EU AI Act Art. 15, DORA ICT risk, NIST AI RMF | |
| 29 | +| 4 | GC-IR cross-target conformance (policy ⇔ circuit ⇔ expectation) | `opa eval` + Circom witness | obligation `ob-ecoa-adverse-reason-codes` | ECOA, GDPR Art. 22, EU AI Act Art. 13 | |
| 30 | +| 5 | Systemic-risk concentration bound (HHI) zk proof | Circom + Groth16 (snarkjs) | `cry-05` | Basel op-risk, systemic telemetry | |
| 31 | +| 6 | SARA/ACR MoE routing stabilization invariants (entropy / load balance / drop) | Python simulator + pytest | `rte-01` | EU AI Act Art. 15 robustness, SR 11-7 | |
| 32 | +| 7 | PQC WORM audit log — real CRYSTALS-Dilithium (ML-DSA-65) signatures + tamper-evident hash chain + S3 Object Lock retention | Python (`dilithium-py`) + pytest | `cry-02` | DORA, EU AI Act Art. 12 logging | |
| 33 | +| 8 | Governance artifact schema validation | Python validator | manifest/schema integrity | OSCAL, evidence logging (EU AI Act Art. 12) | |
| 34 | + |
| 35 | +### New control groups (`oscal/catalog_sentinel_v24_env_rte.json`) |
| 36 | + |
| 37 | +- **ENV — Confidential Computing & Attested Execution**: `env-01` (hardware-attested |
| 38 | + admission for T0/T1 via SEV-SNP / TDX + vTPM PCR_MATCH; runtime TCB-rollback and |
| 39 | + PCR-drift eviction), `env-02` (enclave-bound ML-DSA key custody). |
| 40 | +- **RTE — MoE Routing Stability**: `rte-01` (SARA/ACR stabilization invariants). |
| 41 | + |
| 42 | +## 1. OPA policy tests — `rego/` |
| 43 | + |
| 44 | +- `release_gate.rego` — high-impact release is **deny-by-default**; `allow` requires |
| 45 | + containment `ENFORCED`, dual-control quorum ≥ 2, signed bundle, and both the |
| 46 | + Omni-Sentinel safety control and the SR 11-7 validation control. |
| 47 | +- `high_impact_credit.rego` — adverse credit underwriting requires human review, |
| 48 | + ≥ 3 reason codes, fairness within an equal-opportunity delta, verified lineage, |
| 49 | + no active incident. |
| 50 | +- `fairness_credit_decision.rego` — the Rego emission target of the GC-IR obligation. |
| 51 | + |
| 52 | +```bash |
| 53 | +opa test governance_artifacts/rego/ -v # 12/12 PASS |
| 54 | +``` |
| 55 | + |
| 56 | +## 2. TLA+ containment ratchet — `tla/KillSwitchAbstract.tla` |
| 57 | + |
| 58 | +Models containment levels L0 NORMAL → L4 TERMINATED. Autonomous Supervisory Agents |
| 59 | +(ASAs) may only *raise* level within L0–L2; lowering the level or actuating the |
| 60 | +terminal levels L3/L4 requires a human dual-control quorum. TLC exhaustively checks: |
| 61 | + |
| 62 | +- `TypeOK`, `ASARatchet`, `TerminalNeedsQuorum` (invariants) |
| 63 | +- `ASANeverLowers`, `DeEscalationNeedsQuorum` (action properties) |
| 64 | + |
| 65 | +```bash |
| 66 | +cd governance_artifacts/tla |
| 67 | +java -cp tools/tla2tools.jar tlc2.TLC -config KillSwitchAbstract.cfg KillSwitchAbstract.tla |
| 68 | +# -> "Model checking completed. No error has been found." (13 distinct states) |
| 69 | +``` |
| 70 | + |
| 71 | +## 3. GC-IR cross-target harness — `zk/gcir_harness.py` |
| 72 | + |
| 73 | +The GC-IR design claims a single obligation compiles to multiple targets and that |
| 74 | +"any disagreement fails the build." This harness makes that real for |
| 75 | +`ob-ecoa-adverse-reason-codes`: it runs each shared fixture through the **Rego** |
| 76 | +rule (`opa eval`) and through the **Circom** circuit (real witness generation), then |
| 77 | +asserts `rego_allow == circuit_witness_producible == declared_expectation`. |
| 78 | + |
| 79 | +```bash |
| 80 | +cd governance_artifacts/zk && python3 gcir_harness.py |
| 81 | +# fx-001 allow / fx-002 deny (too few codes) / fx-003 deny (unapproved code) — all agree |
| 82 | +``` |
| 83 | + |
| 84 | +## 4. SRC-1 systemic-risk concentration proof — `zk/` |
| 85 | + |
| 86 | +`circuits/src1_concentration_bound.circom` proves, in zero knowledge, that the |
| 87 | +decision-volume **Herfindahl-Hirschman Index** across foundation-model providers |
| 88 | +does not exceed a board-ratified threshold (basis points), with `circuit_tag` |
| 89 | +binding the proof to circuit revision SRC-1. The flow runs a dev Powers-of-Tau |
| 90 | +ceremony, Groth16 setup, proves the compliant fixture, verifies it, and emits a |
| 91 | +`proof_statement.json` conforming to `proof_statement_schema.json`. The negative |
| 92 | +test shows an over-concentrated portfolio **cannot** produce a witness. |
| 93 | + |
| 94 | +```bash |
| 95 | +cd governance_artifacts/zk && bash run_src1_proof.sh |
| 96 | +# -> snarkJS: OK! (proof verifies); violation fixture rejected (soundness) |
| 97 | +``` |
| 98 | + |
| 99 | +> The Powers-of-Tau ceremony here is a **development** ceremony and is **not** |
| 100 | +> production-secure. A production deployment requires a multi-party trusted setup |
| 101 | +> (or a transparent system such as PLONK/STARK as noted in the schema enum). |
| 102 | +
|
| 103 | +## 6. Confidential-computing attestation gate — `rego/attestation_gate.rego` + `tla/AdmissionWithAttestation.tla` |
| 104 | + |
| 105 | +The `PCR_MATCH=TRUE` assertion that recurs throughout the master docs is now |
| 106 | +*enforced*, not merely stated. The Rego gate (`sentinel.attestation`) admits a |
| 107 | +T0/T1 workload only when it presents a SEV-SNP or TDX report with a verified |
| 108 | +signature, fresh anti-replay nonce, a launch measurement in the golden registry, |
| 109 | +platform TCB at/above the ratified minimum (no rollback), and a vTPM PCR quote |
| 110 | +matching the policy digest. The TLA+ spec proves the *temporal* guarantee: across |
| 111 | +all 64 initial evidence combinations, no workload reaches `RUNNING` without a |
| 112 | +valid attestation, and runtime TCB rollback or PCR drift forces `EVICTED`. |
| 113 | + |
| 114 | +```bash |
| 115 | +opa test governance_artifacts/rego/ # includes 9 attestation tests |
| 116 | +cd governance_artifacts/tla |
| 117 | +java -cp tools/tla2tools.jar tlc2.TLC -config AdmissionWithAttestation.cfg AdmissionWithAttestation.tla |
| 118 | +``` |
| 119 | + |
| 120 | +## 7. SARA/ACR MoE routing stabilization — `routing/sara_acr_router.py` |
| 121 | + |
| 122 | +Defines and demonstrates two stack-specific mechanisms (not external standards): |
| 123 | +**SARA** (Stabilized Adaptive Routing — load-aware gating bias + temperature) and |
| 124 | +**ACR** (Adaptive Capacity Regulation — per-expert capacity factor with overflow |
| 125 | +handling). The simulator shows that under skewed gating a naive top-k router |
| 126 | +collapses (normalised entropy ≈ 0.38, load ratio ≈ 5.6) and *violates* the |
| 127 | +`rte-01` invariants, while SARA+ACR holds entropy ≈ 0.99 and load ratio ≈ 1.25, |
| 128 | +*satisfying* all invariants (entropy ≥ 0.80, load ratio ≤ 1.60, drop ≤ 0.02). |
| 129 | + |
| 130 | +```bash |
| 131 | +python3 governance_artifacts/routing/sara_acr_router.py |
| 132 | +pytest governance_artifacts/routing/test_sara_acr_router.py -q # 4 tests |
| 133 | +``` |
| 134 | + |
| 135 | +## 8. PQC WORM audit log — `kafka/pqc_worm_logger_v2.py` |
| 136 | + |
| 137 | +Replaces the original HMAC placeholder with **real CRYSTALS-Dilithium (ML-DSA-65, |
| 138 | +FIPS 204)** signatures over canonical batch payloads, linked in a tamper-evident |
| 139 | +**hash chain** (`prev_batch_hash`), with an S3 Object Lock COMPLIANCE-mode |
| 140 | +retention record per batch. `verify_chain()` re-validates every signature and link |
| 141 | +and returns a supervisory-ready report; the demo proves that entry mutation, |
| 142 | +batch reordering, and signature forgery are all detected. |
| 143 | + |
| 144 | +```bash |
| 145 | +python3 governance_artifacts/kafka/pqc_worm_logger_v2.py |
| 146 | +pytest governance_artifacts/kafka/test_pqc_worm_logger_v2.py -q # 6 tests |
| 147 | +``` |
| 148 | + |
| 149 | +> ML-DSA-65 here is provided by the pure-Python `dilithium-py` reference |
| 150 | +> implementation — correct and FIPS-204-aligned, but **not** constant-time or |
| 151 | +> side-channel-hardened. Production signing belongs in the env-02 enclave using a |
| 152 | +> validated cryptographic module. |
| 153 | +
|
| 154 | +## Reproducing from a clean checkout |
| 155 | + |
| 156 | +```bash |
| 157 | +# OPA |
| 158 | +curl -sSL -o /usr/local/bin/opa https://openpolicyagent.org/downloads/v0.70.0/opa_linux_amd64_static && chmod +x /usr/local/bin/opa |
| 159 | +# circom 2.1.9 + snarkjs/circomlib |
| 160 | +curl -L -o ~/.local/bin/circom https://github.com/iden3/circom/releases/download/v2.1.9/circom-linux-amd64 && chmod +x ~/.local/bin/circom |
| 161 | +( cd governance_artifacts/zk && npm install ) |
| 162 | +# TLA+ tools |
| 163 | +curl -L -o governance_artifacts/tla/tools/tla2tools.jar https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar |
| 164 | +# Python |
| 165 | +pip install pyyaml jsonschema dilithium-py |
| 166 | +# Run everything |
| 167 | +bash governance_artifacts/run_runnable_assurance.sh |
| 168 | +``` |
| 169 | + |
| 170 | +> Sandbox note: compile circuits with `--O0` if circom raises a `SystemTimeError` |
| 171 | +> during constraint simplification (a known clock-skew issue in some containers). |
0 commit comments