Add a new challenge to verify CStr

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)
 

doc/src/challenges/0013-cstr.md

@@ -0,0 +1,75 @@
+# Challenge 13: Safety of `CStr`
+
+- **Status:** Open
+- **Solution:**
+- **Tracking Issue:** [#150](https://github.com/model-checking/verify-rust-std/issues/150)
+- **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.