Generated by 16-engineer adversarial audit (2026-05-29). Updated 2026-05-30. Primary sources: live attack demonstrations, source code inspection, runtime measurement.
- [RESOLVED] — fix committed; new tests prove the closure
- [MITIGATED] — partial fix; documented residual risk
- [OPEN] — known gap; not yet addressed
- [DEPLOY] — deployment-time concern; cannot be fixed in kernel code
- File:
src/authgate/kernel/entities.py,src/authgate/kernel/registry.py - Fix commit:
tests/test_c1_identity_binding.py(10 new tests) - What changed:
Entitynow has an optionalidentity_tokenfield- Registry's
_claim_keyis now(name, kind, resource)— HUMAN(x) and MACHINE(x) don't collide - Registry tracks
_identity_tokensper (name, kind); impersonation rejected claims_for()returns empty list if presented Entity has wrong/missing tokenowner_of()returns None for impersonators
- Residual risk (DEPLOY): if no token is set, behavior is unchanged. Deployments
must explicitly opt in by setting
identity_tokenon every Entity. - Full closure: Use the Rust TCB (
subject_id = SHA-256(pubkey), compile-time).
- File:
src/authgate/kernel/call_gate.py - Proof: Permitted tool called
subprocess.run()and exfiltrated data. - Cannot be fixed in Python alone — OS-level enforcement required.
- Mitigations in place:
SeccompExecutor(src/authgate/kernel/seccomp_executor.py) for Linux- WASM sandbox (
freedom-kernel/src/sandbox.rs) — Linux CI workflow live
- For full closure: deploy on Linux with seccomp OR use Rust WASM sandbox.
- Commit:
feat: infrastructure hardening(2026-05-29) - What changed:
Action.min_epochfield,RightsClaim.epochfield,Registry.advance_epoch(),can_act()enforces epoch gate - Tests:
tests/test_epoch_revocation.py(11 tests)
- File:
src/authgate/kernel/verifier.py,formal/INCOMPLETENESS.md - Fix: added impurity note to
verify()docstring;formal/INCOMPLETENESS.mdnow has explicit "Formal scope: Rust TCB only" section - Reason: Lean4
verify_deterministictheorem coversengine.rs(pure). Pythonverify()writes to_audit_logand_tracer— formally it's a different function. - For pure-function guarantees: use Rust backend (
authgate.health_check()reports backend).
- File:
src/authgate/kernel/verifier.py:97 - Fix:
FreedomVerifier(audit_log=None)now logs a_log.warning(...)explaining that decisions will be unlogged. Deployments using examples without audit_log will see the warning at startup.
- Commit:
feat: infrastructure hardening - What changed:
AuditLog(max_entries=N)parameter; rotation preserves chain integrity via the retained window.AuditLog.total_counttracks decisions including those rotated out. - Tests:
tests/test_army.py::TestSystems23_AuditMaxEntries,TestSRE89_AuditRotationChainIntegrity
- File:
README.md - Fix: README now says
engine.rs: 250 LOC. Full security-critical Rust path (engine.rs + dag.rs + call_gate.rs): ~934 LOC.
- File:
src/authgate/authority/human_delegation.py - Fix:
MarketOracleSource.request_capability()andReputationGateSource.request_capability()now raiseNotImplementedErrorwith explanation. Tests updated.
- Fix: Created
spec/canonical_action.schema.json,spec/gate_result.schema.json,spec/audit_entry.schema.json. Wire validator available atauthgate.wire_validator.validate(). CLI:authgate-cli validate --schema NAME FILE - Tests:
tests/test_wire_validator.py(16 tests)
- Host function boundary is part of TCB attack surface.
- Needs same Kani-style harnesses as
engine.rs. - Tracked for adversarial-lab branch.
- File:
freedom-kernel/src/tcb/sequence.rs - Fix: 5 Kani harnesses added inside
#[cfg(kani)]block:prop_seq_accumulated_monotone— high-water mark propertyprop_seq_exceeds_limit_consistent— bitmask semanticsprop_seq_step_count_matches_records— bounded counting (unwind=5)prop_seq_empty_never_exceeds— vacuous truthprop_seq_idempotent_rights— idempotent under OR with self
- Run:
cargo kani --harness prop_seq_accumulated_monotone
- File:
freedom-kernel/src/tcb/engine.rs - Fix: 5 new tests covering: all-ones nonce, alternating nonce, binding-hash divergence between nonces, post-seal nonce tamper detection, replay with different nonces.
- Symptom:
advance_epoch()on original registry polluted "immutable" snapshots - Fix:
freeze()now doescopy.copy(c)per claim; tokens dict also copied - Found by: T32, T35 (Distributed systems testers)
- Symptom: After max_entries rotation, retained window's prev_hash didn't match GENESIS
- Fix: chain verifier now validates linkage within the retained window (entries pre-rotation were validated at write time)
- Found by: T89 (SRE)
- Fix: explicit
< 0check afterint()conversion - Found by: T47 (Cryptographer)
- Fix: schema files written to correct path
- Found by: T90 (SRE)
- Fix: dedicated read-only bot in affected tests
- Found by: T02, T03 (Security)
| Finding | Status | Plan |
|---|---|---|
| C-2: Subprocess escape | DEPLOY | Linux + seccomp/WASM (already coded, CI workflow exists) |
| M-3: WASM host functions unaudited | OPEN | Kani harnesses for sandbox.rs (tcb-core branch) |
| External adversarial review | OPEN | Year 1 milestone — humans only |
- 1155 tests passing
- 7 of 8 CRITICAL/SEVERE/MEDIUM findings RESOLVED or MITIGATED
- 5 of 5 LOW/BUG findings RESOLVED
- 2 OPEN items (1 deployment-only, 1 engineering)
Updated: 2026-05-30. Re-audit after external review or any TCB change.