Add a new challenge to verify CStr (model-checking#151)

Proposes a new challenge to verify the safety of `CStr` implementation.

---------
Co-authored-by: Zyad Hassan <[email protected]>

Author: celinval

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,85 @@
+# 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 `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
+
+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` |
+| `as_ptr`               | `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`  |
+
+4. Verify that the following trait implementations for the `CStr` type are safe:
+
+
+| Trait                               | Implementation Location |
+|-------------------------------------|-------------------------|
+| `CloneToUninit` [^unsafe-fn]        | `core::clone`           |
+| `ops::Index<ops::RangeFrom<usize>>` | `core::ffi::c_str`      |
+
+[^unsafe-fn]: Unsafe functions will require safety contracts.
+
+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.

doc/src/tool_template.md

@@ -20,9 +20,9 @@ _Please list the license(s) that are used by your tool, and if to your knowledge
 
 ## Steps to Use the Tool
 
-1. [First Step]
-2. [Second Step]
-3. [and so on...]
+1. \[First Step\]
+2. \[Second Step\]
+3. \[and so on...\]
 
 ## Artifacts
 _If there are noteworthy examples of using the tool to perform verificaiton, please include them in this section.Links, papers, etc._