Fearless Unsafe. A More User-friendly Document for Unsafe Rust Programming Base on Refined Safety Properties.

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

scope and contribution

Cui et al. study how unsafe Rust API documentation can state safety requirements in a uniform, complete, and usable form. They review standard-library APIs, classify requirements as safety properties, reorganize rustdoc text, and expose the result through a rust-analyzer hover plugin. The abstract reports: “We defined a category of Safety Properties (22 items in total) that learned from the documents of unsafe APIs in the standard library.” (p. 1). The paper analyzes 438 public unsafe APIs, 419 Rust CVEs, and unsafe-API usage in 103,516 crates.io repositories. Its final taxonomy has 13 major properties and 22 sub-properties, divided into preconditions and postconditions (Introduction, p. 3).

technique: pre-filter an API corpus before labeling

Inference: use pre-filtering when multiple namespaces and monomorphizations would overweight near-duplicate APIs. The authors inspect Rust 1.75’s std, core, and alloc, including stable and nightly channels (Section 3.1.2, p. 6). They apply three filters:

1. when an API is exposed by both core, std, and alloc, keep one copy
2. for methods on similar numeric types, keep one implementation
3. for compiler intrinsics, retain only those without a stable counterpart

The resulting corpus has 438 unsafe functions; Filter 3.2 folds 127 functions into 11 unique APIs (Section 3.1.2, p. 7).

Inference: for Verus, deduplicate APIs by semantic operation and contract shape before building a proof corpus. Keep distinct ownership, lifetime, and representation cases even when signatures differ only by a numeric type. Record the filtering rules so a learned safety checklist does not silently omit a type-specific obligation.

technique: extract safety properties through staged code review

The review process audits five sources for every API: functional description, safety requirements, subchapters, examples, and source code with comments (Section 3.2, p. 7). It uses five rounds:

1. R1 constructs properties in batches of 30 APIs. The first author proposes unrevealed properties and the other authors verify them in an assembly line. A new property is created only when an obligation cannot fit an existing item; all authors jointly review creation, merging, splitting, or deletion. The paper notes that OverflowCheck and IndexCheck were merged into Bounded, while DualOwned was split from Aliased (Section 3.2.1, p. 7)
2. R2 labels every API with the initial safety properties; the first and second authors audit concurrently and resolve conflicts
3. R3 repeats the labeling review for secondary confirmation, correction, and supplementation
4. R4 revises definitions and labels. The revision reduces 19 earlier properties to 13 major properties with 22 subclasses (Section 3.2.3, p. 7)
5. R5 rewrites documents by linking each document slice to a property and the relevant argument in the signature (Section 3.2.3, p. 7)

Conflicts in property creation or modification require unanimous author agreement; labeling conflicts require more than three authors to agree, otherwise the original decision remains (Conflict Resolution, p. 8). The design goals are generality, unambiguous Rust terminology, non-overlap, composability, essentiality, practicality, and excluding FFI requirements (Section 3.1.1, p. 6). The paper states: “A new item will be defined whenever a safety description cannot be categorized under the existing scheme.” (Section 3.2.1, p. 7).

technique: separate precondition and postcondition safety

The taxonomy isolates call-site obligations from later-use obligations. A precondition safety property (PRE-SP) is an assumption: if inputs violate it, the call can trigger undefined behavior. A postcondition safety property (POS-SP) concerns later operations, assuming all PRE-SPs hold (Section 4.1, p. 8). The authors write: “PRE-SP aligns with the characteristic of unsafe function, i.e., it cannot ensure safety for arbitrary inputs.” (Section 4.1.1, p. 8). They define seven PRE-SPs with 14 sub-properties and six POS-SPs with eight sub-properties.

The 13 major properties and their API-label counts in Table 3 (p. 9) are:

• Allocated, 172: non-null and non-dangling storage
• Bounded, 141: numerical relations and dereferenceable ranges
• Initialized, 104: initialized, typed, and correctly encoded values
• Layout, 109: size, alignment, and exotic-size restrictions
• SystemIO, 26; Thread, 2; Unreachable, 5
• Aliased, 32: aliased, mutated, or outlived access
• DualOwned, 46: overlapping owners or bitwise copies
• Untyped, 37; Freed, 19; Leaked, 35; Pinned, 5

These counts are labels, not disjoint API counts: one API can carry several properties. The authors explicitly note: “No API has all safety property labels in the standard library.” (Section 4.1, p. 9).

Inference: for Verus, encode PRE-SPs as requires predicates on a wrapper function and POS-SPs as ensures clauses about ownership, validity, or allowed subsequent use. For low-level pointer APIs, a documentation label still needs a formal ownership and memory specification. DualOwned, Freed, Leaked, and Pinned often describe obligations around resource protocols rather than simple value predicates, so model them in ghost state or an abstract state machine. Keep the paper’s isolation boundary: prove call preconditions first, then prove post-call usage under those assumptions.

technique: refine overlapping properties with correlation analysis

The authors build two labeled databases. The large dataset keeps the original labeled API collection. The small dataset removes redundancy using Filter 4.1: grouped APIs must have identical labels and at least one relation such as the same method with different mutability, the same trait on different types, the same name within a namespace, or intrinsic encapsulation (Section 4.3.1, pp. 11–12). The stated aim is to “counteract the potential bias from excessive similar APIs” (p. 12). They compute correlation matrices and retain coefficients greater than 0.20 (Figure 3, p. 12). The large dataset can inflate correlation: 30 SliceIndex<[T]> implementations all labeled Bounded and Allocated raise that pair from 0.44 in the small dataset to 0.59 in the large dataset. In the small dataset, Allocated and DualOwned rise from 0.32 to 0.41 because diversity changes the sample (Section 4.3.2, p. 12).

Table 5 reports average correlation coefficients across the two datasets for four pairs: Allocated–Bounded (0.51), Allocated–Layout (0.48), Layout–Untyped (0.45), and Leaked–Untyped (0.49) (Table 5, p. 13). Four properties—Unreachable, SystemIO, Thread, and Pinned—have no substantial correlation in either matrix (Section 4.3.2, p. 12). The authors infer a dereference checklist of Allocated, Bounded, Layout, and Initialized after merging earlier categories (Section 4.3.2, p. 13).

Inference: for Verus, use correlation only to discover candidate reusable lemmas or predicates, never to drop a contract. Evaluate correlations on a deduplicated API set and on a full set, since generic or trait-generated code can distort counts. A high correlation can justify a review shortcut but cannot imply logical entailment; prove each Verus obligation separately.

technique: reorganize documentation into parameter-property-slice triplets

The document-revision procedure has five goals: each API has one unique identifier; safety requirements do not require hyperlink jumps; relevant requirements throughout the native document are covered and irrelevant content removed; missing safety descriptions are supplemented as much as possible; and requirements are enumerated structurally (Section 4.4, p. 13). The authors split native documents into sentences, classify each sentence, identify the related parameter or return value, and form a triplet (P, S, D) where P is parameter, S is safety property, and D is document slice. They flatten linked documents and manually add missing descriptions from other standard-library slices (Section 4.4, p. 13).

For ptr::read, the revised page gives a unique identifier and groups self under Allocated, Bounded, Initialized, and Layout, while retval has DualOwned (Figure 4, p. 14). The revised example attaches non-null, non-dangling, single-allocation, initialization, and alignment requirements to self; Figure 4 labels the example ptr::read but uses a pointer-method identifier and self in the revision. The authors state: “The safety property document has a unique identifier and matches the safety properties, parameters, and native document slices, providing a more structured format.” (Figure 4 caption, p. 14).

Inference: for Verus, represent each verified API in a machine-readable registry keyed by fully qualified function and version. Map each parameter and return value to named predicates and source citations. Generate requires and ensures templates only where the predicate has a checked Verus definition; otherwise show the obligation as documentation. Include version identifiers so a dependency upgrade cannot silently change the contract.

technique: integrate structured safety prompts into an editor

The prototype stores documents in TOML as Parameter.SafetyProperty.[DocumentSlice1, DocumentSlice2, …], converts TOML to JSON, and serializes a lookup structure to avoid repeated parsing. rust-analyzer’s hover component intercepts a function hover, resolves its unique page identifier, and injects the safety-property document when present (Section 4.5, pp. 14–15; Figure 5, p. 15). This gives a developer the obligation at the call site rather than requiring a chain of hyperlinks.

Inference: for Verus, build a language-server or CI integration that shows a function’s Verus requires, ensures, ghost-state obligations, and trusted assumptions on hover. Link each item to the exact source and proof lemma. The editor should expose the proof status and version, but must not imply that a displayed contract has been proved for the caller.

technique: validate taxonomy coverage against real vulnerabilities

For RQ3, the authors search CVEMitre for “Rust”, sort IDs from CVE-2017-20004 through CVE-2024-21629, retain memory-safety issues with source links, exclude information leaks, panic-safety cases, and deprecated or yanked crates, and manually audit code and reports (Section 5.1.1, p. 16). The first two authors double-check the retained set. From 419 screened CVEs, 198 involve misuse of unsafe code; 86.36% of those are attributed to misuse of standard-library unsafe APIs (Section 5.1.1, p. 16). Figure 7’s distribution is Thread 70, Initialized 46, Bounded 27, Layout 20, Aliased 19, Allocated 5, DualOwned 5, Untyped 4, and Freed 5; Unreachable, SystemIO, Leaked, and Pinned have no corresponding CVEs (Section 5.1.2, p. 17).

The CVE-2021-45709 case shows the procedure: inspect the source, identify slice::from_raw_parts_mut, compare the input slice’s constraints with the unsafe call, and classify the violated Layout: Aligned property (Figure 6 and Section 5.1.1, pp. 16–17). The paper says: “In the final dataset (198 CVEs in total), 86.36% of them were attributed to misuse of unsafe APIs within the standard library.” (Section 5.1.1, p. 16).

technique: measure ecosystem exposure with source mining

The crates.io analysis reports mining the latest crates as of 2023-01-30. Section 5.2.1 describes active repositories as its database; the reported total also identifies yanked crates. It finds 21,506 crates containing unsafe code among 103,516 crates, with 3,614 yanked (Section 5.2.2, p. 18). The authors build a dictionary of 140 unsafe API name strings, remove 20 names that also identify safe functions, and filter out cases where the source code does not use the unsafe keyword (Section 5.2.1, p. 18). They count both crates containing each string and total occurrences without compiling, to avoid overhead. Frequent categories include transmutation, allocation/deallocation, unchecked constructors, deferred initialization, unchecked indexing, raw-pointer references, and non-overlapping copies (Section 5.2.2, p. 18).

what is proved, measured, and trusted

Reported: taxonomy size and labels, property correlations, CVE classification, and crates.io source-string counts. The paper also describes document revision and editor integration, without a quantitative usability evaluation of the revised plugin. The paper does not mechanize the taxonomy, prove all revised documents, or show that a rust-analyzer hover prevents a vulnerability. The labels rely on manual reviews, expert judgments, and standard-library documentation. The authors acknowledge that the standard library may not cover every safety category, that programmers may disagree about property boundaries, and that future language versions can add or deprecate APIs (Section 6, pp. 18–19).

techniques for the catalog

Inference: the following catalog entries summarize reusable methods from this study.

• API pre-filtering — deduplicate standard-library namespaces, numeric variants, and intrinsics before safety labeling
• staged property review — derive and revise a safety taxonomy through five audited rounds with explicit conflict rules
• pre/post safety isolation — separate call preconditions from obligations on later use of outputs and memory
• correlation-guided refinement — compare full and deduplicated API datasets to detect taxonomy overlap and sampling bias
• parameter-property-slice documents — attach each requirement to a parameter or return value with a unique API identifier
• editor-integrated safety prompts — serialize structured obligations and show them at the unsafe call site through hover
• CVE coverage audit — classify historical vulnerabilities by violated safety property and double-check the code review
• ecosystem exposure mining — count unsafe API names in crates.io source to prioritize common operations and risks

Last edited: 2026-10-19