# Formal Methods Assurance — Honest Assessment

This document is a self-audit of Nucleus's formal verification claims.
It tries to be more critical of our work than any external reviewer would be.
If you find a gap this document doesn't disclose, please file an issue.

## What We Verify

### 1. Permission Lattice Algebra (Lean 4 — unbounded, kernel-checked)

**What's proved:**
- `CapabilityLevel` (3-element total order) is a `HeytingAlgebra` — full Mathlib instance
- `CapabilityLattice` (13-dimensional product) is a `HeytingAlgebra` — 23 theorems
- Function correspondence: the Aeneas-generated `meet`/`join`/`implies` compute the
  same result as the Mathlib lattice operators — closing the loop between Rust and Lean
- Monotonicity: `(a ⊓ b) ≤ a` — permissions can only tighten (VC-001)
- Idempotency: `a ⊓ a = a` — applying the same policy twice is a no-op

**What's NOT proved:**
- The `PermissionLattice` (which wraps `CapabilityLattice` + path rules + budget + time)
  is not in Lean. Only the capability dimensions are verified algebraically.
- The Aeneas pipeline only translates `CapabilityLevel` and `CapabilityLattice`.
  `ExposureSet`, `Operation`, and `IFCLabel` are not yet translatable by Aeneas
  (it errors on `bool`-field structs and 13-variant enums with `repr(u8)`).

**Correspondence gap:**
The Lean types (`PortcullisCore.Types`) are machine-generated by Aeneas from the
Rust source. The lattice FUNCTIONS are hand-curated extracts from the full Aeneas
output, because the full output includes trait impls that don't compile under Lean 4.28.
The curated functions are UNMODIFIED from Aeneas output — the bodies are byte-for-byte
identical — but we selected which functions to include. CI verifies the Aeneas output
hasn't drifted from the committed code.

**Note:** The generated Lean code currently has 12 CapabilityLattice fields (missing
`spawn_agent`). The Rust source has 13. A re-extraction is needed to close this gap.

### 2. Exposure Tracker (Lean 4 — unbounded, kernel-checked, hand-written model)

**What's proved:**
- Monoid laws: `union` is associative, commutative, idempotent with `empty` as identity
- Monotonicity: exposure count never decreases under `union`
- Once uninhabitable, always uninhabitable (under `union`)
- Uninhabitable ↔ count = 3 (sound and complete)
- `classify_operation` maps all 13 operations to the correct labels
- `should_gate` blocks exfil when completing/maintaining uninhabitable state
- `should_gate` never blocks non-exfil operations
- `should_gate` never blocks anything from empty state

**What's NOT proved:**
- These proofs are on a HAND-WRITTEN Lean model, not Aeneas-generated code.
  Aeneas cannot currently translate `ExposureSet` (struct with `bool` fields).
- Correspondence between the Lean model and the Rust source is enforced by
  `include_str!` compile-time tests, not by machine-verified bisimulation.

### 3. IFC Label Lattice & Flow Kernel (Lean 4 — unbounded)

**What's proved (20 theorems in FlowProofs.lean):**
- Authority confinement: adversarial data cannot steer privileged actions
- Integrity taint propagation: join of labels preserves integrity ordering
- Invariant exploit theorem: WebContent → OutboundAction is blocked
- Label monotonicity: propagation only widens labels (never narrows)
- Freshness expiry detection

**What's proved (15 theorems in FlowGraphProofs.lean):**
- Semilattice properties of the causal DAG
- Label propagation through parent chains

**What's proved (11 theorems in DeclassifyProofs.lean):**
- Declassification rule safety properties

**What's proved (12 theorems in DecidePureProofs.lean):**
- `decide_pure()` correctness properties

### 4. DecisionToken Linearity (Kani BMC — bounded)

**What's proved (5 harnesses, E1-E5):**
- E1: `decide()` produces a token iff verdict is `Allow` (symbolic over all 13 ops)
- E2: Denied operations never produce tokens
- E3: Token operation and sequence match the decision
- E4: `issue_approved_token()` produces audited tokens with exposure tracking
- E5: `issue_approved_token()` bypass under deny policy is still audited

### 5. FlowGraph DAG Invariants (Kani BMC — bounded)

**What's proved (G1-G8):**
- G1: Sentinel parent (ID 0) always rejected
- G2-G6: Various DAG structural invariants
- G7: Denied nodes cannot become parents (causal isolation)
- G8: Denied set persists across subsequent operations

### 6. Certificate & Delegation (Kani BMC — bounded)

**What's proved (C1-C3):**
- C1: `meet(parent, child) ≤ parent` — delegation is deflationary
- C2: SHA-256 is deterministic for symbolic inputs
- C3: Chain depth exceeding max is rejected

### 7. I/O Confinement (Kani BMC — bounded)

**What's proved (IO-1, IO-2):**
- IO-1: `Never` capability always produces `Deny` — kernel cannot escalate beyond policy
- IO-2: `meet(parent, child)` never exceeds parent for any dimension — delegation
  cannot widen the I/O surface

### 8. Adversarial Rejection Scenarios (integration tests)

**What's covered (12/12 scenarios from §12):**
- Scenarios 1-4: Covered by existing exposure/lattice tests
- Scenario 5: Classifier tampering rejected (deterministic mapping)
- Scenario 8: Replay attack detected by receipt chain hash links
- Scenario 9: Lineage tampering detected by HWM file
- Scenario 10: Sandbox relaxation blocked by compartment `meet()`
- Scenario 11: Exposure tracks regardless of file arguments
- Scenario 12: Policy/code mismatch detected by compiler hash

## What We DON'T Verify

These are important security properties that have NO formal verification:

1. **Sandbox isolation** — Firecracker VM boundary, seccomp BPF filters, filesystem
   sandboxing. Tested but not formally verified.

2. **Cryptographic operations** — Ed25519 signing in receipts uses the `ring` library.
   We trust the library, not our own proof.

3. **Network policy enforcement** — `iptables` rules for agent network isolation.

4. **Time and budget checks** — Runtime checks with no formal model.

5. **Path and command restrictions** — String-based matching, no formal filesystem model.

6. **Concurrency** — The hook is single-threaded. No formal concurrency model.

7. **Compartment transitions** — The flow graph reset on compartment transition is tested
   but not formally verified. The monotonicity property of compartment ceilings is
   verified by Kani (IO-2: meet never exceeds parent) but not by Lean.

8. **Receipt chain integrity** — Hash chaining and Ed25519 signing are tested but the
   append-only property is not formally proved in Lean (issue #427).

9. **Hook I/O boundary** — The `nucleus-claude-hook` binary's stdin/stdout JSON parsing
   is not verified. The `hook_adapter` module extracts pure decision logic for future
   verification, but the I/O wrapper remains unverified.

## Verification Stack Summary

| Layer | Tool | Scope | Bound | Artifacts | CI |
|-------|------|-------|-------|-----------|-----|
| Lattice algebra + correspondence | Lean 4 + Mathlib + Aeneas | `CapabilityLevel`, `CapabilityLattice` HeytingAlgebra | Unbounded | 23 theorems | Every PR |
| Exposure tracker | Lean 4 | `ExposureSet`, `classify_operation`, `should_gate` | Unbounded | 16 theorems | Every PR |
| IFC labels + flow kernel | Lean 4 | Authority, integrity, Invariant exploit | Unbounded | 20 theorems | Every PR |
| Flow graph DAG | Lean 4 | Semilattice, label propagation | Unbounded | 15 theorems | Every PR |
| Declassification rules | Lean 4 | Rule safety properties | Unbounded | 11 theorems | Every PR |
| Decision logic | Lean 4 | `decide_pure()` correctness | Unbounded | 12 theorems | Every PR |
| Bridge/correspondence | Lean 4 | Aeneas fn = lattice op | Unbounded | 23 theorems (overlap) | Every PR |
| DecisionToken | Kani BMC | Token issuance, audit, exposure | Bounded | 5 harnesses | Every PR |
| FlowGraph DAG | Kani BMC | Denied-parent, structural invariants | Bounded | 8 harnesses | Every PR |
| Certificate delegation | Kani BMC | Monotonicity, depth, hash | Bounded | 3 harnesses | Every PR |
| I/O confinement | Kani BMC | Never→Deny, delegation narrowing | Bounded | 2 harnesses | Every PR |
| Permission algebra | Kani BMC | Distributivity, monotonicity, monoid | Bounded | ~45 harnesses | PR (fast) + nightly |

**Total: 68 Kani BMC harnesses + 98 Lean 4 theorems = 166 verification artifacts.**

## Claude Code Hook — What's Verified vs Not

The `nucleus-claude-hook` binary is the user-facing product. Here's what's verified:

| Component | Verified? | How |
|-----------|-----------|-----|
| Tool → Operation mapping | **Tested** (unit + Kani classify) | `hook_adapter::classify_tool()` |
| Capability check | **Lean + Kani** | `CapabilityLattice::meet/leq` |
| Exposure accumulation | **Lean** | `ExposureSet` monoid + gating |
| Flow taint propagation | **Lean** | IFC label lattice + FlowGraph |
| Denied-parent isolation | **Kani** | G7, G8 harnesses |
| I/O confinement | **Kani** | IO-1, IO-2 harnesses |
| DecisionToken linearity | **Kani** | E1-E5 harnesses |
| Compartment ceiling | **Kani** (via IO-2) | `meet` never exceeds parent |
| Receipt chain hashing | **Tested** | Hash chain + tamper detection |
| Receipt Ed25519 signing | **Tested** | sign/verify roundtrip |
| DAG leaf tracking | **Tested** | LeafTracker unit tests |
| Session tamper detection | **Tested** | HWM file survives state deletion |
| JSON protocol parsing | **Not verified** | Trusted boundary |
| Session state persistence | **Not verified** | File I/O |
| Side-channel compartment file | **Not verified** | File I/O |

## Known Limitations & Honest Caveats

1. **Kani is bounded, not complete.** For the lattice properties (3-element type,
   13-dimensional product), the bound covers the entire state space. For kernel
   decision logic with strings and paths, the bound is a practical limit.

2. **Lean proofs are on models, not machine code.** The Aeneas pipeline provides
   correspondence for `CapabilityLevel` and `CapabilityLattice`. Other types use
   hand-written Lean models with structural correspondence tests.

3. **The exposure tracker Lean model is hand-written.** `include_str!` tests enforce
   structural correspondence but not semantic correspondence.

4. **No proof of the full `decide()` function.** The kernel calls verified lattice
   and exposure logic, but also checks time, budget, paths, commands (not verified).

5. **The Aeneas-generated Lean code is stale.** The committed Types.lean has 12
   CapabilityLattice fields; the Rust source has 13 (spawn_agent was added).
   CI re-extracts and checks, but the committed files need updating.

6. **The flow graph in the hook is a DAG, not the full causal graph.** The
   `LeafTracker` assigns parents by source category (trusted vs adversarial).
   This is conservative but not precise — we don't know the true causal
   dependencies between tool calls because Claude Code doesn't provide them.

## How to Reproduce

```bash
# Lean 4 proofs (requires elan)
cd crates/portcullis-core/lean
lake build   # All proof files

# Kani BMC (requires kani toolchain)
cargo kani -p portcullis --solver cadical

# Aeneas pipeline (requires Nix or manual Charon/Aeneas install)
./scripts/aeneas-translate.sh

# Verify no sorry (proof holes)
grep -rn 'sorry' crates/portcullis-core/lean/ --include='*.lean'
# Should return only comments, never proof terms

# Assurance report
cargo run -p nucleus-audit -- assurance --project-dir .
```

## Comparison to Other Projects

| Project | Scope | Proof depth | Our gap |
|---------|-------|-------------|---------|
| seL4 | Microkernel | Full functional correctness, binary verified | We verify algebra + decision logic, not the full kernel or binary |
| AWS Cedar | Authorization policy | Lean 4 policy evaluation | We verify capability accumulation + IFC, not policy evaluation |
| Microsoft Fides | Agent IFC | Confidentiality/integrity labels, deterministic enforcement | Similar approach; we have Lean proofs + runtime hook, they have a framework |
| OPA/Rego | Policy as code | No formal verification | We have Lean + Kani proofs |
| HACL* | Cryptography | F* + C extraction | We trust ring, don't verify crypto |
| CompCert | C compiler | Coq, binary-level | We use the standard "trusted compiler" assumption |

## Component Status

Full maturity table for every nucleus component. **Maturity key:** *Verified* = formal proofs + tests. *Tested* = compiles, has passing tests, never deployed. *Partial* = works for some cases, known gaps. *Implemented* = code exists, minimal testing.

| Component | Maturity | Evidence |
|-----------|----------|----------|
| **Permission lattice** (portcullis) | Verified | 162K LOC, 1,443 tests, 297 Verus VCs, 112 Kani BMC proofs, 3 fuzz targets |
| **Uninhabitable state detection** | Verified | Static scan + runtime guard, monotonicity proven (E1-E3, Kani B1-B9) |
| **Attenuation tokens** | Verified | Compact delegation credentials with Kani-proven invariants (D1-D7) |
| **Delegation chains** | Verified | Monotone attenuation with `meet_with_justification`, Lean proofs for delegation narrowing |
| **Deep packet inspection (DPI)** | Verified | `DerivationClass`, `EffectKind`, `StorageLane`, `FieldEnvelope`, `WitnessBundle`. 3 Kani proofs + 16 Lean theorems |
| **Constitutional kernel** | Tested | `ck-kernel` admission engine, `PolicyRuleSet`, 17 Kani proofs |
| **Unicode injection defense** | Tested | 8-category invisible character detection; warn/strip/deny policy |
| **Execution receipts** | Tested | Cryptographic pod execution proof with token usage and cost tracking |
| **Permission market** | Tested | Lagrangian pricing oracle for multi-dimensional capability constraints |
| **Web fetch security** | Tested | Unified MCP+HTTP path: MIME gating, DNS/URL allowlist, redirect verification |
| **Audit log verification** | Tested | HMAC-SHA256 + SHA-256 chain; optional S3 append-only sink |
| **PodSpec scanner** | Tested | Uninhabitable state, credentials, network, isolation, timeout checks |
| **Claude Code scanner** | Tested | Uninhabitable state via allow/deny projection, Bash capability propagation |
| **MCP config scanner** | Tested | Well-known server classification (15 packages), `npx -y` supply chain detection |
| **Permission profiles** | Tested | 18 named profiles (10 canonical + 8 legacy) backed by lattice constructors |
| **Tool proxy** (MCP enforcement) | Tested | 154 tests; enforces agent sessions in GitHub Actions |
| **Firecracker isolation** | Tested | Real jailer invocation + iptables; Linux+KVM only |
| **Network enforcement** | Tested | Default-deny egress, DNS allowlisting, drift detection |
| **Causal ancestry** | Tested | Per-artifact `FlowGraph::causal_label()` queries; kernel refactored for artifact-granular decisions |
| **Governed memory** | Tested | `GovernedMemory` with rebuttal history and `MemoryAuthority` |
| **Egress policy** | Tested | Config-driven `EgressPolicy` with `HostPattern` matcher wired into `Kernel::decide()` |
| **Receipt chain** | Tested | Hash-chain integrity for linked execution receipts across sessions |
| **OWASP LLM Top 10 gauntlet** | Tested | 70 attack scenarios covering all 9 OWASP LLM vulnerability categories |
| **DPI flow red team** | Tested | 33 red team tests for causal flow graph attacks |
| **OTLP permission telemetry** | Tested | OTel spans with all 13 capability dimensions, exposure state, lockdown status |
| **Fleet lockdown** | Tested | `nucleus lockdown` drops agents to read-only via gRPC streaming (sub-second) |
| **C2PA content credentials** | Tested | c2pa-rs manifest builder, signer config, sidecar emission, audit verification |
| **AI confidence scoring** | Tested | `AiDerivedWitness` with input context hash, model ID, multi-generation agreement rate |
| **Budget tracking** | Partial | AtomicBudget exists; pre-exec reservation works, post-exec accounting incomplete |
| **SPIFFE identity** | Implemented | mTLS + cert management code exists; no SPIRE deployment |
| **Command exfiltration detection** | Partial | Program-name matching; `bash -c` bypasses documented |

## Verification Tools

| Tool | Type | Count | What It Proves |
|------|------|-------|----------------|
| **Lean 4 + Mathlib** | Unbounded, kernel-checked | 165 theorems | HeytingAlgebra, IFC flow rules, compartment safety, delegation narrowing, DerivationClass lattice |
| **Kani** | Bounded model checking | 112 harnesses | DecisionToken linearity, lattice distributivity, exposure monoid, constitutional kernel invariants |
| **Verus** | SMT (Z3) | 297 VCs | Lattice laws, nucleus operator, Heyting adjunction, Galois connections, graded monad |
| **Proptest** | Property-based testing | 130+ invariants | Full PermissionLattice composition |
| **Red team** | Adversarial testing | 162 scenarios | OWASP LLM Top 10, DPI flow attacks, delegation chain attacks |

## Permission Lattice Algebra

| Structure | What It Gives You | Status |
|-----------|-------------------|--------|
| **Quotient Lattice** | Uninhabitable state detection as a structural nucleus operator | Verified (Verus) |
| **Heyting Algebra** | Conditional permissions with formal semantics | Verified (Verus + Lean) |
| **Galois Connections** | Policy translation across trust domains | Verified (Verus) |
| **Graded Monad** | Risk accumulation through computation chains | Verified (Verus) |
| **Deep Packet Inspection** | DerivationClass, EffectKind, StorageLane, FieldEnvelope, WitnessBundle | Verified (Kani + Lean) |
| **Attenuation Tokens** | Compact delegation credentials for wire transport | Verified (Kani D1-D7) |
| **Exposure Invariants** | Exposure-set monotonicity, uninhabitable state iff count==3 | Verified (Kani B1-B9) |
| **Modal Operators** | Distinguish "guaranteed safe" from "might be safe" | Tested |
| **Delegation Chains** | Monotone attenuation with justification trails | Verified (Lean) |
