Skip to main content

9. The Trusted Computing Base (TCB) & Axiom Audit

1. Introduction: The "Roots of Trust" in a Total Adversary Model​

In formal verification, the Trusted Computing Base (TCB) is the set of all components (software, hardware, and mathematical assumptions) that must be correct for the verification results to be valid. If a component in the TCB is flawed, the verifier might report a "Success" for code that actually contains a critical bug.

Sector9 operates under a Total Adversary model. We assume all participants—including the SR9 toolchain developers themselves—are rational, greedy adversaries. The TCB is the only "Trust" we admit, and its reduction and audit are the primary missions of the Proving Ground.

Sector9’s TCB is composed of three major layers:

  1. The Infrastructure: The OCaml compiler, the Viper verifier, and the Z3 SMT solver.
  2. The Prelude (prelude.ml): The Viper-level axioms that define the mathematical semantics of the language.
  3. The Prim layer: The language-level stubs and trusted functions that bridge the specification to the runtime.

This research performs an Axiom Audit to identify the most sensitive assumptions in Sector9 and evaluates the risk of "Axiom Inconsistency."

2. The Viper Prelude: Mathematical Foundations​

The code in src/viper/prelude.ml is the "Heart of the TCB." It defines how Sector9's high-level concepts (arrays, tuples, maps) are seen by the SMT solver.

The Array Injectivity Axiom​

One of the most sensitive axioms in the prelude is the Array Loc Inversion:

axiom $all_diff_array {
  forall $a: Array, $i: Int :: {$loc($a, $i)}
    $loc_inv1($loc($a, $i)) == $a && $loc_inv2($loc($a, $i)) == $i
}

Assumption: Every unique pair of (array, index) maps to a unique heap reference (Ref). Risk: If the IC runtime or the compiler’s memory layout violates this (e.g., via shared internal buffers or overlapping fields), the verifier will prove properties that are false at runtime. Sector9 mitigates this by ensuring the compiler's code generation strictly follows this disjointness model.

Tuple and Option ADTs​

Sector9 generates domain-based encodings for Tuples and Options to ensure compatibility with various Viper versions.

axiom some_injective {
  forall $v1: T, $v2: T :: Some($v1) == Some($v2) ==> $v1 == $v2
}

These are "Standard ADT Axioms" and are generally low-risk, provided the Z3 solver’s theory of equality is sound.

3. The prim.mo Layer: Spec-only Truths​

The src/prelude/prim.mo file defines constructs that are "Pure and Trusted."

Spec-Only Quantifiers​

Functions like Prim.forall and Prim.exists are marked as pure trusted.

pure trusted func forall<T>(f : T -> Bool) : Bool

Assumption: The verifier correctly translates these into SMT-level quantifiers. Risk: These functions have trap bodies at runtime, so they are intended for specifications and ghost proof code only. Sector9's proof-dependency checks, runtime projection checks, and proof-only type restrictions reject proof-only values from executable roots; the trap body is a backstop if such a function were somehow emitted into runtime code.

4. Arithmetic Soundness: The Partiality Strategy​

A common source of inconsistency in SMT verifiers is fixed-width arithmetic (e.g., Nat32). If a verifier assumes a + b is always a Nat32, it becomes unsound when an overflow occurs.

Sector9 uses a Partial Axiom Strategy in prelude.ml:

axiom {
  forall $a, $b :: 0 <= $a && $a <= MAX && 0 <= $b && $b <= MAX && $a + $b <= MAX ==>
  $add_nat32($a, $b) == $a + $b
}

The Assumption: The verifier only knows the result of an operation if it can prove there is no overflow. The Safety Net: If an overflow might occur, the $add_nat32 function becomes Uninterpreted. The solver doesn't know its value, and any postcondition that depends on the exact result will fail to verify.

This is a high-integrity choice. It moves the risk from "Unsoundness" (accepting bad code) to "Incompleteness" (rejecting good code). For DeFi, this is the correct trade-off.

5. The "Place" and "Address" TCB​

Sector9 implements a Prusti-inspired logical identity system.

domain Place {
  function $place_index($base: Place, $i: Int): Place
  // ... axioms for disjointness and inversion
}

This is the TCB for Alias Reasoning. The system assumes that p.field1 and p.field2 are distinct logical identities. Soundness Check: The verifier must ensure that no two fields in a Sector9 record ever share the same field_tag. Sector9 enforces this via the shape/tag machinery, which generates unique, stable tags for every record field in the program.

6. SMT Solver Dependency (Z3)​

Sector9, like Dafny and Viper, is ultimately dependent on the soundness of Z3.

  • The Risk: Z3 bugs are rare but exist, especially in the theory of non-linear integer arithmetic and quantifiers.
  • Mitigation: Sector9 avoids non-linear arithmetic where possible (e.g., using partial axioms for multiplication) and uses explicit triggers (Subject 7) to keep the solver within its "Well-Behaved" subset.

7. Evaluation & Comparison​

vs. Solidity (Trusting the Compiler)​

In Solidity, the TCB includes the entire solc compiler. Verification usually happens on the bytecode (using HEVM or Certora), which is safer but much harder to write.

  • Sector9: The TCB includes the sector9 translator. Verification obligations are generated from typed Sector9/MVIR into Viper, which reduces some source/model drift but still trusts the translation pipeline more than a bytecode-level verifier would.

vs. Move Prover (Axiom Volume)​

The Move Prover has a massive set of axioms for its global storage and resources.

  • Sector9: Has a relatively small, modular prelude. This makes the Sector9 TCB easier to audit and reduces the risk of cross-axiom contradictions (which can lead to proving 1=0).

vs. Coq / Isabelle (Proof Checking)​

Interactive proof assistants have the smallest TCB (a small kernel that checks proofs).

  • Sector9: Sacrifices the tiny TCB for Automation. The use of SMT solvers and a complex prelude is what enables the "One Codebase" experience.

8. Conclusion: The Dual-Proof Architecture​

Sector9's Trusted Computing Base is engineered for protocol safety, but it remains part of the assurance argument and must be reviewed like any other trusted component:

  1. SR9 (Logic Proof): Checks stated contracts and invariants, anchored in the audited TCB (axioms, prelude, and translator).
  2. Internet Computer (Execution Proof): Provides replicated deterministic execution and platform-level protection against malicious node providers.

While the verifier depends on Z3 and a complex OCaml pipeline, the modular nature of the prelude.vpr and adversarial review in the Proving Ground create incentives to find flaws. In this model, trust is reduced through collective responsibility, explicit assumptions, and slashing rules for accepted claims that later fail.

Strengths:

  1. Fail-Closed Arithmetic: Partial axioms prevent unsoundness from overflows.
  2. Modular Prelude: Easy to audit and update for different Viper backends.
  3. Logical Identity: "Places" provide a sound foundation for alias reasoning.

Weaknesses:

  1. Complex Translator: The Sector9-to-MVIR-to-Viper pipeline is large and has a high "surface area" for implementation bugs.
  2. Runtime-Proof Gap: There is still a small gap between the mathematical model (Viper) and the actual Wasm runtime (Subject 10).