Challenge 13: Safety of CStr
- Status: Open
- Solution:
- Tracking Issue: #150
- Start date: 2024/11/04
- End date: 2025/04/10
- Reward: N/A
Goal
Verify that CStr safely represents a borrowed reference to a null-terminated array of bytes sequences similar to
the C string representation.
Motivation
The CStr structure is meant to be used to build safe wrappers of FFI functions that may leverage CStr::as_ptr
and the unsafe CStr::from_ptr constructor to provide a safe interface to other consumers.
It provides safe methods to convert CStr to a Rust &str by performing UTF-8 validation, or into an owned CString.
Any issue with this structure or misusage of its unsafe methods could trigger an invalid memory access, which poses a security risk for their users.
Description
The goal of this challenge is to ensure the safety of the CStr struct implementation.
First, we need to specify a safety invariant that captures the essential safety properties that must be maintained.
Next, we should verify that all the safe, public methods respect this invariant.
For example, we can check that creating a CStr from a byte slice with method from_bytes_with_nul will only yield
safe values of CStr.
Finally, for unsafe methods like from_ptr() and from_bytes_with_nul_unchecked, we need to specify appropriate safety contracts.
These contracts should ensure no undefined behavior occurs within the unsafe methods themselves,
and that they maintain the overall safety invariant of CStr when called correctly.
Assumptions
- Harnesses may be bounded.
Success Criteria
-
Implement the
Invarianttrait forCStr. -
Verify that the
CStrsafety invariant holds after calling any of the following public safe methods.
| Function | Location |
|---|---|
from_bytes_until_nul | core::ffi::c_str |
from_bytes_with_nul | core::ffi::c_str |
count_bytes | core::ffi::c_str |
is_empty | core::ffi::c_str |
to_bytes | core::ffi::c_str |
to_bytes_with_nul | core::ffi::c_str |
bytes | core::ffi::c_str |
to_str | core::ffi::c_str |
as_ptr | core::ffi::c_str |
- Annotate and verify the safety contracts for the following unsafe functions:
| Function | Location |
|---|---|
from_ptr | core::ffi::c_str |
from_bytes_with_nul_uncheked | core::ffi::c_str |
strlen | core::ffi::c_str |
- Verify that the following trait implementations for the
CStrtype are safe:
| Trait | Implementation Location |
|---|---|
CloneToUninit 1 | core::clone |
ops::Index<ops::RangeFrom<usize>> | core::ffi::c_str |
Unsafe functions will require safety contracts.
All proofs must automatically ensure the absence of the following undefined behaviors ref:
- Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
- Performing a place projection that violates the requirements of in-bounds pointer arithmetic.
- Mutating immutable bytes.
- Accessing uninitialized memory.
Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.