From b8eedc4ea2c1b5a2698f888c84218abdde37bfca Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 4 Nov 2024 12:09:05 -0800 Subject: [PATCH] Add a new challenge to verify `CStr` --- doc/src/SUMMARY.md | 2 +- doc/src/challenges/0013-cstr.md | 75 +++++++++++++++++++++++++++++++++ 2 files changed, 76 insertions(+), 1 deletion(-) create mode 100644 doc/src/challenges/0013-cstr.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index ca25c36bf449a..4e15d7cacdb50 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -25,5 +25,5 @@ - [10: Memory safety of String](./challenges/0010-string.md) - [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md) - [12: Safety of `NonZero`](./challenges/0012-nonzero.md) - + - [13: Safety of `CStr`](./challenges/0013-cstr.md) diff --git a/doc/src/challenges/0013-cstr.md b/doc/src/challenges/0013-cstr.md new file mode 100644 index 0000000000000..2adb6965a28e3 --- /dev/null +++ b/doc/src/challenges/0013-cstr.md @@ -0,0 +1,75 @@ +# Challenge XXXX[^challenge_id]: Challenge Title + +- **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.