Skip to content

TCB.md

Latest commit

 

History

History
448 lines (316 loc) · 19.9 KB

TCB.md

File metadata and controls

448 lines (316 loc) · 19.9 KB

Lion Formal Verification - Trusted Computing Base (TCB)

Version: 2.1 (Open Source) Date: 2026-01-05 Status: END-TO-END CORRECTNESS PROVEN ✓

Executive Summary

Lion is a formally verified security architecture for a capability-based microkernel. This document defines what we PROVE vs what we ASSUME (the Trusted Computing Base).

Open Source Release: This is the abstract specification layer. Refinement proofs connecting to implementation are not included.

MILESTONE ACHIEVED: End-to-End Correctness Proof Complete

theorem any_reachable_from_init_is_secure (s : State) (h : Reachable init_state s) :
    EndToEndCorrectness s

What We Prove (Machine-Checked):

  • End-to-End Correctness (capstone theorem)
  • Complete Mediation (type-level enforcement via Authorized witness)
  • Confinement (semilattice algebra - rights cannot amplify)
  • Unforgeability (game-based cryptographic reduction)
  • Deadlock Recovery (timeout-based liveness)
  • Workflow Termination (concrete measure decrease)
  • Noninterference / TINI (stuttering bisimulation)
  • Attack Coverage (all attack classes mitigated)

What We Assume (TCB):

  • WASM sandbox correctness (Wasmtime)
  • Cryptographic hardness (SHA-256, HMAC)
  • Scheduler fairness (OS kernel)
  • Hardware correctness (CPU, memory)

1. What We PROVE

1.0 End-to-End Correctness (v1 Theorem 5.3) ⭐ CAPSTONE

Claim: Any state reachable from init_state satisfies full security.

Mechanism: Inductive proof over Reachable relation, composing all security properties.

structure EndToEndCorrectness (s : State) : Prop where
  system_invariant : SystemInvariant s      -- 11 security properties
  all_components_safe : AllComponentsSafe s -- Compositional security
  attack_coverage : ∀ attack, Mitigates attack s

theorem any_reachable_from_init_is_secure (s : State)
    (h_reach : Reachable init_state s) : EndToEndCorrectness s

Trust Level: IRONCLAD - Proven from 9 axioms, 0 sorry. Machine-checked.

Key Theorems:

  • init_satisfies_end_to_end: Base case
  • step_preserves_end_to_end: Inductive step
  • reachable_satisfies_end_to_end: Full induction
  • v1_theorem_5_3_invariant_preservation: Explicit v1 mapping
  • v1_theorem_5_5_security_composition: N-ary composition
  • v1_theorem_5_6_attack_coverage: Defense completeness

1.1 Complete Mediation (Theorem 012)

Claim: No effectful operation can occur without proper authorization.

Mechanism: Proof-by-construction via the Authorized witness type. The Step inductive type requires an Authorized witness for every state transition.

Trust Level: IRONCLAD - Type system enforces this at compile time.

structure Authorized (op : Operation) where
  h_policy : policy_allows op
  h_capability : capability_valid op.cap

1.2 Confinement (Theorem 004)

Claim: Rights cannot be amplified through delegation.

Mechanism: Rights form a semilattice under intersection. Delegation produces delegated_rights = parent_rights ∩ requested_rights ⊆ parent_rights.

Trust Level: IRONCLAD - Pure algebraic proof, no crypto assumptions.

1.3 Unforgeability (Theorem 001)

Claim: Capability forgery probability is negligible.

Mechanism: UF-CMA game reduction using HMAC-SHA256. Attacker advantage bounded by 2^(-λ/2) where λ = security parameter.

Trust Level: HIGH - Standard cryptographic proof.

Key Fix (2025-12-23): Replaced unsound hmac_injective_under_key axiom with provable injectivity via SymbolicTag inductive type.

1.4 Deadlock Freedom (Theorem 003)

Claim: The actor system never reaches a permanent deadlock.

Mechanism: Timeout-based recovery instead of cycle prevention. Any blocked actor eventually unblocks via timeout.

Trust Level: MEDIUM - Depends on scheduler fairness axiom.

Key Fix (2025-12-23): Removed unrealistic h_no_cycle precondition. Pivoted from deadlock prevention to deadlock detection & recovery.

1.5 Workflow Termination (Theorem 008)

Claim: Every workflow eventually terminates (success or failure).

Mechanism: Concrete lexicographic measure on (time_left, pending, active, retries). Each step strictly decreases the measure.

Trust Level: HIGH - Fully proven with bounded DFS cycle detection.

Key Fix (2025-12-23): Replaced circular measure_decreases_on_progress axiom with concrete WorkflowStep inductive and provable measure decrease.

2. What We ASSUME (Trusted Computing Base)

2.1 WASM Sandbox Correctness

Axiom: plugin_internal_frame - Plugin execution respects memory isolation.

axiom plugin_internal_frame :
  forall pid pi s s', PluginExecInternal pid pi s s' ->
    forall other, other ≠ pid -> s'.plugins other = s.plugins other

Dependency: Wasmtime implementation correctness. Verification: Not machine-checked. Relies on Wasmtime's own security guarantees.

2.2 Cryptographic Hardness

Axiom: hmac_collision_resistant - HMAC-SHA256 collision probability is negligible.

axiom hmac_collision_resistant (λ : ℕ) (m₁ m₂ : ByteArray) :
  m₁ ≠ m₂ →
  PrU (fun k => hmac_sha256 k m₁ = hmac_sha256 k m₂) ≤ 2^(-λ/2)

Dependency: SHA-256 hash function, HMAC construction. Verification: Standard cryptographic assumption, peer-reviewed.

2.3 Scheduler Fairness

Axiom: timeout_fairness - Blocked actors eventually unblock or timeout.

axiom timeout_fairness : ∀ sys a,
  sys.blockedSending a ≠ none →
  ∃ sys', ActorStep sys sys' ∧ sys'.blockedSending a = none

Dependency: OS scheduler, timeout mechanism. Verification: Runtime property, verified via TLA+ model checking (~50,000 states).

2.4 Serialization Injectivity

Axiom: serializeCap_injective - Capability serialization is canonical.

axiom serializeCap_injective : Function.Injective serializeCap

Dependency: Serialization implementation (e.g., protobuf, msgpack). Verification: Implementation detail, not mathematically deep.

3. What We DON'T Cover

3.1 Timing Channels (TINI, not TSNI)

The noninterference proof uses Termination-Insensitive Noninterference (TINI). Timing channels are explicitly out of scope:

  • Execution time differences
  • Termination vs non-termination
  • Cache timing attacks
  • Memory access patterns

Rationale: TSNI (Timing-Sensitive) requires hardware support and is overkill for a WASM plugin system.

3.2 Implementation Bugs

The Lean proofs verify the specification, not the implementation.

Open Source Scope: This release contains the abstract specification and proofs. Refinement proofs connecting to implementation are not included.

Gap: Bugs in the Rust kernel, WASM plugin host, or FFI bindings could violate security properties even with correct specifications. The specification proves what security means; implementation verification proves that the code does it.

3.3 Side-Channel Attacks

Physical side channels are out of scope:

  • Power analysis
  • Electromagnetic emissions
  • Acoustic attacks

3.4 Supply Chain Attacks

We assume:

  • Lean4 compiler is correct
  • Mathlib is trustworthy
  • Build toolchain is uncompromised

4. Axiom Audit Summary

Current Status: 9 axioms in 3 trust bundles ✅

4.1 The Three Trust Bundles

Bundle Category Underlying Axioms Risk
CryptoTrustBundle Crypto cap_mac_security, seal_assumptions, hash_assumptions LOW
RuntimeTrustBundle Runtime runtime_isolation, low_step_determinism_axiom, message_delivery_assumptions MEDIUM
RuntimeBridge Correspondence rust_type_instances, initial_correspondence_bundle, runtime_correspondence_preserved MEDIUM

Note: RuntimeBridge axioms define the interface for future binary validation. They are not exercised in this open source release (no refinement proofs included).

4.1.1 CryptoTrustBundle (Lion/Theorems/Unforgeability.lean)

Cryptographic hardness assumptions.

structure CryptoTrustBundle : Prop where
  mac_security : CapMACSecurity     -- HMAC-SHA256 UF-CMA security
  seal_props : SealAssumptions      -- Authenticated encryption
  hash_props : HashAssumptions      -- SHA-256 collision resistance

theorem crypto_trust_bundle : CryptoTrustBundle := ...

4.1.2 RuntimeTrustBundle (Lion/Theorems/RuntimeTrustBundle.lean)

Runtime environment correctness (WASM + scheduler).

structure RuntimeTrustBundle : Prop where
  isolation : RuntimeIsolation              -- WASM sandbox + key protection
  determinism : LowStepDeterministic        -- Scheduler picks unique step
  delivery : MessageDeliveryAssumptions     -- Scheduler routes messages fairly

theorem runtime_trust_bundle : RuntimeTrustBundle := ...

Components:

  • RuntimeIsolation: WASM memory bounds + HMAC key in kernel
  • LowStepDeterministic: Low steps are deterministic (scheduler assumption)
  • MessageDeliveryAssumptions: Messages eventually delivered (fairness)

4.1.3 RuntimeBridge (Lion/Contracts/RuntimeCorrespondence.lean)

Interface for future binary validation (not exercised in open source release).

These axioms define the correspondence interface between Lean specifications and Rust implementation. They are included for completeness but the refinement proofs that use them are not part of this release.

structure RuntimeBridge : Type 1 where
  type_instances : RustTypeInstances         -- Rust types are inhabited
  initial : InitialCorrespondence            -- Initial states correspond
  preserved : ∀ rs rs' ls, ...               -- Steps preserve correspondence

Opaque Types (trust boundary - would be implemented in Rust):

  • RustState, RustKernelState, RustPluginMemory, etc.

4.2 Underlying Axiom Count

The 3 bundles contain 9 underlying axioms:

Bundle Axiom File
Crypto cap_mac_security Unforgeability.lean
Crypto seal_assumptions Crypto.lean
Crypto hash_assumptions Crypto.lean
Runtime runtime_isolation RuntimeIsolation.lean
Runtime low_step_determinism_axiom RuntimeTrustBundle.lean
Runtime message_delivery_assumptions MessageDelivery.lean
Correspondence rust_type_instances RuntimeCorrespondence.lean
Correspondence initial_correspondence_bundle RuntimeCorrespondence.lean
Correspondence runtime_correspondence_preserved RuntimeCorrespondence.lean

4.3 Proof Status

0 sorries in entire Lion/ codebase. All theorems fully proven.

$ grep -rn "sorry" Lion/ --include="*.lean" | wc -l
0

~24,000 lines of Lean, 3,139 build jobs, 9 axioms.

4.4 Converted to Theorems (No Longer Axioms)

Former Axiom Disposition Date
time_bounded_when_running THEOREM 2025-12-31
termination_time_bounded THEOREM 2025-12-31
workflow_eventually_terminates THEOREM 2025-12-31
prf_assumptions Replaced by cap_mac_security 2025-12-31
exp_sum_bound_nat THEOREM (via Mathlib asymptotics) 2026-01-01
hmac_key_in_kernel Bundled into runtime_isolation 2025-12-31
plugin_internal_respects_bounds Bundled into runtime_isolation 2025-12-31
default_policy_state Eliminated (PolicyProvider typeclass) 2025-12-31
high_step_no_downgrade THEOREM (non-declassify steps) 2025-12-31
authorized_write_requires_dominance THEOREM (via h_biba in Authorized) 2025-12-31
cap_send_requires_dominance ELIMINATED (baked into can_communicate definition) 2025-12-31
step_consistent_implies_nd THEOREM (via low_step_match_same_type) 2026-01-01
seal_assumptions Bundled into CryptoTrustBundle 2026-01-01
hash_assumptions Bundled into CryptoTrustBundle 2026-01-01
rust_type_instances Bundled into RuntimeBridge 2026-01-01
initial_correspondence_bundle Bundled into RuntimeBridge 2026-01-01
runtime_correspondence_preserved Bundled into RuntimeBridge 2026-01-01
TINI_noninterference THEOREM (via stuttering bisimulation) 2026-01-01
low_step_match_same_type THEOREM (via strengthened step_consistent) 2026-01-01
low_step_match_level ELIMINATED (subsumed by low_step_match_same_type) 2026-01-01
hmac_injective_under_key Removed (unsound) 2025-12-23
measure_decreases_on_progress Removed (circular) 2025-12-23

4.5 Target: 3 True Trust Bundles ✅ ACHIEVED

The 3 conceptual trust bundles are now in place:

  1. Crypto: CryptoTrustBundle - MAC unforgeability + seal + hash assumptions
  2. Runtime: RuntimeTrustBundle - WASM sandbox + scheduler determinism + message delivery
  3. Correspondence: RuntimeBridge - Rust↔Lean step correspondence

All other security properties are provable theorems from these bundles.

No orphan axioms remaining - all axioms are properly bundled into one of the 3 categories.

5. Honest Claims

What You CAN Say

"Lion features a Formally Verified Security Architecture. We have machine-checked proofs that the kernel's design specification guarantees Complete Mediation, Confinement, and Unforgeability, assuming the correctness of the underlying WASM sandbox and cryptographic primitives."

What You SHOULD NOT Say

  • "Lion is a formally verified microkernel" (implies binary correctness like seL4)
  • "Lion has zero security vulnerabilities" (implementation not verified)
  • "Lion is immune to timing attacks" (TINI, not TSNI)

6. Comparison to Other Verified Systems

Aspect Lion (Open Source) seL4 CertiKOS
Proof Assistant Lean4 Isabelle/HOL Coq
LOC Proven ~24,000 ~200,000 ~100,000
LOC Verified (impl) 0 (spec only) 8,830 C 6,500 C
End-to-End Proof ✓ Complete ✓ Complete ✓ Complete
Refinement Proofs Not included 4-layer Layered
Binary Verification No Yes (ARM/RISC-V) Partial
Crypto Integration Yes (HMAC) Abstracted Abstracted
Axiom Count 9 ~50 ~30

Lion's Position: Complete specification-level verification with end-to-end correctness proof. This open source release is analogous to seL4's abstract specification layer.

7. Future Work (Not in Open Source Release)

  1. Refinement Proofs: Rust↔Lean correspondence connecting spec to implementation
  2. Hardware Model: Cache, TLB, DMA considerations
  3. TSNI: Timing-sensitive noninterference for high-security contexts
  4. Property Tests: Property-based tests matching Lean properties

8. Document History

Date Change
2025-12-23 Initial TCB document after adversarial review
2025-12-23 Fixed HMAC axiom crisis (SymbolicTag approach)
2025-12-23 Pivoted DeadlockFreedom to timeout-based liveness
2025-12-23 Replaced circular termination axiom with concrete measure
2025-12-31 Fixed time_tick bug (deterministic now+1)
2025-12-31 Converted 3 termination axioms to theorems (28→18)
2025-12-31 Replaced PRFAssumptions with CapMACSecurity
2025-12-31 Converted exp_sum_bound_nat to lemma+sorry (18→14 axioms)
2025-12-31 Phase 9: Converted authorized_write_requires_dominance to theorem via h_biba (11→10 axioms)
2025-12-31 Phase 11: Eliminated cap_send_requires_dominance by baking Biba check into can_communicate (10→9 axioms)
2026-01-01 Bundled crypto axioms into CryptoTrustBundle (3→1 conceptual)
2026-01-01 Bundled correspondence axioms into RuntimeBridge (3→1 conceptual)
2026-01-01 Converted step_consistent_implies_nd to theorem via low_step_match_same_type
2026-01-01 Target achieved: 3 true trust bundles (Crypto, Runtime, Correspondence)
2026-01-01 TINI_noninterference converted to THEOREM via stuttering bisimulation
2026-01-01 Eliminated low_step_match_same_type and low_step_match_level axioms (12→10 axioms)
2026-01-01 Strengthened step_consistent signature to return matching step properties
2026-01-01 exp_sum_bound_nat converted to THEOREM via Mathlib asymptotics (no more math fact sorries)
2026-01-02 Expanded RuntimeCorrespondence from 3 to 9 fields (full-state coverage)
2026-01-02 Added 6 new opaque types: RustPluginLevel, RustHeldCaps, RustActorRuntime, RustResources, etc.
2026-01-02 Added HostCallFootprint framework for systematic preservation proofs
2026-01-02 Added BoundsInv (overflow safety) and SystemInv invariants
2026-01-02 Eliminated PluginIdWithinU64 sorry via Inhabited PluginState
2026-01-03 Fixed critical valid_dag bug (only detected 1-2 step cycles, now uses bounded DFS)
2026-01-03 Added policy distributivity laws (Kleene three-valued logic completeness)
2026-01-03 Added PolicyWorkflowBridge.lean (Track A ↔ Track B connection, 523 lines)
2026-01-03 END-TO-END CORRECTNESS PROVEN - EndToEnd.lean capstone theorem (269 lines)
2026-01-03 Eliminated all sorries (0 remaining)
2026-01-05 TCB v2.1 - Open source release (refinement layer removed, ~24k lines)