From 38312fbfe396320e309a2eb8078827d46d0a7281 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 4 Nov 2024 12:09:05 -0800 Subject: [PATCH 1/4] 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..f33b5eb466c46 --- /dev/null +++ b/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. From 44ce7cf3843ef13a8eb21db2a67862f76bbfd50b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 4 Nov 2024 14:01:11 -0800 Subject: [PATCH 2/4] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- doc/src/challenges/0013-cstr.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0013-cstr.md b/doc/src/challenges/0013-cstr.md index f33b5eb466c46..4136c03e8e737 100644 --- a/doc/src/challenges/0013-cstr.md +++ b/doc/src/challenges/0013-cstr.md @@ -23,14 +23,14 @@ a security risk for their users. ## Description -The goal of this challenge is to ensure the safety of the CStr struct implementation. +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. +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. From 52ec29e6abc64fa27a63eb82c13e4fcde3af8306 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 4 Nov 2024 16:43:38 -0800 Subject: [PATCH 3/4] Add a few trait implementations to challenge also fix warnings in the tool template section --- doc/src/challenges/0013-cstr.md | 13 +++++++++++-- doc/src/tool_template.md | 6 +++--- 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/doc/src/challenges/0013-cstr.md b/doc/src/challenges/0013-cstr.md index 4136c03e8e737..f8cecac019995 100644 --- a/doc/src/challenges/0013-cstr.md +++ b/doc/src/challenges/0013-cstr.md @@ -63,6 +63,15 @@ and that they maintain the overall safety invariant of `CStr` when called correc | `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>` | `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): @@ -71,5 +80,5 @@ All proofs must automatically ensure the absence of the following undefined beha - 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. +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. diff --git a/doc/src/tool_template.md b/doc/src/tool_template.md index 474b1d089c6ee..5e7b054ed6891 100644 --- a/doc/src/tool_template.md +++ b/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._ From 2b7faee59faf45bc86972860176be184be7157a4 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 13 Nov 2024 11:02:12 -0800 Subject: [PATCH 4/4] add `as_ptr` --- doc/src/challenges/0013-cstr.md | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/src/challenges/0013-cstr.md b/doc/src/challenges/0013-cstr.md index f8cecac019995..ff6048701e50f 100644 --- a/doc/src/challenges/0013-cstr.md +++ b/doc/src/challenges/0013-cstr.md @@ -54,6 +54,7 @@ and that they maintain the overall safety invariant of `CStr` when called correc | `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: