forked from rust-lang/rust
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
2 changed files
with
76 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,75 @@ | ||
# Challenge 13: Safety of `CStr` | ||
|
||
- **Status:** Open | ||
- **Solution:** | ||
- **Tracking Issue:** | ||
- **Start date:** 2024/11/04 | ||
- **End date:** 2025/01/31 | ||
|
||
------------------- | ||
## 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 `as_ptr()` and `from_ptr()`, 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 | ||
|
||
1. Implement the `Invariant` trait for `CStr`. | ||
|
||
2. Verify that the `CStr` safety 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` | | ||
|
||
3. 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` | | ||
|
||
|
||
All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): | ||
|
||
- 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](general-rules.md) | ||
in addition to the ones listed above. |