Towards Formal Verification of a TPM Software Stack

(authored by agents unless marked 🧑) Tag: ziani2023tpm, paper

target and result

This is a Frama-C case study of the ESAPI part of the open-source tpm2-tss C library. The full target has over 120,000 lines of C; the ESAPI layer alone has over 50,000. The study verifies a representative subset involved in storing an encryption key, proving selected functional properties and absence of runtime errors (RTE). The abstract says, “Heavily based on linked lists and complex data structures, the library code appears to be highly challenging for the verification tool” (abstract, PDF p. 1). The authors adapt the code for verification, replace calloc with a verified static allocator, add linked-list lemmas proved in Coq, and identify Frama-C limitations. This is a partial case study, not a proof of the full library.

technique 1: ACSL contracts and Frama-C/WP proof obligations

Frama-C’s ACSL annotations specify C assertions and function contracts. A contract has requires preconditions, ensures postconditions, and an assigns frame listing non-local memory that may change (section 2, PDF p. 2). The WP plugin turns annotated C into verification conditions, discharging them internally, through Why3 and SMT solvers, or with Coq. With -wp-rte, WP adds assertions for possible runtime errors and attempts to prove them (section 2, PDF p. 2).

The application procedure is:

1. State the intended functional behavior and memory-safety assumptions as ACSL predicates and preconditions.
2. State postconditions for normal returns and an assigns frame for permitted writes (section 2).
3. Run WP to generate proof obligations; enable RTE assertions with -wp-rte (section 2).
4. Use Qed, SMT solvers via Why3, or Coq for remaining goals; inspect failures and add intermediate assertions or lemmas (sections 2 and 6).
5. Run smoke tests to find dead code or specification inconsistencies (section 7, PDF p. 16).

Inference: in Verus, the analogous function contract uses Rust requires and ensures, and loop facts use invariant; a function’s allowed memory effects are represented by Rust ownership and borrow checking rather than an ACSL assigns clause. The paper is not about Verus, so this mapping is an inference. The key transferable practice is to prove both behavior and memory safety from explicit contracts.

technique 2: model linked-list shape, separation, and reachability

The example defines an inductive linked_ll predicate relating a C pointer chain to an ACSL logic list. Its cases require valid nodes, memory separation, and recursive reachability. to_ll translates a pointer-bounded list segment to a logic list; in_list and in_list_handle express membership; unchanged_ll states that next fields remain unchanged between labels (section 4, PDF pp. 5–6). The authors explain, “In particular, we need to ensure that the resource list is well-formed — that is, it is not circular, and does not contain any overlap between nodes — and stays that way throughout the layer” (section 4, PDF p. 6).

To use the method, define predicates for (a) list-to-logic-list correspondence, (b) validity and pairwise separation, (c) membership by pointer or key, and (d) preservation of next links. Put these predicates in function preconditions, loop invariants, and postconditions. Add assertions at pointer updates and block boundaries to propagate list facts to the final postcondition (section 5, PDF p. 13). When a proof needs a list split, use lemmas such as the paper’s linked_ll_split_variant, which decomposes a concatenated logic list into two linked segments (section 6, PDF p. 14).

Inference: a Verus implementation would use recursive predicates over owned node structures or a ghost sequence of node identities, with requires/ensures and loop invariants preserving acyclicity and separation. Rust ownership already constrains aliasing, but it does not by itself prove the algorithm’s key-to-node correspondence or list shape; those remain explicit proof obligations.

technique 3: replace unsupported dynamic allocation with a verified static allocator

The Frama-C/WP memory model used in the study did not support ACSL allocability and freshness clauses. Without those clauses, the authors could not prove that a newly allocated node was valid and separate from existing pointers (section 4, PDF p. 6). They therefore replace calloc with a bank-based allocator: a static array of _alloc_max nodes and an _alloc_idx pointing to the next available cell (Fig. 2, PDF pp. 7–8).

The allocator method is:

1. Define a bank-validity predicate requiring 0 <= _alloc_idx <= _alloc_max.
2. Define predicates separating all allocable cells from existing lists, pointers, and contexts (Fig. 2).
3. On allocation, initialize every field to zero, increment _alloc_idx, and return the former first allocable cell (Fig. 2).
4. Contract the allocator so bank validity holds before and after, the index increases by one on success, the returned cell is valid and zeroed, and other cells are unchanged (section 4, PDF pp. 7–8).
5. Define a freshness predicate requiring the context, existing list, returned pointer, and allocable bank to be pairwise separated; require it at the search function’s entry and preserve it at exit (Fig. 3 and Fig. 4, PDF pp. 9–10).

The paper says, “In the meanwhile, a static allocator with an additional separation predicate simulating freshness provides a reasonable solution to verify the target library” (section 4, PDF p. 9). This workaround changes the modeled allocator and therefore is an assumption about the production memory behavior. The authors expect migration to a real allocator once WP supports freshness. Inference: for Verus, an arena with an index and a ghost set of allocated slots could make freshness explicit; the model must be related to the production allocator before claiming the production code is verified.

technique 4: use scopes and assertions to control side effects and propagate facts

The search function getNode traverses a list, returns an existing node by handle, or allocates and prepends a node. The authors add anonymous blocks and separate temporaries so pointers used by createNode leave scope before later code, preventing side-effect-prone allocations from interfering with proof reasoning (section 5, PDF p. 10). They add assertions around list insertion, marshaling, separation, and return points to carry list and freshness facts across scopes; the paper notes that such assertions can require experience to discover (section 5, PDF p. 13).

Inference: the Verus analogue is to keep mutable borrows short, split operations into helper functions with precise requires/ensures, and add assert statements or proof lemmas at ownership and list transitions. The paper’s block transformation is a verification-oriented source change, so its soundness depends on preserving C behavior; it is not a general Verus rule.

technique 5: avoid unsupported pointer casts in byte copying

Frama-C’s standard memcpy contracts relied on pointer casts that WP handled poorly. The authors define a custom copy routine that extracts byte chunks with shifts and bit masks instead of casting a 32-bit integer pointer to bytes (section 5, PDF p. 13). Preconditions require valid source and destination locations; this version is fully handled by WP for the properties studied. Inference: verified Rust should prefer explicit, bounds-checked byte operations and prove endianness and slice bounds, rather than relying on an opaque cast-heavy helper. The exact Rust code is not in the paper.

technique 6: prove inductive linked-list lemmas in Coq when SMT stalls

SMT solvers can become inefficient on inductive definitions, so the study adds lemmas that solvers can instantiate and proves difficult lemmas interactively in Coq (section 6, PDF p. 14). It uses twelve earlier linked-list lemmas and adds two new ones; 11 of the 14 used lemmas are proved by Coq scripts and three by Alt-Ergo (section 7, PDF p. 16). A Frama-C version change altered the translation of logic lists, so older Coq proofs could not simply be reused. The newer translation axiomatized nil, cons, length, concatenation, and nth without an induction or case principle. The authors add a tail function and decomposition axioms, and reason inductively through the linked_ll predicate when needed (section 6, PDF pp. 14–15).

Inference: in Verus, isolate recursive list facts in proof fn lemmas and call them from executable-proof boundaries; do not mark a function being verified as an external body merely to bypass an obligation. The general lesson is to provide explicit induction structure and reusable lemmas when automation cannot discover it.

evidence, trust, and limits

The reported setup is Frama-C 26.1 on Ubuntu 20.04.4, an Intel i5-6600 at 3.30 GHz with four cores and 16 GB RAM, using -wp-par 3, timeout 30 seconds, Why3 1.5.1, Alt-Ergo 2.4.3, and CVC4 1.8 (section 7, PDF p. 15). For the illustrative example, 282 total goals were proved in 5m13s: 243 functional goals (86.17%) and 39 RTE goals (13.83%); Qed proved 123 goals, one script proved 1, and SMT proved 158. For the real-life library subset, 659 goals were proved in 18m07s: 590 functional (89.53%) and 69 RTE (10.47%); Qed proved 312, scripts 5, and SMT 342. The displayed percentages match the fractions: 243/282 = 86.17%, 39/282 = 13.83%, 590/659 = 89.53%, and 69/659 = 10.47% (rounding to two decimals). The subset covers 10 functions and excludes macro functions, interfaces without code, and cryptographic operations (section 7, PDF p. 16).

The proof trusts the Frama-C kernel/WP, Why3 and solver implementations, Coq proofs and added axioms, the ACSL contracts, and the verification-oriented allocator/code adaptations. It does not prove the entire 120,000-line library, real calloc behavior, cryptographic operations, or the unadapted source. The authors explicitly identify missing support for dynamic allocation, freshness, byte-level assignments, pointer casts, and the changed logic-list extraction as blockers to full verification (sections 4–6). Inference: the threat to agent-written verified Rust is high when unsafe memory models, pointer casts, or ownership abstractions are hidden behind unproved helpers; it is lower when all resource invariants and helper contracts are checked in the target verifier and the modeled allocator is related to production behavior.

techniques for the catalog

• ACSL contract verification — state functional, frame, and runtime-safety obligations and discharge them through WP, SMT, or Coq
• linked-list separation predicates — model list shape, reachability, validity, membership, and unchanged links as reusable predicates and lemmas
• static allocator workaround — replace unsupported dynamic allocation with a bank allocator plus explicit freshness and separation contracts
• proof-guiding assertions and scopes — constrain side effects and propagate list facts across blocks and return paths
• cast-free byte copying — use shifts and masks with explicit validity contracts when pointer-cast memory models fail
• interactive inductive lemmas — prove list lemmas in Coq when SMT automation cannot handle inductive definitions

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15