This document presents a draft outlining the fundamental safety properties essential for contract definition. The current documentation on API safety descriptions in the standard library remains ad hoc. For example, the term valid pointer is frequently used, but the validity of a pointer depends on the context. In practice, a valid pointer may need to satisfy several fundamental conditions, such as being non-null, not dangling, and pointing to memory properly aligned and initialized for type T. It is worth noting that the Rust community is making progress toward standardizing contract design, as highlighted in the links below. We believe this proposal will contribute to the development and refinement of contract specifications.
Rust Contracts RFC (draft)
MCP759
std-contracts-2025h1
In contract design, safety properties can be categorized into two types:
Precondition: Safety requirements that must be satisfied before invoking an unsafe API. These represent the fundamental conditions for safely using the API.
Postcondition: Traditionally, this refers to properties the system must satisfy after the API call. In Rust, it implies that the program must not violate Rust's safety requirements, such as exclusive mutability, after the API is executed. If an API has postconditions, it indicates that satisfying the preconditions alone does not guarantee program safety. Developers must also carefully analyze the API's implementation and its usage context.
While preconditions and postconditions are foundational to safety reasoning, they may not always be sufficient in Rust. For instance, an API may include optional preconditions. If these conditions are satisfied, the Rust compiler can guarantee that the postconditions will hold. However, meeting these optional requirements is not mandatory. For example, in the case of ptr::read(), specifying that the parameter implements the Copy trait can help avoid undefined behavior related to exclusive mutability. By meeting this optional precondition, developers can ensure safe use of the API while still having the flexibility to omit it when not needed.
Option (new): Optional preconditions for an unsafe API. If satisfying such conditions, it can guarantee that the post condition can be satisfied.
Besides optional preconditions, we also need to document potential hazards of Unsafe APIs. For instance, certain scenarios such as implementing a doubly linked list or the internals of Rc and RefCell require temporarily violating postconditions. In such cases, it is crucial to document how the program state deviates from Rust's safety principles and whether these vulnerabilities are eventually resolved.
Hazard (new): Invoking an unsafe API may temporarily leave the program in a vulnerable or inconsistent state with respect to safe Rust.
In practice, a safety property may correspond to a precondition, optional precondition, or hazard. To address the ambiguity of certain high-level or ad hoc safety property descriptions, we propose breaking them down into primitive safety requirements. By collecting and analyzing commonly used safety descriptions, we aim to provide a clearer framework for understanding and documenting these properties. The following sections will elaborate on these details.
In short, while preconditions must be satisfied, optional preconditions are not mandatory. Hazards highlight vulnerabilities that deviate from Rust's safety principles. Meeting optional preconditions can help avoid certain types of hazards.
| ID | Primitive SP | Usage | Example API |
|---|---|---|---|
| I.1 | Align(p, T) | precond | ptr::read() |
| I.2 | NonZST(T) | precond | NonNull.offset_from |
| I.3 | NoPadding(T) | precond | raw_eq() |
| I.4 | NonNull(p) | precond | NonNull::new_unchecked() |
| I.5.1 | NonDangling(p) | precond | |
| I.5.2 | NonDangling(p, T) | precond | ptr::offset() |
| II.1.1 | AllocatorConsistency(p, A) | precond | Box::from_raw_in() |
| II.1.2 | AllocatorConsistency(p) | precond | Box::from_raw() |
| II.2 | Bounded(p, T, range) | precond | ptr::offset() |
| II.3.1 | NonOverlap(dst, src, T, count) | precond | ptr::copy_nonoverlapping() |
| II.3.2 | NonOverlap(dst, src, T) | precond | ptr::copy() |
| III.1.1 | ValidInt(T, x) | precond | f32.to_int_unchecked() |
| III.1.2 | ValidInt(range(T), x) | precond | NonZero::from_mut_unchecked() |
| III.1.3 | ValidInt(range(T,U), x) | precond | u32::unchecked_shl() |
| III.1.4 | ValidInt(T, uop, x) | precond | unchecked_neg() |
| III.1.5 | ValidInt(T, binop, x, y) | precond | usize.add() |
| III.1.6 | ValidInt(T, binop1, x, binop2, y, z) | precond | slice::from_raw_parts() |
| III.2.1 | ValidString(v) | precond | String::from_utf8_unchecked() |
| ValidString(v) | hazard | String.as_bytes_mut() | |
| III.2.2 | ValidString(p, len) | precond | String::from_raw_parts() |
| III.2.3 | ValidString(s, I) | precond | String.get_unchecked() |
| III.2.4 | ValidString(s, begin, end) | precond | String.slice_unchecked() |
| III.3 | ValidCStr(p, len) | precond | CStr::from_bytes_with_nul_unchecked() |
| III.4.1 | Init(p, range) | precond | BorrowedBuf::set_init() |
| III.4.2 | Init(p, T) | precond | Box::assume_init() |
| III.4.3 | Init(p, T, range) | precond | MaybeUninit::slice_assume_init_mut() |
| Init(p, T, range) | hazard | ptr::copy() | |
| Init(p, T, range) | option | ptr::copy() | |
| III.5 | Unwrap(x, T) | precond | Option::unwrap_unchecked() |
| IV.1 | NonOwned(p) | precond | Box::from_raw() |
| IV.2 | Owned(p) | precond | trait.FromRawFd::from_raw_fd() |
| IV.3 | Alias(p1, p2) | hazard | pointer.as_mut() |
| IV.4 | Lifetime(p, 'a) | precond | AtomicPtr::from_ptr() |
| V.1 | Trait(T) | option | ptr::read() |
| V.2 | Send(T, NoRc) | option | Send |
| V.3 | Sync(T, NoInteriorMut) | option | Sync |
| V.4 | Pinned(p) | hazard | Pin::new_unchecked() |
| V.5 | Opened(fd) | precond | trait.FromRawFd::from_raw_fd() |
| V.6 | NonVolatile(p) | precond | ptr::read() |
Note: These primitives are not yet complete. New proposals are always welcome.
The term valid pointer is widely used for safety descriptions in Rustdoc. Based on the official document, we define the following compound safety properties for valid pointers.
| Compound SP | Primitive SPs | Usage | Example API |
|---|---|---|---|
| ValidPtr(p, T) | !NonZST(T) || ( NonZST(T) && NonDangling(p, T) ) | precond | read(src: *const T) |
| ValidPtr(p, T, range) | !NonZST(T) || ( NonZST(T) && Bounded(p, T, range) ) | precond | copy(src: *const T, dst: *mut T, count: usize) |
| ValidPtr2Ref(p, T) | Align(p,T) && NonDangling(p,T) && Init(p,T) && Alias(p, otherp) | precond, hazard | as_uninit_ref(self) |
Besides,
-
Dereferenceable: The property is equivalent to
$\text{NonDangling}(p, T)$ . -
Typed: The property is equivalent to
$\text{Init}(p, T)$ or$\text{Init}(p, T, range)$ .
Refer to the document of type-layout, there are three components related to layout: alignment, size, and padding.
Alignment is measured in bytes. It must be at least 1 and is always a power of 2. This can be expressed as T is considered aligned if the address is a multiple of alignment(T). The alignment requirement can be formalized as
In practice, we generally require a pointer p of type *T to be aligned. This property can be formalized as:
psp I.1 Align(p, T):
Example APIs: ptr::read(), ptr::write(), Vec::from_raw_parts()
The size of a value is the offset in bytes between successive elements in an array with that item type including alignment padding. It is always a multiple of its alignment (including 0), i.e.,
A safety property may require the size of a type T cannot be zero. We can formulate the requirement as
psp I.2 NonZST(T):
Example API: NonNull.offset_from(), pointer.sub_ptr()
Padding refers to the unused space inserted between successive elements in an array to ensure proper alignment. Padding is taken into account when calculating the size of each element. For example, the following data structure includes 1 byte of padding, resulting in a total size of 4 bytes.
struct MyStruct { a: u16, b: u8 } // alignment: 2; padding 1
mem::size_of::<MyStruct>(); // size: 4A safety property may require the type T has no padding. We can formulate the requirement as
psp I.3 NoPadding(T):
Example API: intrinsic raw_eq()
Referring to the pointer validity documentation, whether a pointer is valid depends on the context of its usage, and the criteria vary across different APIs. To better describe pointer validity and reduce ambiguity, we break down the concept into several primitive components.
The memory address that the pointer refers to is critical. A safety property may require the pointer p to be non-null, as the behavior of dereferencing a null pointer is undefined. This property can be formalized as:
psp II.1 NonNull(p):
Example APIs: NonNull::new_unchecked(), Box::from_non_null()
To determine whether the memory address referenced by a pointer is available for use or has been allocated by the system (either on the heap or the stack), we consider the related safety requirement: non-dangling. This means the pointer must refer to a valid memory address that has not been deallocated on the heap or remains valid on the stack.
In practice, an API may require that a pointer p to a type T must satisfy the non-dangling property.
psp II.2.1 NonDangling(p):
psp II.2.2 NonDangling(p, T):
Proposition 1 (NOT SURE): NonDangling(p, T) implies NonNull(p).
Example APIs: ptr::offset(), Box::from_raw()
Besides, some properties may require the allocator to be consistent, i.e., the memory address pointed by the pointer p should be allocated by a specific allocator A.
psp II.3.1 AllocatorConsistency(p, A):
Example APIs: Arc::from_raw_in(), Box::from_raw_in()
If the allocator A is unspecified, it typically defaults to the global allocator.
psp II.3.2 AllocatorConsistency(p):
Example APIs: Arc::from_raw(), Box::from_raw()
There are two useful derived safety properties based on the previous components.
The first one is bounded access, which requires that the pointer access with respet to an offset stays within the bound. This ensures that dereferencing the pointer yields a value (which may not yet be initialized) of the expected type T.
psp II.4 Bounded(p, T, range):
Example APIs: ptr::offset(), ptr::copy()
Proposition 2 (NOT SURE): Every pointer (p + sizeof(T) * offset) for offset in range implies NonDangling(p, T).
A safety property may require the two pointers do not overlap with respect to T:
psp II.5.1 NonOverlap(dst, src, T):
(This requirement might be more regid than Rustdoc.)
Example APIs: ptr::copy_from(), ptr.copy()
It may also require the two pointers do not overlap with respect to
psp II.5.2 NonOverlap(dst, src, T, count):
Example APIs: ptr::copy_nonoverlapping(), ptr.copy_from_nonoverlapping
When converting a value x to an interger, the value should not be greater than the max or less the min value that can be represented by the integer type T.
psp III.1.1 ValidInt(T, x):
Example APIs: f32.to_int_unchecked(), SimdFloat.to_int_unchecked()
The value x of type T should be within a specific range to be valid.
psp III.1.2 ValidInt(range(T), x):
Example APIs: NonZero::from_mut_unchecked(), isize.unchecked_div() |
psp III.1.3 ValidInt(range(T, U), x):
Example APIs: u32::unchecked_shl(), u32::unchecked_shr()
The result of unary arithmatic operations should not overflow the max or the min value.
psp III.1.4 ValidInt(T, uop, x):
Example API: isize.unchecked_neg()
The result of interger arithmatic of two values x and y of type T should not overflow the max or the min value.
psp III.1.5 ValidInt(T, binop, x, y):
Example APIs: isize.add(), usize.add(), pointer.add(usize.add())
psp III.1.6 ValidInt(T, binop1, x, binop2, y, z):
Example APIs: slice::from_raw_parts()
There are two types of string in Rust, String which requires valid utf-8 format, and CStr for interacting with foreign functions.
The safety properties of String requires the bytes contained in a vector v should be a valid utf-8.
psp III.2.1 ValidString(v):
Example APIs: String::from_utf8_unchecked(), String.as_bytes_mut(), String.as_mut_vec().
We have to label the hazard of the APIs String.as_bytes_mut() and String.as_mut_vec() with ValidString(v) because mutating the resulting bytes or vector may lead to invalid utf-8.
The safety properties of String requires the content pointed by a pointer p of length len should be a valid utf-8.
psp III.2.2 ValidString(p, len):
Example API: String::from_raw_parts().
The content extracted from String s using slice index I must remain valid UTF-8.
psp III.2.3 ValidString(s, I):
Example APIs: String.get_unchecked(), String.get_unchecked_mut()
The slice content ranging from begin to end within String s must be valid UTF-8.
psp III.2.4 ValidString(s, begin, end):
Example APIs: String.slice_unchecked(), String.slice_mut_unchecked()
The safety property of CString generally requires the bytes of a u8 slice or pointed by a pointer p shoule contains a null terminator within isize::MAX from p.
psp III.3 ValidCStr(p, len):
Example APIs: CStr::from_bytes_with_nul_unchecked(), CStr::from_ptr()
A safety property may require a range of memory pointed by a pointer p is initialized. This range of memory can be independent of type T.
psp III.4.1 Init(p, range):
Example APIs: BorrowedBuf::set_init()
Besides, a safety property may require the memory pointed by a pointer p is initialized with specified type T.
psp III.4.2 Init(p, T):
Example APIs: MaybeUninit.assume_init(), Box::assume_init()
psp III.4.3 Init(p, T, range):
Note that this property may serve as either preconditions (e.g., MaybeUninit::slice_assume_init_mut()) or optional requirements and hazards (e.g., ptr::copy().
Example APIs: MaybeUninit::slice_assume_init_mut(), ptr::copy(), ptr::copy_nonoverlapping, NonNull.copy_from
Such safety properties relate to the monadic types, including Option and Result, and they require the value after unwarpping should be of a particular type.
psp III.5 Unwrap(x, T):
Example APIs: Option::unwrap_unchecked(), Result::unwrap_unchecked(), Result::unwrap_err_unchecked()
This category relates to the core mechanism of Rust which aims to avoid shared mutable aliases and achieve automated memory deallocation.
Let one value has two owners at the same program point is vulnerable to double free. Refer to the traidional vulnerbility of mem::forget() compared to ManuallyDrop. The property generally relates to convert a raw pointer to an ownership, and it can be represented as:
psp IV.1 NonOwned(p):
Example APIs: Box::from_raw(), ptr::read(), ptr::read_volatile(),
psp IV.2 Owned(p):
Example APIs: trait.FromRawFd::from_raw_fd(), UdpSocket::from_raw_socket()
(TO FIX: there should be similar issues for other RAII resources, we may not need this because FFI memories cannot require owned.)
There are six types of pointers to a value x, depending on the mutabality and ownership, i.e., owner, mutable owner, reference, mutable reference, raw pointer, mutable raw pointer. The exclusive mutability principle of Rust requires that if a value has a mutable alias at one program point, it must not have other aliases at that program point. Otherwise, it may incur unsafe status. We need to track the particular unsafe status and avoid unsafe behaviors.
psp IV.3 Alias(p1, p2):
Example APIs: pointer.as_mut(), pointer.as_ref(), pointer.as_ref_unchecked()
The property generally requires the lifetime of a raw pointer p must be valid for both reads and writes for the whole lifetime 'a.
psp IV.4 Lifetime(p, 'a):
Example APIs: AtomicPtr::from_ptr(), AtomicBool::from_ptr(), CStr::from_ptr()
If a parameter type T implements certain traits, it can guarantee safety or mitigate specific hazards
psp V.1 Trait(T):
In particular,
Example APIs: ptr::read(), ptr::read_volatile(), Pin::new_unchecked()
Refer to the Rustnomicon, it generally relates to the implementation of the Send/Sync attribute that requires update operations of a critical memory to be exclusive.
Automatically verifying the correctness of the Send trait implementation for any type T is difficult. However, implementing the Send trait can be considered safe if T has no field of Rc type.
psp V.2 Send(T, NoRc):
The function hasrefcount(field) evaluates to true if the type of the field is Rc. If the field is also a compound type, we should recursively evaluate each sub-field.
(TO FIX: This can be defined in a recursive form.)
This is a conditional precondition for implementing the Send trait (NOT SURE: Is it sufficient?). Since implementations of Send trait must not introduce concurrency issues, we do not define corresponding hazards.
Similar to Send(T), we can define the followin optional precondition for Sync(T):
psp V.3 Sync(T, NoInteriorMut):
The function interiormut(field) evaluates to trues if the type of the field is Cell, RefCell, or UnsafeCell. If the field is also a compound type, we should recursively evaluate each sub-field.
(TO FIX: This should be changed to a recursive form.)
Example APIs: Auto trait Send, Sync
Implementing Pin for !Unpin is also valid in Rust, developers should not move the pinned object pointed by p after created.
psp V.4 Pinned(p):
Example APIs: Pin::new_unchecked(),Pin.into_inner_unchecked(), Pin.map_unchecked(), Pin.get_unchecked_mut(), Pin.map_unchecked_mut
The file discripter fd must be opened.
psp V.5 Opened(fd):
Example APIs: trait.FromRawFd::from_raw_fd(), UdpSocket::from_raw_socket()
There are specific APIs for volatile memory access in std-lib, like ptr::read_volatile() and ptr::write_volatile(). Other memory operations should require non-volatile by default.
psp V.6 NonVolatile(p):
Example APIs: ptr::read(), ptr::write()