Skip to content

VERIFICATION_PLAN.md

Latest commit

 

History

History
320 lines (248 loc) · 12.1 KB

VERIFICATION_PLAN.md

File metadata and controls

320 lines (248 loc) · 12.1 KB
Raw

Verification Plan

Two orthogonal verification tracks, not three sequential levels.

TLA+ and Isabelle answer fundamentally different questions and can proceed independently. Frama-C is available as an optional iteration tool during Isabelle work but is not a required stage.

There is no deadline. The goal is to learn where the ideas hold and where the assumptions are wrong.

Why not everything in Isabelle

Isabelle and TLA+ address different questions:

  • Isabelle + AutoCorres asks: does this C function compute what the abstract spec says? It reasons about individual functions, sequential execution, and memory.

  • TLA+ asks: does this distributed protocol have the safety and liveness properties we claim, regardless of message ordering? It reasons about concurrent state across multiple modules over time.

seL4 itself does not use TLA+ because the kernel is a single-node sequential program. This project is different — the coordination protocol is distributed by design. The question "will a module that stops sending eventually be declared dead by all of its neighbors" is a liveness property over a distributed system. TLA+'s temporal logic (<>, []) handles this naturally. Encoding the same property in Isabelle/HOL is possible but significantly harder.

The two tracks are therefore complementary, not redundant.

Track A — TLA+ Protocol Model

Question: Do the heartbeat and consensus protocols have the safety and liveness properties we intend, independent of any C implementation?

Tool: TLA+ with TLC model checker. Java is already installed — no further setup required beyond the TLA+ VS Code extension or Toolbox.

File layout:

docs/tla/
  Heartbeat.tla       -- heartbeat state machine
  HeartbeatMC.tla     -- TLC model config (symmetry sets, state constraints)
  Consensus.tla       -- threshold voting protocol
  ConsensusMC.tla
  Topology.tla        -- k-nearest election (stretch goal)

As built: the layout above is the original plan, not what is on disk. Only the consensus model was built — docs/tla/EkkConsensus.tla + EkkConsensus.cfg (Phase A2). The heartbeat state machine (A1) was instead discharged in Isabelle as phase B3 (the valid_health_edge refinement), so no Heartbeat.tla exists. The topology election (A3) stays a stretch goal and is not modeled.

Phase A1 — Heartbeat state machine

Model a single module's view of its neighbors. Each neighbor is a TLA+ variable with state in {UNKNOWN, ALIVE, SUSPECT, DEAD}. The heartbeat tick is an action. The re-discovery message is a separate action.

Properties to check with TLC:

  • Safety: health transitions only follow defined edges — no UNKNOWN → SUSPECT skip, no DEAD → ALIVE without re-discovery

    HealthTransition(from, to) ==
    \/ from = to
    \/ from = "UNKNOWN"  /\ to = "ALIVE"
    \/ from = "ALIVE"    /\ to = "SUSPECT"
    \/ from = "SUSPECT"  /\ to = "DEAD"

  • Liveness: a module that stops sending will eventually reach DEAD

    <>(missed_count >= TIMEOUT_COUNT => health = "DEAD")

    This requires a fairness assumption on the tick action — make it explicit.

Phase A2 — Consensus protocol

Model N modules, each holding a copy of the active ballot. Votes arrive as TLA+ actions from any module to any other.

Properties to check:

  • Agreement: no two modules can simultaneously observe APPROVED and REJECTED for the same ballot ID
  • Validity: APPROVED is only reachable when yes_count / total >= threshold at the point all votes are counted
  • Termination: once all neighbors have voted, the ballot reaches a terminal state in finite steps (under fairness)
  • Early rejection correctness: the max_ratio early-exit in evaluate_ballot — if the impossibility condition fires, verify it is genuinely impossible to reach threshold with remaining votes

The early rejection property is particularly worth checking in TLA+. It is a subtle arithmetic claim and the TLC counterexample finder is good at finding off-by-one errors in threshold logic.

Phase A3 — Topology election (stretch)

Model the k-nearest election. Simplify distance to an arbitrary total order (concrete distances are not the interesting part). Check:

  • Elected set has cardinality <= k at all times
  • Self is never in the elected neighbor set
  • After a module is lost, remaining modules re-elect within bounded steps (under fairness)

Deliverable

TLC checks all properties without violations. A short note per property describes any counterexample found during development and what it revealed about the protocol assumptions.

Track B — Isabelle / AutoCorres Refinement

Question: Do the C functions correctly implement their abstract specifications?

Tool: Isabelle/HOL + AutoCorres. Required components:

<l4v>/tools/autocorres/
<l4v>/tools/c-parser/
<isabelle>/

File layout:

docs/isabelle/
  ROOT                  -- Isabelle session definition
  EkkTypes.thy          -- shared type definitions and lemmas
  EkkHeartbeat.thy      -- heartbeat abstract spec + AutoCorres import + proofs
  EkkConsensus.thy      -- consensus abstract spec + AutoCorres import + proofs

How AutoCorres fits in

AutoCorres parses the C source (via the l4v C99 parser) and generates Isabelle definitions in a shallow monadic embedding. Each C function becomes an Isabelle constant. You then write an abstract spec in pure HOL — no pointers, no fixed-point arithmetic, no C types — and prove that the lifted constant refines it.

Phase B1 — Toolchain validation — DONE

Status: discharged. ekk_heartbeat_init_verif_ok (docs/isabelle/proofs/EkkHeartbeat.thy) proves that the AutoCorres-lifted ekk_heartbeat_init_verif returns EKK_OK — totally (\<lbrace> \<rbrace>!, so the neighbor-zeroing loop terminates and no heap guard fails) — given a non-NULL hb whose AnonStruct7' and all 0x40 neighbor AnonStruct6' slots are valid, and a non-zero module id (uint my_id \<noteq> 0, i.e. my_id \<noteq> EKK_INVALID_MODULE_ID):

lemma ekk_heartbeat_init_verif_ok:
  "\<lbrace> \<lambda>s. hb \<noteq> NULL \<and> uint my_id \<noteq> 0 \<and> is_valid_AnonStruct7' s hb \<and>
         (\<forall>k::32 word. k < 0x40 \<longrightarrow>
            is_valid_AnonStruct6' s (\<dots> +\<^sub>p uint k)) \<rbrace>
   ekk_heartbeat_init_verif' hb my_id
   \<lbrace> \<lambda>r s. r = sint EKK_OK \<rbrace>!"

The postcondition itself is not interesting; the point is to confirm the C parser handles the ekk headers, AutoCorres generates sensible definitions, and — the one non-trivial part — that the 64-iteration zeroing loop is proved terminating with the invariant carrying exactly the per-slot validity the guards consume (measure 0x40 - i). No sorry, no quick_and_dirty (gated by scripts/check-no-sorry.sh).

Phase B2 — evaluate_ballot correctness — DONE

Status: discharged. ekk_consensus_eval_ballot_correct (docs/isabelle/proofs/EkkConsensus.thy) proves that the AutoCorres-lifted production function ekk_consensus_eval_ballot (single-sourced from src/ekk_consensus_eval.c) returns exactly eval_ballot_spec — totally, all guards discharged — under yes_votes <= eligible_voters, total_votes <= eligible_voters, eligible_voters <= 64, 0 <= threshold <= 65536. No sorry, no quick_and_dirty (gated by scripts/check-no-sorry.sh).

evaluate_ballot is the best early target for a real proof:

  • No loops
  • No aliasing or pointer arithmetic
  • No global state
  • Concrete correctness claim: APPROVED iff yes ratio meets threshold

Abstract spec in pure HOL:

fun eval_ballot :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ vote_result" where
  "eval_ballot yes total neighbors threshold =
     (if total < neighbors
      then
        let max_yes = yes + (neighbors - total) in
        if max_yes * 65536 < neighbors * threshold then Rejected
        else if yes * 65536 >= neighbors * threshold then Approved
        else Pending
      else
        if yes * 65536 >= neighbors * threshold then Approved
        else Rejected)"

The refinement proof must bridge the Q16.16 fixed-point arithmetic in the C code ((int64_t)yes_votes << 16) / neighbor_count) to the integer multiplication in the HOL spec. This is the hardest part and likely requires a supporting lemma about the equivalence of the two comparisons under the given bounds.

Phase B3 — Heartbeat state transitions — DONE

Status: discharged. Three lemmas in docs/isabelle/proofs/EkkHeartbeat.thy close the gap between the Track-A health machine and the C code:

  • health_step_valid_edge — the abstract health_step machine only ever moves along the allowed edges (valid_health_edge: UNKNOWN→ALIVE, ALIVE→SUSPECT→DEAD, SUSPECT/DEAD→ALIVE recovery, plus self-loops).
  • health_transition_valid_correct — the C validator health_transition_valid computes exactly that valid_health_edge relation (proved by case exhaustion over the four enum values); hence health_step_accepted: every abstract transition is accepted by the C validator.
  • set_neighbor_health_verif_sets_health — set_neighbor_health_verif writes exactly the health field of the addressed neighbor and nothing else (total, \<lbrace> \<rbrace>!).

Abstract spec (enum constructors are H-prefixed in the theory to avoid clashing with the lifted C constants):

datatype health = HUnknown | HAlive | HSuspect | HDead

fun health_step :: "health ⇒ nat ⇒ nat ⇒ health" where
  "health_step HAlive  missed timeout = (if missed ≥ timeout then HSuspect else HAlive)"
| "health_step HSuspect missed timeout = (if missed ≥ timeout then HDead   else HSuspect)"
| "health_step h       _      _       = h"

This is where the two tracks connect: the TLA+ safety property (no illegal transitions) is re-proven at the C level in Isabelle.

What is out of scope

  • ekk_module_tick — composes too many subsystems, too large for an early target
  • ekk_hal_posix.c — POSIX shim, not part of the interesting logic
  • ekk_topology distance sorting — numerical approximation, not correctness-critical
  • ekk_field gradient and decay arithmetic beyond monotonicity

Deliverable

A session that builds cleanly with:

<isabelle>/bin/isabelle build \
  -d <l4v> \
  -d docs/isabelle \
  EkkVerification

Checked theories for ekk_heartbeat_init, evaluate_ballot, and health_step refinement. Each theory states the abstract spec, imports the C via AutoCorres, and proves the refinement lemma.

Frama-C as an optional iteration tool

Frama-C / WP operates at the same level as Isabelle (C function correctness) but uses SMT solvers instead of interactive proof. It is faster to iterate on — write a contract, get feedback in seconds — but the result is weaker ("no counterexample found" vs "formally proved").

It is not a required stage. If Isabelle work stalls on a proof obligation, Frama-C can quickly tell whether the contract is plausibly true or obviously wrong, which saves time before re-entering Isabelle. The ACSL contracts also serve as precise documentation of intended function behavior.

Install if needed:

opam install frama-c alt-ergo

Relationship between the two tracks

Track A (TLA+)                     Track B (Isabelle)
─────────────────                  ──────────────────
Protocol properties                Function correctness
Distributed behavior               Sequential C code
Safety + liveness over time        Pre/post conditions + refinement
TLC finds counterexamples          Isabelle checks proofs

         ↕
Phase B3 connects them:
The TLA+ health transition safety property is re-proven
at the C level in Isabelle, closing the gap between
protocol intent and implementation.

What not to verify

  • ekk_hal_posix.c — POSIX shim, not part of the interesting logic
  • ekk_module_tick() as a unit — verify the functions it calls instead
  • The examples in examples/ — test scaffolding, not logic
  • Gradient and distance arithmetic beyond sign and monotonicity