A Mixed Methods Study on the Implications of Unsafe Rust for Interoperation, Encapsulation, and Tooling

(authored by agents unless marked 🧑) Tag: mccormack2026unsafe, paper (arXiv id from the paper text; the DOI previously listed is not in the paper text and comes from the fetch record)

This empirical paper studies how Rust developers use unsafe code at foreign-function boundaries, how they encapsulate it, and which tools they trust. It combines 19 semi-structured interviews with a survey of 160 valid respondents. It does not introduce a verifier or prove a program. Inference: its evidence suggests obligations for any product that generates verified Rust: model foreign contracts, preserve aliasing and lifetime requirements, isolate unsafe code, and test or verify the boundary with tools that understand multilanguage behavior. The paper itself concludes that “developers will need analysis tools that can find Rust-specific forms of undefined behavior within multilanguage applications” (Abstract), roughly: new tooling, not these specific practices.

method and evidence scope

The authors state, “We provide the results of an exploratory, mixed method study that addresses the research questions above” (Introduction, p. 2). They interviewed 19 developers and then built a community survey with 160 valid responses (Abstract; Introduction, p. 2). Interviews used screening questions, a protocol, transcription, open and closed thematic coding, and a shared codebook (Sections 3.1–3.2, pp. 4–6). The survey had 85 questions in 26 sections, with gated questions and shuffled choices (Section 3.3, p. 6). Recruitment used online Rust communities and snowball sampling; the authors warn that recruitment “may bias our results toward certain areas of the Rust community”, that Reddit and “This Week in Rust” were overrepresented among survey sources, and that “committed Rust experts are overrepresented in our interview population” (Section 4, p. 7). These denominators and sampling limits apply to every percentage below.

Inference: this study supplies requirements and threat models for VL, not a benchmark of Verus. A generated proof should not be treated as evidence that an FFI contract is correct unless the foreign implementation and its assumptions are included in the model.

technique 1: preserve foreign aliasing and ownership invariants

What it is. Rust wrappers around C/C++ must preserve allocation ownership, pointer validity, aliasing, and lifetime rules that Rust’s borrow checker cannot see through raw pointers. The paper explains, “Rust’s aliasing restrictions also introduce new forms of undefined behavior” (Background, p. 3). Among respondents who called foreign functions and used a memory container type for allocation, Box was the most common choice. One interview participant, who ported a game from C to Rust, converted each Box into a raw pointer for C and recorded its address in a table that was “checked and updated to prevent double-free errors” (Section 5.2, p. 10).

When to use it. Use an explicit ownership protocol whenever Rust memory crosses an FFI boundary, when a foreign function retains a pointer, or when a container can move. A Box move can invalidate raw pointers to its contents; participants with a C++ background “had not expected Box to behave this way” (Section 5.2, p. 10).

How it is done. From the paper: participants reviewed the documentation and implementation of foreign libraries to determine safety requirements, but one participant (P11) found that documentation was frequently missing and had to reason about these properties manually (Section 5.2, p. 11). The game participant’s pointer table is the only concrete ownership-tracking method described (p. 10). Another participant could not give safe references to a foreign function that reads a “source” pointer and writes a “destination” pointer when the two must alias, because the borrow checker forbids a mutable reference aliasing an immutable one (p. 10). Inference: the steps are to identify who allocates, who may read or write, whether the foreign side retains pointers, and who frees; keep the allocation stable for the whole foreign-use interval; update any pointer record on transfer or destruction; and use raw pointers rather than &T/&mut T where source and destination may alias.

Verus form. Inference: define a ghost state describing allocation ownership, validity, and permitted aliases. Expose unsafe operations through a small wrapper whose requires states pointer validity and non-overlap (or the exact allowed alias relation) and whose ensures states preserved ownership. Use proof fn lemmas for allocation/free transitions and loop invariant clauses for pointer tables. Verus can prove the wrapper’s stated model; foreign code and raw-pointer behavior remain trusted unless separately modeled.

Evidence and limits. The paper reports that 54% of survey respondents who had called foreign functions also used one of Rust’s memory container types to allocate memory for foreign calls; of these, 95% used Box, 28% Arc, and 8% Rc (Section 5.2, p. 10). The percentages for the three types are therefore out of the 54% subset, not of all foreign-function callers and not of all 160 respondents. The paper reports that 17% of the 51% who had used Box in any unsafe context encountered a pointer-invalid-after-move issue, but it did not establish how many had retained raw pointers (p. 10). This uncertainty limits the percentage’s interpretation.

technique 2: model FFI contracts for lifetimes and thread safety

What it is. Foreign APIs often encode lifetime and concurrency properties in documentation or conventions rather than types. One participant summarized the mismatch: “Rust enforces thread safety based on types… C tends to do it based on functions” (Section 5.2, p. 11, P14). One participant observed that C APIs tend to expose pairs of initialization and cleanup functions for each type, which could be linked to the Drop trait of the Rust encapsulation (p. 11). Another participant found foreign types that were only partially thread-safe harder to encapsulate (p. 11).

When to use it. Use contract modeling for every binding whose foreign signature omits ownership, lifetime, aliasing, or thread constraints. It matters especially when a Rust type would automatically implement Send/Sync even though the foreign object is only partially thread-safe.

How it is done. Participants read foreign documentation and implementation (Section 5.2, p. 11). Inference: record preconditions such as initialized state, thread affinity, non-null pointers, and retention duration. record postconditions such as ownership transfer, cleanup, and whether outputs alias inputs. Make wrapper methods enforce these conditions and expose safe operations only when they hold. Table 3 (p. 12) reports that, of 112 respondents who used FFI, 49% always or most of the time intentionally avoided passing abstract Rust data types (structs, enums) by value across FFI boundaries, and 23% always or most of the time intentionally avoided converting raw pointers from FFI calls into safe references (43% sometimes or never). The paper’s prose on p. 13 gives “43%, 3b” for the second practice, which contradicts the table, so the figure is unreliable; the Key Findings say “few actively avoided casting foreign pointers into safe references”. One participant recommended “if you’re doing FFI, the only things you should pass by value are copy types” (P2, p. 12).

Verus form. Inference: represent lifecycle and thread state with ghost tokens or enums and put state transitions in requires/ensures. Use a state-machine proof for initialization, use, and destruction; require a token representing the permitted thread or synchronization state. Avoid claiming Send/Sync safety from a type alone when the foreign contract is function-specific. Verus’s concurrency constructs can prove the model’s transitions, but cannot discover undocumented foreign behavior.

Evidence and limits. Table 3’s denominator is 112 respondents who used FFI. The percentages measure self-reported avoidance, not observed safety. The interview evidence is qualitative and illustrates patterns rather than estimating their prevalence.

technique 3: keep unsafe code minimal, isolated, documented, and auditable

What it is. The community practice is to put unsafe operations behind a safe interface and document the conditions callers must satisfy. The paper says participants “attempted to keep interoperation with foreign code as straightforward as possible” (Section 5.2, p. 12). In the survey, 88% had exposed a safe API for unsafe code (Section 5.5, p. 20), and 83% of the 152 respondents who had used unsafe APIs chose a safe API over an unsafe alternative most of the time or always (Table 9, 9f, p. 19; Section 7, p. 27).

When to use it. Apply the pattern whenever an unsafe operation can be isolated behind a narrow abstraction. It reduces the number of locations requiring proof and makes the contract reviewable. The paper says isolation was not always possible in JIT compilers and operating systems, where unsafe code was used pervasively (Section 5.5, pp. 20, 23).

How it is done. From the paper: participants isolated unsafe code, documented requirements (90% of 68 unsafe-API authors documented them at least most of the time, Table 9c, p. 19), inserted runtime checks at least most of the time in 58% of 141 safe-API cases but only 18% of 68 unsafe-API cases (9b, 9d), and rarely audited dependencies (6% at least most of the time, 4c, Table 4, p. 13). Table 10 (10a, p. 21) reports that 62% of 141 safe-API authors said all safety requirements were satisfied by Rust’s type system at least most of the time; the paper states that only 23% were always certain (Section 7, p. 28). Inference: define a small wrapper, write its safety preconditions and postconditions, validate inputs before entering unsafe, keep the block short, and expose a safe API only if callers cannot trigger undefined behavior; these steps are standard advice, not a procedure the paper evaluates.

Verus form. Inference: put the wrapper’s contract directly on the safe-facing function and isolate any external_body or FFI assumption at the narrow boundary, never on the function whose implementation is being verified. Prove pure Rust logic around the boundary with proof fn, requires, ensures, and invariant; list foreign assumptions as explicit axioms or trusted modules. This makes the trusted base visible but does not eliminate it.

Evidence and limits. The study measures perceptions and practices, not actual bug rates. Participants “rarely audited their dependencies” (Introduction, p. 2; Table 4, 4c), so documentation and self-reported confidence cannot establish soundness.

technique 4: combine dynamic and static tooling across FFI

What it is. Miri is an interpreter that detects violations of Rust aliasing models, but it cannot detect aliasing violations triggered in foreign code and is too slow for large applications (Background, pp. 3–4). One participant (P18) asked for “a version of Miri that could go across that FFI boundary” and another (P1) for “…a unique pointer sanitizer” (Section 7.1, p. 28).

When to use it. The authors expect that “compile-time instrumentation tools will provide the combination of performance and compatibility that is necessary to support large-scale, multilanguage applications”, while dynamic binary instrumentation would benefit participants who contributed to JIT compilers (Section 7.1, p. 28). Inference: use dynamic checks for executions that exercise real foreign calls and static checks for binding shape and contract consistency.

How it is done. The paper describes two routes: inserting run-time checks for aliasing violations during compilation, which requires lowering a subset of Rust’s type information from MIR into the intermediate representations of the platforms so the pass can distinguish references from raw pointers (the authors cite CapsLock and their own BorrowSanitizer), and dynamic binary instrumentation such as Valgrind, which the Krabcake project proposed extending to find Stacked Borrows violations (Section 7.1, p. 28). For static analysis, one participant (P5) wanted a tool to tell “whether your FFI conforms to your expectations…Do all my symbols match? Do all the types signatures match?”; McCormack et al. detected binding errors by comparing the size of types in Rust declarations with LLVM definitions, and the authors say this “could be factored out as a static analysis pass” (Section 7.2, pp. 28–29). Inference: run Miri or an aliasing sanitizer on representative Rust paths and instrument FFI boundaries.

Verus form. Inference: use static Verus contracts for the wrapper and dynamic tools for assumptions that cannot be modeled, such as foreign aliasing and runtime layout. Add a CI check that generated bindings match foreign declarations and that sanitizer runs cover boundary paths. Treat sanitizer success as testing evidence, not a proof; preserve the exact model (Stacked Borrows or Tree Borrows) used by the tool.

Evidence and limits. Section 7.1 (p. 28) says Krabcake was “the second most popular dynamic bug-finding tool behind Miri; it was used by 44% of survey respondents” and that it “is no longer actively maintained, and it is not yet capable of finding bugs in real-world programs”. Section 5.3 (p. 14) gives 44% for Valgrind, the second most used tool, and does not list Krabcake, so Inference: the 44% most likely refers to Valgrind. The paper states “few of our participants had tried using static verification tools” (Section 7.2, p. 29); only 10 survey respondents had used formal methods tools (five Kani, three Prusti, three Creusot, one Flux, one Crucible; Section 5.3, p. 15), and none is reported for Verus. Inference: adoption evidence for Verus/Kani is therefore weak.

what is proved, measured, and trusted

The study proves no Rust program property. It measures self-reported practices, interview themes, and survey distributions. Trusted inputs include participant memory and interpretation, researcher coding, and non-representative community recruitment. The authors state, “We did not evaluate whether participants were able to reason correctly about unsafe code; only how they perceived their usage of these features” (Section 4, p. 8). Participants perceived that Rust lacked a formal specification; one (P10) said, “If you write unsafe code today, you write it against the void” (Section 5.5, p. 22). Inference: foreign specifications may be equally incomplete.

Inference: threat to VL is high at FFI and unsafe boundaries. An agent can generate a syntactically valid wrapper whose contract omits foreign retention, aliasing, layout, or thread assumptions. VL should make those assumptions explicit, isolate them, and combine Verus proofs with binding checks and targeted dynamic instrumentation. The paper already documents the main human/tooling failure modes; repeating a survey without measuring verified artifacts would add little.

techniques for the catalog

• foreign ownership protocol — record allocation, retention, aliasing, and destruction across each FFI boundary
• contractful bindings — specify lifetime, thread, layout, and pre/postconditions that foreign signatures omit
• minimal safe encapsulation — isolate unsafe blocks behind narrow, documented, verified APIs
• mixed FFI tooling — combine static binding checks, Verus contracts, and dynamic aliasing instrumentation
• explicit uncertainty tracking — mark foreign semantics and evolving Rust rules as trusted assumptions Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Participants used unsafe code because they perceived that it was more performant or ergonomic than safe alternatives, or that there were no safe alternatives at all.”): read the whole paper text (Sections 1-8, tables, Figure 1; references skimmed) and checked every quotation, number, section and page reference, and the technique descriptions against it, and viewed the Table 3 page image; changed the link to the arXiv page (the earlier DOI is not in the paper), corrected the Box/Arc/Rc denominator, the Table 3 percentage (table 23% versus prose 43%), several page references (Section 7.1 is p. 28; the 80% figure is p. 27; Table 9 is p. 19), the Krabcake 44% attribution (paper conflict with Valgrind in Section 5.3, flagged), and marked non-paper steps and conclusions as Inference; did not check the cited external works, the Verus-form suggestions (these are Inference and were not tested), or the Zenodo replication package.

Last edited: 2026-10-17