The Safety Promise Ends at the Proof Boundary
Rust is often introduced through a reassuring promise: the compiler prevents a large class of memory errors before a program runs. CULPA, the research system at the center of this series, begins where that promise becomes conditional. Its subject is unsafe Rust and the attempt to detect memory-safety bugs by checking the safety requirements that unsafe operations impose. The useful question is not whether unsafe creates a mysterious hole in Rust, but which proof has moved from the compiler to a programmer, an API caller, or a tool—and whether that proof still holds when real code crosses several boundaries.
That perspective gives this series a practical destination. A reader should be able to look past the presence of an unsafe block, identify the condition that must be true, follow the evidence that supports it, and judge what CULPA's results do and do not establish. The distinction matters because an unsafe marker can mean responsible low-level engineering, an unverified assumption, or a reachable vulnerability. The marker alone cannot tell us which.
The guarantee Rust keeps—and the obligation it moves
Safe Rust gets much of its strength from rules about ownership, borrowing, and lifetimes. A reference is not just an address: its type and lifetime carry constraints about who may use the referred-to data and for how long. The compiler can enforce those constraints in ordinary code, preventing common failures such as dangling references, double frees, and data races. That is why Rust can offer stronger memory-safety guarantees without giving up systems-level performance.
But systems programs sometimes need operations that those rules cannot express directly. A library may need to call foreign code, work with a device, manipulate a raw allocation, or represent a data structure whose most efficient links are not ordinary references. Rust therefore provides an escape hatch, but the escape hatch is more precise than “turn safety off.” An unsafe block permits particular unsafe actions, such as dereferencing a raw pointer or calling an unsafe function. It does not prove that those actions are correct, and it does not erase every other rule in the surrounding program.
The Rust Reference describes this arrangement as the creation and discharge of an extra safety condition. An unsafe function defines conditions that callers must uphold even though the compiler does not check them. An unsafe block says that the programmer asserts those conditions have been satisfied for the operations inside it. The two constructs are logical opposites: the function exports a responsibility, and the block records an attempt to discharge it.
The same pattern appears at other interfaces. An unsafe trait places additional conditions on every implementation; unsafe impl asserts that an implementation meets them. An unsafe external block requires the declared foreign signatures to be correct. An unsafe attribute carries conditions that the compiler cannot determine from the attribute's spelling alone. In each case, the keyword identifies a responsibility boundary. It tells a reviewer where ordinary static guarantees stop being enough, not that the code on one side is automatically defective.
That distinction changes how a code review should begin. “There is an unsafe block here” is an observation. “The pointer must be aligned, non-null, initialized, within the intended allocation, and used under the correct aliasing discipline” is a set of obligations. The second statement can be checked against code, invariants, and inputs. The first cannot support a judgment by itself.
One unsafe boundary, several ways to fail
The Rust Reference's account of unsafety names operations that can violate the memory-safety guarantees of Rust's safe subset. The important lesson for a newcomer is not the entire list of language positions, but the variety of facts an operation may require. CULPA organizes its memory-safety analysis around five: staying within the intended bounds, avoiding a null pointer, using a suitable alignment, reading initialized and type-valid contents, and respecting aliasing and lifetime discipline. A failure in any one of these dimensions can produce a different symptom.
Consider a vector with reserved capacity. Allocating capacity gives a Vec<T> room for elements, but the spare bytes are not automatically initialized values of T. An unsafe operation that increases the vector's length must therefore establish at least two different facts: the new length does not exceed capacity, and every newly exposed element is initialized in a way valid for T. Forgetting the first fact can lead to an out-of-bounds access. Forgetting the second can expose uninitialized memory. The same call, Vec::set_len, sits at the intersection of both obligations.
A type conversion creates a different problem. The paper's motivating examples use an unsafe conversion that can reinterpret bytes as another type. The address might not be correctly aligned for the destination type. Even if the address is aligned, the bytes might not represent a legal value: a bit pattern accepted as raw data is not necessarily a valid bool, character, reference, or other typed value. Alignment and type validity are related to the same memory, but they are not the same proof. Establishing one does not establish the other.
The distinction also applies when safe-looking values cross an unsafe boundary. A string slice carries a UTF-8 validity guarantee. If a wrapper transforms characters into bytes in a way that truncates multibyte characters, that guarantee can be lost before the wrapper calls an unchecked UTF-8 conversion. The final unsafe call may be in a small, visually unremarkable function; the missing evidence was created earlier by a transformation that made the original invariant false.
These examples explain why the paper's authors looked for a common cause beneath different bug names. In their analysis of 64 memory-safety-related bugs from 39 RustSec advisories, they report that every case arose from a violation of a documented safety requirement for an unsafe API. Their categories were InBound, with 27 cases; Initialization, with 26; Alignment, with 7; and NonNull, with 4. Their corpus contained no case classified under ExclusiveAlias, although CULPA models that requirement as well. This is evidence for a unifying lens over that selected advisory corpus, not a claim that every unsafe-Rust defect everywhere has one of these five causes.
A pattern-based analyzer can be useful while still missing this connection. One tool may recognize a suspicious deallocation pattern, another a problematic type conversion, and another a familiar data-flow shape. Such tools can catch important instances, but a new manifestation may not look like any known pattern. CULPA asks a more general question: for this operation and this memory region, are the documented conditions satisfied along a path that an external caller can reach?
CULPA's question: where did the proof break?
CULPA is built around a simple change in emphasis. Instead of treating each bug class as a separate starting point, it treats an unsafe operation's safety requirements as the common ground. The paper's architecture has three linked parts. One part translates documentation into executable predicates. Another identifies the memory object and the sub-regions to which those predicates apply. A third finds the checks and invariants that protect those regions, then follows them through the program to see whether a required safeguard is missing or has been invalidated.
That outline already reveals why the problem is harder than searching for the word unsafe. A contract may be written in natural language and may compress several properties into a phrase such as “valid at its given type.” The relevant memory may be only a range inside one allocation, not the allocation as a whole. A constructor or safe API may establish an invariant without appearing as a direct caller of the unsafe operation. A previous unsafe operation may quietly destroy the invariant that later code appears to rely on. A useful detector must preserve all of those relationships.
The paper calls the final structure a Requirement Graph. Its nodes represent a memory segment and the safeguards that could satisfy requirements for that segment. A path to an unsafe operation is concerning when it remains reachable from a public entry point and lacks a valid safeguard for one of the operation's conditions. A check in an unrelated function is not enough. A guarantee attached to the wrong allocation is not enough. A guarantee that was revoked by a later mutation is not enough.
This is not a promise that every graph result is a confirmed security bug. It is a disciplined way to locate the missing proof. The study reports that CULPA's scope is concentrated on memory-safety problems involving raw pointers and unsafe APIs, especially where standard-library contracts are inherited by third-party wrappers. It does not model every problem that can occur around unsafe code. The paper excludes or leaves outside its main analysis foreign-function issues, logic errors, ordinary runtime panics, and interactions among threads. A package can also fail to reach the analysis because of compilation or dependency problems.
Those boundaries are part of the subject, not a footnote. A detector that reports a warning is not the same as a maintainer who confirms a vulnerability, and a confirmed vulnerability is not the same as a universal proof that all similar code is unsafe. CULPA's value lies in making a class of obligations visible and checkable at a scale where line-by-line human inspection is difficult. Its credibility depends on the quality of its specifications, the accuracy of its memory model, and the care with which warnings are interpreted.
The next question is therefore precise: what does Rust place on each side of the boundary, and how can a reader tell when an unsafe permission has been supported by evidence rather than by confidence? Once that language-level responsibility is clear, CULPA's predicates, memory segments, and reports become easier to understand as attempts to preserve a proof across the places where programs change shape.