SNAPKITTYWEST

push from SNAPKITTYWEST/rowm-polymorphic-notebook

1d3f990 verified 3 days ago

preview code

Raw

History Blame Contribute Delete

18 kB

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)

Prolog/Datalog engine — Logic evaluation, rule grounding
Rust runtime — Memory safety, WORM enforcement
Cryptographic libraries — Blake3, Ed25519 (from established crates)
Kernel/OS — Process isolation, filesystem, system clock

Untrusted Components (Validated Before Use)

External source code — All user-provided code in any language
Notebook metadata — Cell definitions, execution counts, outputs
Network input — Remote code, serialized instructions, proofs
User-provided proofs — Terms claimed to be proofs (external tools verify)
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

Implement Ed25519 signing (NOT HMAC) for all receipts
Enforce full-hash usage (no truncation)
Test proof tool integrations end-to-end
Add per-system context binding to receipts (replay protection)
Implement notebook signing (GPG or Ed25519)
Migrate to canonical time (logical clock or Git height)
Use HSM for private keys (not filesystem storage)
Enable SELinux/AppArmor for process isolation
Audit Prolog engine for fact retraction vulnerabilities
Pin dependency versions and verify checksums

Ongoing Operations

Rotate Ed25519 keys annually or on compromise suspicion
Monitor Blake3/Ed25519 cryptanalysis literature
Run regular security audits (penetration testing)
Log all authorization failures (detect attacks)
Verify receipt chains weekly (detect tampering)
Back up WORM ledger to geographically distributed stores
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

Immediately revoke all capabilities issued by compromised agent
Rotate Ed25519 keypair (new key, new identity if necessary)
Audit all receipts signed by old key (may be forged)
Notify all systems that consume receipts from this agent
Drain old private key from all storage (HSM, filesystem, memory)
Document incident with timestamp and details

Detected Proof Obligation Failure

Halt release process (transition blocked by gate)
Investigate failed proof: which obligation failed?
Review code for semantic changes or unproved invariants
Attempt re-proof with external verifier (Agda/Ada/Lean)
If re-proof fails: revert cell execution, understand root cause
Document in incident log (WORM-sealed)

Detected Receipt Chain Tampering

Compute which receipts are affected (from gap in sequence)
Verify previous hash linkages (detect insertion point)
Revert affected cells (or entire notebook)
Investigate attacker access (how did they modify Prolog facts?)
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."