| # ROWM Threat Model & Security Analysis | |
| **Version:** 1.0.0 | |
| **Status:** Complete (verified 2026-07-27) | |
| **Authors:** Ahmad Ali Parr, Jessica SNAPKITTYWEST | |
| --- | |
| ## 1. Trust Boundaries | |
| ### Trusted Components (Assumed Secure) | |
| 1. **Prolog/Datalog engine** — Logic evaluation, rule grounding | |
| 2. **Rust runtime** — Memory safety, WORM enforcement | |
| 3. **Cryptographic libraries** — Blake3, Ed25519 (from established crates) | |
| 4. **Kernel/OS** — Process isolation, filesystem, system clock | |
| ### Untrusted Components (Validated Before Use) | |
| 1. **External source code** — All user-provided code in any language | |
| 2. **Notebook metadata** — Cell definitions, execution counts, outputs | |
| 3. **Network input** — Remote code, serialized instructions, proofs | |
| 4. **User-provided proofs** — Terms claimed to be proofs (external tools verify) | |
| 5. **Previously sealed artifacts** — Must re-verify linkage | |
| --- | |
| ## 2. In-Scope Threats | |
| ### Threat T1: Unauthorized Code Execution | |
| **Attack Vector:** Agent without permission executes code on protected runtime | |
| **Mitigation:** | |
| - All dispatch routes through `dispatch_gated/5` (sealed entry point) | |
| - Prolog checks: agent_active, trust_level ≠ tier_2, capability_issued, capability_active, not_revoked, not_expired, permission_granted, runtime_active | |
| - No bypass: code cannot query `capability_active/2` or `dispatch_permitted/5` directly | |
| **Residual Risk:** LOW | |
| - Requires compromise of Prolog engine or Rust runtime boundary | |
| - Requires forging Ed25519 signature OR recovering private key | |
| **Test Case:** `test_unauthorized_agent_dispatch` in test_queries.pl | |
| --- | |
| ### Threat T2: Capability Bypass via Expiration Boundary | |
| **Attack Vector:** Agent with expired capability uses it by manipulating time | |
| **Mitigation:** | |
| - Expiration boundary is EXCLUSIVE: `Timestamp < ExpiresAt` (not ≤) | |
| - Capability ExpiresAt=T is inactive at time T | |
| - get_time/1 uses system clock (not user-settable in normal mode) | |
| - Timestamp checked in hardened `dispatch_gated/5` | |
| **Residual Risk:** MEDIUM | |
| - If system clock can be manipulated (e.g., via NTP attack), boundary is bypassed | |
| - If Prolog engine can be forced to use stale time value, boundary is bypassed | |
| **Mitigation Upgrade:** Pin to monotonic clock; disallow backward clock adjustments | |
| **Test Case:** `test_expired_capability_rejection` in test_queries.pl (uses fixed time) | |
| --- | |
| ### Threat T3: Capability Revocation Evasion | |
| **Attack Vector:** Agent retains reference to revoked capability; uses it before revocation is detected | |
| **Mitigation:** | |
| - Revocation recorded as fact: `capability_revoked(CapID, Reason)` | |
| - Every dispatch checks: `\+ capability_revoked(CapID, _)` (negation-as-failure) | |
| - Revocation is WORM-sealed (immutable once written) | |
| - No capability can be "un-revoked" (monotonic) | |
| **Residual Risk:** LOW | |
| - Requires Prolog engine compromise (to retract revocation fact) | |
| - Requires racing between revocation and dispatch in nanosecond window | |
| **Test Case:** `test_revoked_capability_immediate_rejection` in test_queries.pl | |
| --- | |
| ### Threat T4: Proof Obligation Circumvention | |
| **Attack Vector:** Agent forces transition to RELEASED without discharging all 4 proof obligations | |
| **Mitigation:** | |
| - Release gate 1: `all_proofs_satisfied(true)` queries proof_satisfied/2 for all 4 obligations | |
| - Each proof obligation checked before release transition: | |
| 1. InvariantPreservation — loop invariants maintained | |
| 2. SemanticPreservation — source ≡ compiled semantics | |
| 3. LoopInvariantMaintenance — bounds and termination | |
| 4. ReceiptChainIntegrity — monotonic sequence + hash linkage | |
| - Failed proof blocks transition (state stays RECEIPTED) | |
| **Residual Risk:** LOW | |
| - Requires compromise of proof validator or Prolog engine | |
| - Requires forging proof artifact from external verifier | |
| **Test Case:** `test_release_blocked_on_failed_proof` in test_queries.pl | |
| --- | |
| ### Threat T5: Receipt Chain Tampering | |
| **Attack Vector:** Attacker modifies a receipt or inserts a receipt out of sequence | |
| **Mitigation:** | |
| - Receipt is signed with Ed25519 (once issued, immutable) | |
| - Signature covers canonical receipt bytes + previous_receipt_hash | |
| - Chain integrity verified via `receipt_chain_valid/1` predicate | |
| - Monotonic sequencing enforced: `Receipt_N.sequence < Receipt_N+1.sequence` | |
| - Out-of-order insertion detected by hash linkage mismatch | |
| **Residual Risk:** MEDIUM | |
| - If Ed25519 private key is compromised, receipts can be forged | |
| - If Prolog engine allows fact retraction, receipts can be deleted | |
| - Timestamp manipulation can reorder receipts within same second | |
| **Mitigation Upgrade:** | |
| - Use hardware-backed Ed25519 keys (TPM/HSM) | |
| - Append receipts to tamper-evident external ledger (blockchain or WORM storage) | |
| - Use nanosecond timestamps or logical clocks | |
| **Test Case:** `test_receipt_tampering_detected` in test_queries.pl | |
| --- | |
| ### Threat T6: Invariant Violation & Rollback Abuse | |
| **Attack Vector:** Attacker deliberately violates invariant to trigger rollback, causing state loss or inconsistency | |
| **Mitigation:** | |
| - Invariant violation triggers rollback to LAST VALID CHECKPOINT | |
| - Rollback is WORM-sealed (cannot undo a rollback) | |
| - Violation is recorded in receipt chain (permanent audit trail) | |
| - Repeated violations increment agent's violation counter (eventually triggers revocation) | |
| **Residual Risk:** LOW | |
| - Attacker can cause localized rollback but cannot escape global audit | |
| - Proof obligations will fail on violated execution path | |
| **Test Case:** `test_invariant_violation_triggers_rollback` in test_queries.pl | |
| --- | |
| ### Threat T7: Self-Modifying Code Escape | |
| **Attack Vector:** Cell code rewrites bytecode to bypass invariant checks or authorization | |
| **Mitigation:** | |
| - Code invariant is extracted and proved: `∀t ∈ [code_start, code_end]: M[t] == original[t]` | |
| - If code violates this invariant, symbolic execution detects the rewrite | |
| - Rewritten code is NOT re-compiled (would fail signature verification) | |
| - Self-modification is only allowed via M4 feedback (between cells), not within execution | |
| **Residual Risk:** LOW | |
| - Requires compromise of invariant extractor or symbolic execution engine | |
| - Requires proof obligation bypass (T4) | |
| **Test Case:** `test_code_self_modification_detected` in test_queries.pl | |
| --- | |
| ### Threat T8: Cross-Cell State Leakage via M4 | |
| **Attack Vector:** Cell N writes secret to M4 definitions; Cell N+1 accesses secret | |
| **Mitigation:** | |
| - M4 definitions are sandboxed: max_expansion_depth=100, max_output_size=1MB | |
| - Definitions are scoped to individual notebook execution (not global) | |
| - Outputs are passed through Prolog facts (auditable, signed) | |
| - Proof obligation checks semantic equivalence (no covert channels) | |
| **Residual Risk:** MEDIUM | |
| - M4 macro expansion is Turing-complete (can compute anything) | |
| - If M4 sandbox limits are exceeded, behavior is undefined | |
| **Mitigation Upgrade:** | |
| - Disable M4 macro expansion for untrusted agents | |
| - Use restricted M4 builtins (no system calls) | |
| - Require proof of M4 output equivalence | |
| **Test Case:** `test_m4_cross_cell_access_denied` (when sandboxed) | |
| --- | |
| ## 3. Out-of-Scope Threats | |
| ### Threat OOS-1: Physical Attacks | |
| **Scope:** Tamper with machine hardware, steal RAM, modify CPU | |
| **Rationale:** System assumes hardware boundary is protected. Mitigated by: | |
| - Deployment in secure data center | |
| - Hardware security modules (HSM) for key storage | |
| - Physical access controls | |
| --- | |
| ### Threat OOS-2: Compromised Kernel/OS | |
| **Scope:** Kernel patch that violates memory isolation or filesystem integrity | |
| **Rationale:** System assumes kernel is trustworthy. Cannot defend if OS is compromised. | |
| **Mitigation:** | |
| - Use verified kernel (e.g., seL4 with formal proof of isolation) | |
| - Run in VM hypervisor with attestation | |
| - Use signed boot (Secure Boot, measured launch) | |
| --- | |
| ### Threat OOS-3: Supply Chain Attack on Dependencies | |
| **Scope:** Malicious update to blake3, ed25519-dalek, or swipl packages | |
| **Rationale:** System assumes crates.io and package managers are trustworthy. | |
| **Mitigation:** | |
| - Pin dependency versions to verified commits | |
| - Use cargo vendor to isolate dependencies | |
| - Run internal security audit on critical crates | |
| - Use binary reproducibility to verify builds | |
| --- | |
| ### Threat OOS-4: Spectre/Meltdown CPU Attacks | |
| **Scope:** Side-channel attacks via CPU cache/speculation | |
| **Rationale:** Prolog/Rust don't have built-in defenses against CPU microarchitecture attacks. | |
| **Mitigation:** | |
| - Use constant-time implementations for cryptography (already in ed25519-dalek) | |
| - Run on CPUs with microcode patches | |
| - Deploy in VM with IBRS enabled | |
| --- | |
| ## 4. Cryptographic Assumptions | |
| ### Assumption C1: Blake3 Collision Resistance | |
| **Claim:** Two different inputs X, Y never produce same Blake3 hash (within 256-bit space) | |
| **Usage:** Receipt hashing, capability hashing, checkpoint ancestry verification | |
| **Risk:** If collision found, receipt chain integrity compromised | |
| **Mitigation:** | |
| - Use full 256-bit hash (not truncated) | |
| - Verify against Blake3 team's formal analysis | |
| - Monitor cryptanalysis literature for attacks | |
| --- | |
| ### Assumption C2: Ed25519 Signature Unforgeability | |
| **Claim:** Attacker without private key cannot produce valid Ed25519 signature | |
| **Usage:** Receipt signing, release manifest signing, agent identity | |
| **Risk:** If forged, attacker can fake any receipt or impersonate agent | |
| **Mitigation:** | |
| - Protect private keys in HSM or secure enclave | |
| - Rotate keys periodically | |
| - Publish public keys in tamper-evident registry | |
| - Use key pinning for critical agents | |
| **Current Gap:** HMAC-SHA256 used instead of Ed25519 (symmetric, not asymmetric) | |
| → Cannot verify signatures without secret key | |
| → Third-party audit impossible | |
| --- | |
| ### Assumption C3: SHA2 Second Preimage Resistance | |
| **Claim:** Attacker cannot find X' ≠ X such that SHA256(X') = SHA256(X) | |
| **Usage:** Source code hashing, bytecode hashing | |
| **Risk:** If preimage found, two different code paths could have same hash | |
| **Mitigation:** | |
| - Use full 256-bit hash (not truncated) | |
| - Transition to Blake3 where feasible (already using in receipts) | |
| --- | |
| ### Assumption C4: CBOR Deterministic Encoding | |
| **Claim:** Two semantically identical values always encode to identical CBOR bytes | |
| **Usage:** Canonical representation for hashing and signing | |
| **Risk:** If non-deterministic, same payload hashes differently at different times | |
| **Mitigation:** | |
| - Define canonical byte order (little-endian, ascending key order) | |
| - Validate CBOR library implements RFC 7049 deterministic encoding | |
| - Test equivalence: canonical(X) = canonical(canonicalize(X)) | |
| --- | |
| ## 5. Known Vulnerabilities & Limitations | |
| ### Vulnerability V1: Timestamp-Based Nondeterminism | |
| **Issue:** Receipt timestamps make reproducible verification impossible | |
| **Evidence:** Receipt includes `timestamp: 1719432000`, which differs on each execution | |
| **Impact:** Two executions of same code produce different receipt hashes | |
| **Mitigation:** | |
| - Inject canonical time at sealing time (not at execution time) | |
| - Use logical clock or block height (e.g., Git commit count) | |
| - For testing: mock get_time/1 | |
| **Status:** Known, documented, accepted for now | |
| **Upgrade Path:** Canonical time injection via test harness | |
| --- | |
| ### Vulnerability V2: No Cross-System Replay Protection | |
| **Issue:** Receipt from System A can be replayed in System B | |
| **Evidence:** Release.pl gate 11 checks "no_active_dependencies" but doesn't verify context | |
| **Impact:** Attacker can use same receipt in multiple contexts | |
| **Mitigation:** | |
| - Add context-specific binding: receipt includes system_id or deployment_context | |
| - Require capabilities to be per-system (not global) | |
| - Validate receipt is for current deployment | |
| **Status:** Known, documented, acknowledged | |
| **Upgrade Path:** Per-system capability scoping | |
| --- | |
| ### Vulnerability V3: Notebook Mutation After Seal | |
| **Issue:** Jupyter .ipynb file can be edited after cell execution recorded | |
| **Evidence:** Notebook cells are mutable JSON; no signature covers them | |
| **Impact:** Attacker modifies notebook cell after it executed, creating false history | |
| **Mitigation:** | |
| - Don't trust notebook file as source of truth | |
| - Use Prolog facts as authoritative record of cell state | |
| - Optionally: GPG-sign .ipynb file after each execution | |
| - For production: use immutable notebook storage (e.g., IPFS, blockchain) | |
| **Status:** Known, documented, mitigation available | |
| **Upgrade Path:** Signed notebook artifacts | |
| --- | |
| ### Vulnerability V4: HMAC Instead of Ed25519 | |
| **Issue:** Receipts are HMAC-signed (symmetric), not Ed25519-signed (asymmetric) | |
| **Evidence:** Scripts use `hmac_sha256(data, WORM_SECRET)`, not Ed25519 | |
| **Impact:** Cannot verify receipts without secret key; third-party audit impossible; not legally admissible | |
| **Compliance Impact:** | |
| - SOX §302: Officer certification requires independent verification ✗ | |
| - GDPR Article 5(2): Accountability requires third-party audit capability ✗ | |
| - ISO 27001 A.12.4: Event logging integrity requires asymmetric signatures ✗ | |
| **Mitigation:** | |
| - Implement Ed25519 signing for all receipts | |
| - Keep private key in HSM (not in code) | |
| - Publish public key for verification | |
| - Rotate keys annually | |
| **Status:** Known, unresolved | |
| **Upgrade Path:** Ed25519 implementation required before production release | |
| --- | |
| ### Vulnerability V5: Truncated Hashes | |
| **Issue:** Some implementations truncate hashes to 16 bytes (128 bits) instead of full 256 | |
| **Evidence:** `signature.slice(0, 16)` in worm-receipts.js | |
| **Impact:** Collision resistance reduced from ~2^128 to ~2^64; attackers can forge signatures with ~2^64 operations | |
| **Mitigation:** | |
| - Use full 256-bit hashes everywhere | |
| - Audit all hash truncation and remove it | |
| - Enforce minimum hash size in schemas | |
| **Status:** Known, unresolved | |
| **Upgrade Path:** Full-hash enforcement in cryptographic layer | |
| --- | |
| ### Vulnerability V6: Untested Proof Tool Integration | |
| **Issue:** Agda, Ada/SPARK, Lean 4 invocations are stubs; proof artifacts not validated | |
| **Evidence:** No integration tests for external proof tools | |
| **Impact:** Proof claims are unverified; release gates can pass falsely | |
| **Mitigation:** | |
| - Implement end-to-end tests for each proof tool | |
| - Validate proof artifacts (terms, types, signatures) | |
| - Reject unverified proof status | |
| - Require manual proof review for critical proofs | |
| **Status:** Known, documented | |
| **Upgrade Path:** Proof tool integration tests (Phase 8+) | |
| --- | |
| ## 6. Security Recommendations | |
| ### Before Production Release | |
| 1. **Implement Ed25519 signing** (NOT HMAC) for all receipts | |
| 2. **Enforce full-hash usage** (no truncation) | |
| 3. **Test proof tool integrations** end-to-end | |
| 4. **Add per-system context binding** to receipts (replay protection) | |
| 5. **Implement notebook signing** (GPG or Ed25519) | |
| 6. **Migrate to canonical time** (logical clock or Git height) | |
| 7. **Use HSM for private keys** (not filesystem storage) | |
| 8. **Enable SELinux/AppArmor** for process isolation | |
| 9. **Audit Prolog engine** for fact retraction vulnerabilities | |
| 10. **Pin dependency versions** and verify checksums | |
| ### Ongoing Operations | |
| 1. **Rotate Ed25519 keys** annually or on compromise suspicion | |
| 2. **Monitor Blake3/Ed25519 cryptanalysis** literature | |
| 3. **Run regular security audits** (penetration testing) | |
| 4. **Log all authorization failures** (detect attacks) | |
| 5. **Verify receipt chains** weekly (detect tampering) | |
| 6. **Back up WORM ledger** to geographically distributed stores | |
| 7. **Incident response plan** for leaked private keys | |
| --- | |
| ## 7. Compliance Mapping | |
| | Compliance Requirement | Status | Evidence | | |
| |------------------------|--------|----------| | |
| | SOX §302 Independent Verification | ❌ BLOCKED | Need Ed25519 (HMAC blocks verification) | | |
| | GDPR Art. 5(2) Accountability | ❌ BLOCKED | Need audit trail verification | | |
| | HIPAA Audit Controls | ⏳ PARTIAL | Logs present; signing incomplete | | |
| | ISO 27001 A.12.4 Event Logging | ⏳ PARTIAL | Truncated hashes reduce assurance | | |
| | PCI-DSS 10.5 Log Integrity | ❌ BLOCKED | HMAC not accepted; need asymmetric | | |
| | FedRAMP AC-6 Least Privilege | ✅ VERIFIED | dispatch_gated sealed entry point | | |
| **Production Readiness: NOT COMPLIANT** (until Ed25519 implemented and tested) | |
| --- | |
| ## 8. Incident Response | |
| ### Suspected Private Key Compromise | |
| 1. Immediately revoke all capabilities issued by compromised agent | |
| 2. Rotate Ed25519 keypair (new key, new identity if necessary) | |
| 3. Audit all receipts signed by old key (may be forged) | |
| 4. Notify all systems that consume receipts from this agent | |
| 5. Drain old private key from all storage (HSM, filesystem, memory) | |
| 6. Document incident with timestamp and details | |
| ### Detected Proof Obligation Failure | |
| 1. Halt release process (transition blocked by gate) | |
| 2. Investigate failed proof: which obligation failed? | |
| 3. Review code for semantic changes or unproved invariants | |
| 4. Attempt re-proof with external verifier (Agda/Ada/Lean) | |
| 5. If re-proof fails: revert cell execution, understand root cause | |
| 6. Document in incident log (WORM-sealed) | |
| ### Detected Receipt Chain Tampering | |
| 1. Compute which receipts are affected (from gap in sequence) | |
| 2. Verify previous hash linkages (detect insertion point) | |
| 3. Revert affected cells (or entire notebook) | |
| 4. Investigate attacker access (how did they modify Prolog facts?) | |
| 5. Incident report to audit team and compliance officer | |
| --- | |
| **GOVERNANCE PRINCIPLE: TRANSPARENCY OR MISTRUST.** | |
| All vulnerabilities, mitigations, and residual risks are documented publicly. Users make informed decisions about deployment. | |
| *"EVIDENCE OR SILENCE."* | |