From e1db022362bc78aa36e8dac1f0ab6be7a3507973 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 20 Jun 2024 15:32:09 -0700 Subject: [PATCH 1/3] Add a new challenge about pointer arithmetic ops In this challenge, we want to look at the safe usage of pointer arithmetic operations. --- doc/src/SUMMARY.md | 1 + .../challenges/0003-pointer-arithmentic.md | 107 ++++++++++++++++++ 2 files changed, 108 insertions(+) create mode 100644 doc/src/challenges/0003-pointer-arithmentic.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index dba8cd9090183..992ca46a7c818 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -15,3 +15,4 @@ - [Challenges](./challenges.md) - [Core Transmutation](./challenges/0001-core-transmutation.md) - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md) + - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md) diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md new file mode 100644 index 0000000000000..0becdc544931d --- /dev/null +++ b/doc/src/challenges/0003-pointer-arithmentic.md @@ -0,0 +1,107 @@ +# Challenge 3: Verifying Raw Pointer Arithmetic Operations + +- **Status:** Open +- **Solution:** +- **Tracking Issue:** +- **Start date:** 24/06/24 +- **End date:** 24/12/10 + +------------------- + + +## Goal + +The goal of this challenge is to verify safety of code that relies on raw pointer arithmetic, and eventual +raw pointer access. + +## Motivation + +Raw pointer arithmetic is a common operation employed in the implementation of highly optimized code, +as well as containers with dynamic size. +Examples of the former are `str::repeat`, `[u8]::is_asc_ii`, +while for the latter we have `Vec`, `VecDeque`, `HashMap`. + +These unsafe operations are usually abstracted from the end user with the usage of +[safe abstractions](https://doc.rust-lang.org/beta/book/ch19-01-unsafe-rust.html#creating-a-safe-abstraction-over-unsafe-code). +However, bugs in these abstractions may compromise entire applications, potentially becoming a security concern. +See [CVE-2018-1000810](https://www.cvedetails.com/cve/CVE-2018-1000810/) for an example of an issue with an +optimization of `str::repeat`. + +These safe abstractions are great candidates for software verification. +They are critical for Rust applications safety, and they are modular by design. + +## Description + +Rust provide different options for pointer arithmetic, which have different semantics when it comes to safety. +For example, methods such as [`ptr::offset`](https://doc.rust-lang.org/std/primitive.pointer.html#method.offset), +[`ptr::add`](https://doc.rust-lang.org/std/primitive.pointer.html#method.add), +and [`ptr::sub`](https://doc.rust-lang.org/std/primitive.pointer.html#method.sub) +are unsafe, and one of their safety condition is that: +> - Both the starting and resulting pointer must be either in bounds or one byte past the end of the same allocated object. + +I.e., violating this safety condition triggers immediate UB. + +On the other hand, wrapping operations such as +[`ptr::wrapping_offset`](https://doc.rust-lang.org/std/primitive.pointer.html#method.wrapping_offset), +[`ptr::wrapping_add`](https://doc.rust-lang.org/std/primitive.pointer.html#method.wrapping_add), +[`ptr::wrapping_sub`](https://doc.rust-lang.org/std/primitive.pointer.html#method.wrapping_sub), +are safe, however, the resulting pointer must not be used to read or write other allocated objects. + +Thus, we would like to be able to verify usage of these different methods within the standard library +to ensure they are safely employed, +as well as provide function contract that can be used by other Rust crates to verify their own usage of these methods. + +### Assumptions + +For this challenge, we do not require a full proof that is independent of the pointee type `T`. +Instead, we require that the verification is done for the following pointee types: +1. All integer type. +2. At least one `dyn Trait`. +3. At least one slice. +4. For unit type. +5. At least one composite types with multiple non-ZST fields. + +### Success Criteria + +All the following unsafe functions must be annotated with safety contracts and the contracts have been verified: + +| Function | Location | +|-----------------------------|----------| +| *const T::add | core::ptr | +| *const T::sub | core::ptr | +| *const T::offset | core::ptr | +| *const T::offset_from | core::ptr | +| *const T::byte_add | core::ptr | +| *const T::byte_sub | core::ptr | +| *const T::byte_offset | core::ptr | +| *const T::byte_offset_from | core::ptr | +| *mut T::add | core::ptr | +| *mut T::sub | core::ptr | +| *mut T::offset | core::ptr | +| *mut T::offset_from | core::ptr | +| *mut T::byte_add | core::ptr | +| *mut T::byte_sub | core::ptr | +| *mut T::byte_offset | core::ptr | +| *mut T::byte_offset_from | core::ptr | + +At least 3 of the following usages were proven safe: + +| Function | Location | +|-------------------|---------------| +| \[u8\]::is_asc_ii | core::slice | +| String::remove | alloc::string | + | Vec::swap_remove | alloc::vec | + | Option::as_slice | core::option | + | VecDeque::swap | collections::vec_deque | + +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. +A place projection is a field expression, a tuple index expression, or an array/slice index expression. +- Invoking undefined behavior via compiler intrinsics. +- Producing an invalid value, even in private fields and locals. + +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 5d5fa0b2972ece16eb854766aae22d1f4164c0f6 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 25 Jun 2024 14:14:07 -0700 Subject: [PATCH 2/3] Apply suggestions from code review Co-authored-by: Michael Tautschnig --- doc/src/challenges/0003-pointer-arithmentic.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md index 0becdc544931d..8587b26b35fa4 100644 --- a/doc/src/challenges/0003-pointer-arithmentic.md +++ b/doc/src/challenges/0003-pointer-arithmentic.md @@ -32,11 +32,11 @@ They are critical for Rust applications safety, and they are modular by design. ## Description -Rust provide different options for pointer arithmetic, which have different semantics when it comes to safety. +Rust provides different options for pointer arithmetic, which have different semantics when it comes to safety. For example, methods such as [`ptr::offset`](https://doc.rust-lang.org/std/primitive.pointer.html#method.offset), [`ptr::add`](https://doc.rust-lang.org/std/primitive.pointer.html#method.add), and [`ptr::sub`](https://doc.rust-lang.org/std/primitive.pointer.html#method.sub) -are unsafe, and one of their safety condition is that: +are unsafe, and one of their safety conditions is that: > - Both the starting and resulting pointer must be either in bounds or one byte past the end of the same allocated object. I.e., violating this safety condition triggers immediate UB. @@ -49,17 +49,17 @@ are safe, however, the resulting pointer must not be used to read or write other Thus, we would like to be able to verify usage of these different methods within the standard library to ensure they are safely employed, -as well as provide function contract that can be used by other Rust crates to verify their own usage of these methods. +as well as provide function contracts that can be used by other Rust crates to verify their own usage of these methods. ### Assumptions For this challenge, we do not require a full proof that is independent of the pointee type `T`. Instead, we require that the verification is done for the following pointee types: -1. All integer type. +1. All integer types. 2. At least one `dyn Trait`. 3. At least one slice. 4. For unit type. -5. At least one composite types with multiple non-ZST fields. +5. At least one composite type with multiple non-ZST fields. ### Success Criteria From fbac06593c7e2c04faab1922b38ab41b91760977 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 25 Jun 2024 14:27:17 -0700 Subject: [PATCH 3/3] Update doc/src/challenges/0003-pointer-arithmentic.md Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- doc/src/challenges/0003-pointer-arithmentic.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md index 8587b26b35fa4..0e73c3c7f014a 100644 --- a/doc/src/challenges/0003-pointer-arithmentic.md +++ b/doc/src/challenges/0003-pointer-arithmentic.md @@ -18,7 +18,7 @@ raw pointer access. Raw pointer arithmetic is a common operation employed in the implementation of highly optimized code, as well as containers with dynamic size. -Examples of the former are `str::repeat`, `[u8]::is_asc_ii`, +Examples of the former are `str::repeat`, `[u8]::is_ascii`, while for the latter we have `Vec`, `VecDeque`, `HashMap`. These unsafe operations are usually abstracted from the end user with the usage of