Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Verifying Safe Clients of Unsafe Code and Trait Implementations in Rust

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

scope and result

This is a Master’s thesis (Jakob Beckmann, ETH ZĂŒrich, 28 September 2020). It extends Prusti so that clients of unsafe Rust abstractions can be checked. Its techniques cover unsafe trait contracts, marker-trait invariants, and encodings for interior-mutability wrappers. The motivating problem is stated in the Chapter 1 introduction: “unsafe Rust relaxes some guarantees on which Prusti relies, making Prusti unsound for verifying some programs containing unsafe code” (p. 1). The contribution list says that “Trait annotations allow to attach verifiable meaning to marker traits” and that the work adds “Complete solutions able to handle various common cases of interior mutability” (Section 1.2, p. 3).

Implementation status differs by chapter. Chapter 3 (traits) is described as “a prototype implementation” (Section 3.6, p. 36), and trait scoping is not implemented in it (Section 3.4.1.1, p. 27). Chapter 4 (interior mutability) is a design: “the author did not implement the approach” (Chapter 4 intro, p. 37). Chapter 5 (contract derivation) is called “a theoretical solution” (Section 1.3, p. 4).

unsafe trait method contracts

Use this when a trait method’s behavior is the condition that makes implementing the trait safe. The paper’s Searcher example requires every returned range to be on UTF–8 boundaries. The paper states: “the implementation of lib_print_next() is only safe if the Searcher trait adheres to always returning valid UTF–8 boundaries for the haystack” (Section 3.1, p. 20).

Steps from the paper:

  1. Mark the trait declaration and implementation unsafe, documenting the semantic obligation. Rust recommends marking such a trait unsafe, and “when a trait declaration is marked unsafe, any implementer of the trait needs to mark the implementation as unsafe as well” (Section 3.1, p. 20).
  2. Express the obligation as a method postcondition. Listing 3.4 matches SearchStep::Match(start,end) and requires is_on_utf8_boundary(haystack,start) && is_on_utf8_boundary(haystack,end), assuming a static pure function is_on_utf8_boundary() exists (Section 3.3, p. 23).
  3. Verify each implementation against that postcondition. The paper says this is “quite simple, as the main goal of Prusti is to verify pre- and postconditions” and that unsafe traits “are treated like normal traits” (Sections 3.3 and 3.5.1, pp. 23 and 33). The paper’s WrongSearch returns SearchStep::Match(0, 1), is accepted by rustc, and breaks the documented contract (Listing 3.3, p. 21). Inference: such an implementation would fail the postcondition in step 2; the thesis does not show a Prusti run on it.

Verus form (Inference): encode the boundary predicate as a spec fn, put the result condition in ensures, and prove each unsafe fn or unsafe-trait implementation’s postcondition. A Rust trait and its impl remain executable; the proof obligation is attached to the method contract. The Prusti annotation syntax in Listing 3.4 does not carry over verbatim.

Evidence and limits: the thesis says unsafe-trait support “includes normal and marker unsafe traits” (Section 1.2, p. 3), but gives no aggregate count of verified unsafe implementations. Section 3.5.1 says Searcher “can be fully verified with a contract similar to the one presented in Listing 3.4” (p. 33) without showing a run. The contract is trusted as a specification: a proof shows compliance with the written boundary predicate, not that the predicate captures every UTF–8 safety condition. The thesis also warns that “many properties that are easily expressed in plain text in the documentation can be quite hard to state as Rust expressions” and that, from the author’s experience, this “affects a significant share of unsafe traits”, without a quantitative investigation (Section 3.6, p. 36).

marker-trait invariants and contract refinement

Use a marker trait when its meaning is semantic and has no executable method, such as Eq implying reflexivity. The paper’s example is #[invariant="self.eq(&self)"] pub trait Eq: PartialEq<Self> {} (Listing 3.6, p. 26), and it explains that “any type implementing the trait obtains the invariant” (Section 3.4.1.1, p. 26). Eq is a safe marker trait (Section 3.4, p. 24); the same mechanism applies to unsafe marker traits (Section 3.5.2, p. 33).

Steps from the paper:

  1. State the behavioral meaning as a trait invariant or refined method contract. A trait invariant applies to every implementing type and “allow for far more flexibility in their expressions, such as referencing private fields on the implementing type, and referencing methods unknown to exist at the trait level” (Section 3.4.1.1, p. 25). Prusti type-checks it on each implementing type by generating code on the type (Listing 3.11, Section 3.4.1.2, pp. 28–29). Multiple trait invariants are joined by conjunction (p. 27).
  2. Import the trait where clients rely on it. The design says “when a trait is in scope, all its invariants apply to all types that implement the trait” (Listing 3.9, p. 27), while an out-of-scope client cannot use the invariant (Listing 3.8, p. 27). The paper says call-site checking of in-scope invariants is “very complex” and “scoping is not implemented in the prototype” (p. 27); the same holds for contract refinement (Section 3.4.2.2, p. 32).
  3. Contract refinement is the alternative when a marker trait changes the contract of a method of a super-trait, as TrustedLen does for Iterator::size_hint. It uses the new attributes #[refine_requires] and #[refine_ensures] (Listing 3.12, Section 3.4.2.1, p. 31). A refinement “is joined with the original contract via implication for preconditions, and conjunction for postconditions” (p. 31). The paper notes that the Listing 3.12 contract “does not remove the unsafety from the trait implementation, as the provided contract does not ensure the returned size hint is correct” (p. 31).

Verus form (Inference): use a trait-associated specification or a predicate over Self, then require that predicate at functions relying on the marker semantics. Verus does not use Prusti’s string attributes; write requires/ensures and proof lemmas with supported Verus syntax. Scope-sensitive imports are a design issue: an API should make the predicate available explicitly rather than silently assuming it.

The paper’s reason for adding these annotations is concrete: they “allow reliance on their informally stated contract during verification” and “ensure only types actually adhering to the contract of the trait can implement them” (Section 3.4, p. 25). The assumption remains that the annotation faithfully formalizes the documentation. Quantified invariants such as reflexivity over all values of Self are not supported; Section 6.1.3 says “a quantified expression such as the one shown in Listing 6.1 would be more adequate” than Listing 3.6 (p. 92).

interior mutability: state-machine and rely/guarantee encodings

Use these encodings for Mutex, RwLock, RefCell, or Cell, where Rust permits mutation through a shared reference. The unsound baseline is the Cell example: getter is marked pure and trusted, foo calls cell.set(5), and assert!(v1 == v2) verifies although it fails at runtime (Listing 1.2, p. 2; Listing 4.3, p. 39). The paper explains why: “Rust’s std::cell::UnsafeCell is the only type allowing safe modification via shared references” (Section 4.1, p. 37).

Steps from the paper:

  1. Do not verify UnsafeCell itself; the thesis says direct handling “uses unsafe code; its verification is out of scope for this thesis” (Section 4.3, p. 40).
  2. Choose an abstraction-specific encoding in Viper. For Mutex there are two encodings (Section 4.3.1, pp. 42–56). The first is a two-state machine after Concurrent Abstract Predicates: abstract predicates Mutex and Locked, with lock and unlock as abstract methods (Sections 4.3.1.3–4.3.1.4, pp. 44–51). The second uses a lock-capability predicate CanLock and a magic wand for the returned reference (Section 4.3.1.5, pp. 51–55). Rely/guarantee (Section 4.3.3, pp. 57–63) is a further layer: the paper describes “a rely/guarantee mechanism complementing the second solution” (p. 42).
  3. First encoding: Listing 4.10 gives lock the contract requires acc(Mutex(mutex), read()), ensures acc(Mutex(mutex), read()) and ensures acc(Locked(mutex), write), with the invariant inside Locked (Section 4.3.1.4, p. 51). The paper admits that Viper lets this encoding verify a double lock (Listing 4.11, p. 52). Second encoding: lock requires write permission to CanLock and returns write permission to the data plus a wand back to CanLock (Listing 4.13, p. 54); releasing the guard is apply of that wand (Listing 4.14, p. 54); the invariant is put in the lock() contract (Listing 4.15, p. 55). The paper notes it “does not indeed perform a verification on whether the program is deadlock free”: “Thus two threads can enter a deadlock by sharing two locks and trying to acquire both locks in opposite order” (p. 54).
  4. Rely/guarantee: the client works on a ghost copy of the protected value and calls an interference method before locking and after release, with ensures old(get_inner(dummy)) <= get_inner(dummy) for a monotone counter (Listings 4.21–4.22, pp. 61–62). The Rust-level specification of rely/guarantee is left open: it is “very difficult to formally define on a conceptual level”, Prusti has no support for concurrency, and the guarantee function can be called by only one thread (Section 4.3.3.1, pp. 61–63).
  5. RwLock “can be encoded in the same way” as Mutex; read() takes only a read permission to CanLock (Section 4.3.4, p. 63). RefCell and Cell use a user-declared state machine: #[state="Name => invariant"] and #[transition="From => To"] attributes (Section 4.3.5, pp. 64–65), a CanBorrowMut predicate against double mutable borrows (Listing 4.25, p. 65), and optional implicit transition tracking (Section 4.3.5.3, pp. 67–70). Cell encodes set, replace and swap as an exhale of the source state and an inhale of the target state (Section 4.3.6, p. 72).

Verus form (Inference): model the wrapper with a ghost state-machine predicate and explicit permission predicates; use requires/ensures on lock, borrow, set, and guard-drop operations. For concurrent locks, Verus transition systems can represent allowed lock transitions, while executable Rust remains the wrapper implementation. Do not mark a mutating accessor pure; instead expose a spec view whose relation to the concrete state is proved.

Evidence: the thesis presents “Two Viper encodings” for Mutex, “one backed by a state machine ensuring simple invariants, the other uses a rely/guarantee mechanism to support more detailed verification, at the cost of complexity” (Section 1.2, p. 3). It gives hand-written Viper listings and states that examples verify, such as Listing 4.16 (p. 55, a Mutex client whose caption says it “can be verified using the first Viper encoding”) and Listing C.1 for a stateful RefCell. Chapter 4 is not implemented in Prusti (p. 37), so Inference: these verification claims were not shown by a tool run in the thesis. No whole-library soundness theorem or benchmark denominator is supplied. Section 6.1.2 says the missing concurrency support in Prusti “makes the presented solution for Mutex and RwLock not very useful in practice” (p. 92). Atomic types are not addressed (Section 6.1.1, p. 91). The encodings assume the wrapper implementation and atomic operations satisfy their modeled transitions; foreign code, scheduler behavior, and the correctness of Viper/Prusti remain trusted. Section 4.4 lists identifier handling, error reporting and specification-stability challenges for implementation (pp. 72–73).

derived contracts and operator snapshots

Use contract derivation when Rust generates standard trait implementations through #[derive], because the verifier otherwise cannot use their semantics. The paper’s example is #[derive(PartialEq, Eq)] struct Dummy { inner: i32 } (Listing 5.1, p. 75). Its stated goal is “to showcase a solution enabling Prusti to derive a contract for the implementation provided by the compiler” (Chapter 5, p. 75).

Steps from Sections 5.2–5.3:

  1. Identify a derivable trait and derive its contract from the documented behavior. For PartialEq the documentation says that on structs “two instances are equal if all fields are equal” (Section 5.1, p. 75). Current Prusti already derives PartialEq only if the implementation and all transitively contained types derive it (Section 5.3.2, p. 82).
  2. Handle each trait by its own rule. Eq and Copy are marker traits, so “there is never any work to do when deriving the trait” beyond the trait invariant (Section 5.3.3, p. 84; Section 5.3.8, p. 88). PartialOrd needs axioms for a lexicographic ordering (Section 5.3.4, p. 84). Ord is the same without the Option wrapper (Section 5.3.5, p. 84). Default is built recursively from field contracts (Section 5.3.6, p. 86). Clone tries three cases in order (type implements Eq; derivable PartialEq; per-field contracts) (Section 5.3.7, pp. 87–88). Hash is not solved (Section 5.3.9, p. 89).
  3. For overloaded operators, encode the operation as an abstract domain function and axioms. Prusti creates a bijection between the concrete type encoding and a domain “snapshot”; snapshot equality compares the values themselves, whereas reference comparison checks whether they point to the same object (Section 5.3.1, p. 78; Listing 5.4, p. 79).
  4. Use the derived contract in client proofs. For a manual PartialEq, snapshot equality is not sound, so the thesis introduces a separate eq() domain function whose axiom is extracted from the body of the manual implementation (Section 5.3.2, pp. 82–83). The paper notes that “extracting only the logic from the implementation can be extremely challenging” (Section 5.3.1, p. 81).

Verus form (Inference): define a spec fn view of a type and prove derived PartialEq, ordering, Clone, or Default implementations against that view. For overloaded operators, specify the trait method directly with ensures; a ghost snapshot can represent the abstract value. Rust #[derive] expansion is executable code, so the contract must be proved for the generated implementation or supplied by a trusted standard-library specification.

Evidence and limits: the thesis says solutions were presented “for the majority of Rust’s standard library derivable traits” (Chapter 6, p. 90) and reports no quantitative coverage. Performance was tested only on synthetic examples; operators returning a new snapshot, such as addition, “seemed to lead to significant performance drops in verification” (Section 5.3.1, p. 81). The domain encoding requires operator implementations to be “pure” (Section 5.4, p. 89). The Eq solution “does assume, that the standard library defines a valid trait invariant on the Eq trait, or that the contract is somehow injected” (Section 5.3.3, p. 84). Inference: the snapshot axioms and generated-code correspondence remain trust boundaries.

what VL should reuse and threat

Inference: VL should reuse the separation between executable state and ghost permissions, the explicit unsafe-trait postcondition, and state-machine modeling of lock protocols. It should not redo the observation that a trusted pure accessor over interior mutability is unsound; Listing 1.2 is already a minimal counterexample. Agent-written verified Rust is threatened whenever an unsafe dependency’s semantic trait contract or interior-mutability behavior is left as documentation or an external_body assumption; a proof can then establish a false abstraction. This thesis addresses the specification pattern, but not complete verification of arbitrary unsafe implementations: “verification of unsafe Rust code” is listed as future work (Section 6.1.4, p. 93).

techniques for the catalog

  • unsafe-trait postconditions — express the safety obligation of each unsafe method as a checked postcondition
  • marker-trait invariants — attach semantic predicates to otherwise empty traits and require them at clients
  • trait contract refinement — add postconditions to a super-trait method through a marker trait
  • mutex state-machine encoding — model lock transitions and permissions with abstract predicates
  • lock capability with magic wand — return the protected data with a wand that restores the lock capability on release
  • rely/guarantee lock encoding — separate protected-data guarantees from interference by other threads
  • interior-mutability state machines — declare states with invariants and legal transitions for Cell and RefCell; RwLock reuses the lock encoding with read permissions
  • derived trait contracts — infer standardized contracts for #[derive] implementations and overloaded operators via abstract snapshots Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Thus two threads can enter a deadlock by sharing two locks and trying to acquire both locks in opposite order.”): I read the whole text (chapters 1-6, appendices, bibliography) and compared every quotation, page and section reference, listing number and technique step; the tag (author Beckmann, year 2020) is right, and the link is from the fetch record because the paper text gives no DOI or arXiv link. Changes: fixed the Listing 4.16 page (p. 55, not 60) and the Listing 4.10 page (p. 51, not 52); corrected the Section 1.2 pages for the unsafe-trait and contribution quotes (p. 3); the opening quote is from the Chapter 1 introduction, not Section 1.1; the two Mutex encodings were mis-described (second is CanLock plus magic wand, rely/guarantee is Section 4.3.3 and complements it); added implementation status (Chapter 3 prototype without scoping, Chapter 4 not implemented, Chapter 5 theoretical); moved the Section 3.6 quote from derived contracts to unsafe traits; rewrote the marker-trait step 3 (it was not in the paper as stated) around contract refinement; fixed the RwLock, RefCell and Cell descriptions; changed UTF-8 to the paper’s UTF–8 inside quotes; labeled own conclusions “Inference:”. Not checked: the Verus-form paragraphs (my own mapping, not verified against Verus), the cited external sources, and Viper/Prusti behavior beyond what the thesis states.

Last edited: