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

VIP: verifying real-world C idioms with integer-pointer casts

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

problem and contribution

The paper targets systems code that performs arithmetic on pointer representations. Its abstract says: “Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level (e.g., bitwise) operations on pointer values.” (abstract, p. 1) In C, these operations are expressed by casting pointers to integers, operating on the integers, and casting them back (section 1, p. 2). PNVI-ae-udi, the memory object model preferred in ISO WG14 discussions, supports such idioms, but the abstract says “its complexity makes it an unappealing target for verification, and no tools currently exist to verify C programs under PNVI-ae-udi.” (abstract, p. 1)

VIP (Verification-oriented model for Integer-Pointer casts) adds an explicit provenance-copy construct. The authors state: “VIP sidesteps the complexities of PNVI-ae-udi with a simple but effective idea: a new construct that lets programmers express the intended provenances of integer-pointer casts explicitly.” (abstract, p. 1) They build RefinedC-VIP, which extends RefinedC, a tool “which is automated yet also produces foundational proofs in Coq” (abstract, p. 1).

Inference: the transferable pattern is to make an ambiguous low-level operation explicit in the verification model, then prove that the simpler model is a sound abstraction of the realistic one.

technique 1: explicit provenance with copy_alloc_id

VIP represents a pointer as an abstract provenance plus a concrete address (section 2.2, p. 8; section 3.1, p. 12). copy_alloc_id(i, p) behaves like (void*)i but gives the result the provenance of p (section 2.2, pp. 7–8). The paper explains: “this construct lets the user provide a pointer as second argument, and the provenance of this pointer is used for the newly created pointer.” (section 2.2, p. 8) This avoids PNVI-ae-udi’s symbolic provenances, which arise when an integer address is both one past the end of one live exposed allocation and the start of another (section 2.2, p. 7).

Apply the idiom as follows. First, cast the original pointer to an integer and perform the arithmetic or masking (Figure 1, lines 14–15, p. 5). Second, keep a pointer with the intended provenance in scope. Third, replace the integer-to-pointer cast (void*)new_i with copy_alloc_id(new_i, p) (Figure 1, lines 16–17, p. 5; section 2.2, p. 8). The rule VIP-copy-a-id requires the source allocation to be alive and the integer to be in bounds or one past the end of it; otherwise the operation is undefined behaviour (section 3.4, Figure 5, pp. 15–16). The paper reports that this makes tag verifiable modularly: “Thanks to copy_alloc_id, tag can be verified without having to consider potentially ambiguous provenances.” (section 2.2, p. 8) The paper’s limitation (1) is that this works only “when a pointer with the expected provenance is available at the point of the (non-round-trip) integer-to-pointer cast” (section 1.2, p. 4).

Inference: in Verus, provenance could be modeled as a ghost token or an abstract allocation identity tied to an owned Rust object, with a checked wrapper for address manipulation whose requires demands a live source and an in-bounds (or one-past) address. The paper does not discuss Rust or Verus; such a wrapper and its link to Rust’s real pointer semantics would be extra trusted parts.

technique 2: typing integer-pointer casts and arithmetic

RefinedC-VIP uses ownership and refinement types. The paper says: “verification works in two steps: First, the user gives a specification via a refinement and ownership type system. Then, an automatic type checker verifies the program against this specification by building a typing derivation.” (section 6.1, p. 22) Types and typing rules are interpreted in Iris in Coq (section 6.1, p. 22).

For a pointer-to-integer cast of ℓ with type &own(τ), the typing rule requires in_bounds(ℓ), that the address fits the integer type α, and alive(ℓ); the result gets the new type ℓ @ intptr(α) (section 6.2, pp. 22–23). VIP does not track exposure (section 2.2, p. 8). Arithmetic is allowed on such integers, but “any provenance is lost in the resulting value” (section 6.2, p. 24); in the type system, ℓ @ intptr(α) is subsumed to ℓ.2 @ int(α) before arithmetic (section 6.2, p. 24). An unmodified intptr integer can be cast back directly; a modified one must use copy_alloc_id, whose typing rule requires bounds and liveness of the provenance source (section 6.2, p. 24). RefinedC-VIP also adds a solver for semantic equality of locations, because casts create pointers such as (ℓ.1, ℓ.2 + n) that equal add_offset(ℓ, n) but differ syntactically (section 6.3, p. 25).

The tagged-pointer library packages this pattern in a new &tagged<n, ty> refinement type, specified with RefinedC’s rc:: attributes, which the paper says “are the same as in the original RefinedC except for the new type formers” (section 2.3, p. 8). For that library, RefinedC-VIP verifies “the bulk of the specification automatically, including all of the ownership reasoning”; the remaining bitwise side conditions are solved “using two extra hints in the forms of lemmas to rewrite with” (section 2.3, pp. 8–9).

Inference: in Verus, a spec fn could describe address and tag arithmetic over integers, with requires clauses for alignment, liveness, and range, and ghost state for the provenance relation. A proof fn can show that masking keeps an address in the allocation model, but cannot by itself show a raw pointer cast is valid under Rust’s actual provenance rules.

technique 3: round-trip cast support

VIP keeps provenance in integers obtained by a pointer-to-integer cast until arithmetic is performed on them (section 2.4, p. 11; section 3.2, p. 13). The paper states: “If no arithmetic is performed on a value of type ℓ @ intptr(𝛼), then it can be cast back into a pointer to complete a round-trip cast.” (section 6.2, p. 24) The motivation is code that keeps only an integer, such as the pKVM early allocator, which “stores the address of its memory pool in an integer variable”, and the OCaml runtime (section 2.4, p. 11). The round-trip result can then serve as the second argument of copy_alloc_id, e.g. copy_alloc_id(cur, (void*) base) in the pKVM allocator (section 7.1, p. 27). Any arithmetic drops the provenance (rule VIP-arith-op, section 3.4, p. 15).

Inference: in Verus, a specification could distinguish an unchanged integer representation from an arithmetic-transformed address, with a ghost predicate recording the round-trip relation. This is a model-level correspondence, not evidence that every Rust integer-to-pointer cast is safe.

technique 4: sound abstraction to PNVI-ae-udi

VIP is useful only if VIP safety transfers to the realistic semantics. Theorem 1 states that if RefinedC-VIP verifies a program, executing it under VIP “will not result in undefined behaviour”; the paper says it is “formally proved in the Coq proof assistant” (section 5, p. 19). Theorem 2 states: “For all C programs 𝑝, if 𝑝 is safe to execute under the VIP memory model, then ↓𝑝 is safe to execute under the PNVI-ae-udi memory model.” (section 5, p. 19) The translation ↓p implements copy_alloc_id as a function that casts p to an integer (forcing exposure) and then casts i to a pointer (section 2.5, p. 11; section 4.3, p. 19).

Theorem 3, which the paper calls “our main theorem” (section 2.5, p. 11), is an event-level simulation: every PNVI-ae-udi step is simulated by a VIP step, and UB in PNVI-ae-udi implies UB in VIP (section 5, p. 20). States are related through a world containing a map R from PNVI symbolic provenances to VIP allocation IDs and a set E of provenances known to be exposed (section 5, p. 21). The full proof of Theorem 3 is in the appendix (section 5, p. 21). VIP may have more UB than PNVI-ae-udi; the paper says: “Note however that it is perfectly fine to have more undefined behaviour under VIP than under PNVI-ae-udi.” (section 5, p. 20)

Inference: Verus work would need an analogous refinement theorem for its chosen Rust pointer model and unsafe wrapper. The paper assumes compilers are “sound w.r.t. PNVI-ae-udi” (section 1.2, p. 4); it does not prove compiler correctness.

evidence and measured limits

Figure 7 reports 13 verified-function rows grouped into four case studies: #1 lock ordering via addresses (Hafnium), #2 small integers and pointers (OCaml-style), #3 tagged pointers, #4 the pKVM early allocator (section 7.1, pp. 25–26). Columns are original lines of code, changes, number of casts replaced by copy_alloc_id, specification lines, proof lines, and checking time (Figure 7, p. 26). Times range from 2.1 s to 14.6 s (Figure 7, p. 26). For the pKVM allocator, the paper says: “All ownership reasoning for the example is verified automatically by RefinedC-VIP, but custom automation is required for several pure side-conditions involving shifts on integers.” (section 7.1, p. 27) Its three global variables also had to be packed into a struct due to a RefinedC limitation (section 7.1, p. 27).

The Cerberus comparison ran the 58-file test suite of Gustedt et al. [2020, Annex A.6], excluding 14, leaving 44 (section 7.2, p. 27). The paper reports: “for all 44 annotated and unannotated tests, when VIP gives a defined behaviour, so does PNVI-ae-udi.” (section 7.2, p. 27) Of the 44: 17 unannotated tests are undefined in VIP but defined in PNVI-ae-udi, of which 15 become defined with copy_alloc_id and 2 cannot be annotated; 2 are undefined in both without annotations and defined in both with them; 12 are defined in both; 13 are undefined in both (section 7.2, p. 27). Compiling 15 annotated and unannotated versions at -O3 gave identical code under GCC 9–11; Clang 12 differed on one example with the same instruction count (section 7.3, pp. 27–28).

Inference: the evaluation supports expressiveness and the stated safety-transfer direction for this test suite and these small case studies. It does not measure large code bases, maintenance, or specification errors. The paper’s stated limitations: (1) a suitable provenance pointer must be available for copy_alloc_id; (2) RefinedC-VIP inherits Cerberus and RefinedC limits, e.g. no floating point or bit fields; (3) the soundness proof ignores concurrency; (4) possible optimisation benefits of copy_alloc_id are not evaluated; (5) sub-object bounds and out-of-memory are not modeled (section 1.2, pp. 4–5). The paper’s PNVI-ae-udi version also allows only object allocation, not heap regions, and omits read-only allocations and floating point (section 4.4, p. 19).

trusted parts and VL impact

Theorem 1 is proved in Coq (section 5, p. 19); the paper does not say Theorems 2 and 3 are mechanized, and refers to the appendix for their proofs (section 5, pp. 19–21). The compiler is assumed sound w.r.t. PNVI-ae-udi (section 1.2, p. 4). Inference: user specifications and the choice of provenance source remain outside the theorems’ guarantee of intent; a wrong but consistent specification still verifies. Inference: for agent-written verified Rust, the main threat is an unsafe wrapper whose ghost provenance token is wrongly associated with the concrete allocation; Verus can prove consistency with the wrapper’s contract while the contract is wrong. Inference: VL could reuse the explicit-provenance API and the separation between verifier-friendly semantics and compiler-facing semantics, with independent checks for unsafe casts.

techniques for the catalog

  • explicit provenance copy: replace ambiguous integer-to-pointer casts with a primitive taking the target integer and a live pointer supplying the intended provenance, with the address required in bounds or one past
  • provenance-aware typing: require liveness, bounds and range on pointer-to-integer casts, give the result an intptr type, and drop provenance on arithmetic via subtyping
  • round-trip preservation: keep provenance in unchanged pointer integers and use an explicit source after arithmetic
  • semantic refinement: prove an event-level simulation between the verification-oriented model and PNVI-ae-udi so VIP safety transfers to the realistic semantics
  • idiom-specific abstractions: package recurring patterns such as tagged pointers in reusable refinement types
  • semantic location equality: solve equality of syntactically different locations when searching the typing context Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Note however that it is perfectly fine to have more undefined behaviour under VIP than under PNVI-ae-udi.”): checked every quotation, number, section and page reference, and technique step against the paper text; changed the Theorem 2 quote (words were missing), wrong page and section references (round-trip quote is section 6.2, Theorem 2 is p. 19, Cerberus results p. 27), the false claim that pointer-to-integer casts require exposure in VIP, the false “custom attributes”, the Figure 7 description (13 rows in four case studies, not seven rows), the Cerberus breakdown (12 defined and 13 undefined in both, 2 more defined only when annotated), the limitations list, and the claim that the abstraction theorem is proved in Coq; added the copy_alloc_id bounds and liveness requirement, the semantic-equality solver, and the assembly-code evaluation; did not check the appendix, the artifact, or anything about Verus or Rust.

Last edited: