From 359fe20d6317f9e6238272cc27688052360e77ca Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Tue, 20 Aug 2024 11:49:48 -0700 Subject: [PATCH 1/5] Add challenge on memory safety of String (#55) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Michael Tautschnig --- doc/src/SUMMARY.md | 3 +- doc/src/challenges/0010-string.md | 75 +++++++++++++++++++++++++++++++ 2 files changed, 77 insertions(+), 1 deletion(-) create mode 100644 doc/src/challenges/0010-string.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index bb064448efe87..d5885d4ec7bb7 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -18,4 +18,5 @@ - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md) - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) - [Inductive data type](./challenges/0005-linked-list.md) - - [Contracts for SmallSort](./challenges/0008-smallsort.md) \ No newline at end of file + - [Contracts for SmallSort](./challenges/0008-smallsort.md) + - [Memory safety of String](./challenges/0010-string.md) diff --git a/doc/src/challenges/0010-string.md b/doc/src/challenges/0010-string.md new file mode 100644 index 0000000000000..1e7020c52cf53 --- /dev/null +++ b/doc/src/challenges/0010-string.md @@ -0,0 +1,75 @@ +# Challenge X: Memory safety of String + +- **Status:** Open +- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/61) +- **Start date:** *2024-08-19* +- **End date:** *2024-12-10* + +------------------- + +## Goal + +In this challenge, the goal is to verify the memory safety of `std::string::String`. +Even though the majority of `String` methods are safe, many of them are safe abstractions over unsafe code. + +For instance, the `insert` method is implemented as follows in v1.80.1: +```rust +pub fn insert(&mut self, idx: usize, ch: char) { + assert!(self.is_char_boundary(idx)); + let mut bits = [0; 4]; + let bits = ch.encode_utf8(&mut bits).as_bytes(); + + unsafe { + self.insert_bytes(idx, bits); + } +} +``` +where `insert_bytes` has the following implementation: +```rust +unsafe fn insert_bytes(&mut self, idx: usize, bytes: &[u8]) { + let len = self.len(); + let amt = bytes.len(); + self.vec.reserve(amt); + + unsafe { + ptr::copy(self.vec.as_ptr().add(idx), self.vec.as_mut_ptr().add(idx + amt), len - idx); + ptr::copy_nonoverlapping(bytes.as_ptr(), self.vec.as_mut_ptr().add(idx), amt); + self.vec.set_len(len + amt); + } +} +``` +The call to the unsafe `insert_bytes` method (which itself contains unsafe code) makes `insert` susceptible to undefined behavior. + +### Success Criteria + +Verify the memory safety of all public functions that are safe abstractions over unsafe code: + +1. `from_utf16le` (unbounded) +1. `from_utf16le_lossy`(unbounded) +1. `from_utf16be` (unbounded) +1. `from_utf16be_lossy` (unbounded) +1. `pop` +1. `remove` +1. `remove_matches` (unbounded) +1. `retain` (unbounded) +1. `insert` +1. `insert_str` (unbounded) +1. `split_off` (unbounded) +1. `drain` +1. `replace_range` (unbounded) +1. `into_boxed_str` +1. `leak` + +Ones marked as unbounded must be verified for any string/slice length. + +### List of UBs + +All proofs must automatically ensure the absence of the following [undefined behaviors](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. +* Reading from uninitialized memory. +* Mutating immutable bytes. +* Producing an invalid value + +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 8f3252f0a82b22f9f16f580117d92e8c34a8bf51 Mon Sep 17 00:00:00 2001 From: Patrick Lam Date: Fri, 23 Aug 2024 03:27:24 +1200 Subject: [PATCH 2/5] Add self to pull_requests.toml (#65) As mentioned elsewhere, add self to list of people willing to help evaluate submissions. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/pull_requests.toml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml index 12113728fc722..979d2ad13b80e 100644 --- a/.github/pull_requests.toml +++ b/.github/pull_requests.toml @@ -9,5 +9,6 @@ members = [ "remi-delmas-3000", "qinheping", "tautschnig", - "jaisnan" + "jaisnan", + "patricklam" ] From 46352cfdf318b8c7aff310719aad3ec193de3a23 Mon Sep 17 00:00:00 2001 From: rahulku Date: Thu, 22 Aug 2024 09:14:30 -0700 Subject: [PATCH 3/5] Introduce tool template (#64) --- .github/TOOL_REQUEST_TEMPLATE.md | 31 +++++++++++++++++++++++++++++++ README.md | 9 ++++++--- 2 files changed, 37 insertions(+), 3 deletions(-) create mode 100644 .github/TOOL_REQUEST_TEMPLATE.md diff --git a/.github/TOOL_REQUEST_TEMPLATE.md b/.github/TOOL_REQUEST_TEMPLATE.md new file mode 100644 index 0000000000000..474b1d089c6ee --- /dev/null +++ b/.github/TOOL_REQUEST_TEMPLATE.md @@ -0,0 +1,31 @@ +_The following form is designed to provide information for your tool that should be included in the effort to verify the Rust standard library. Please note that the tool will need to be **supported** if it is to be included._ + +## Tool Name +_Please enter your tool name here._ + +## Description +_Please enter a description for your tool and any information you deem relevant._ + +## Tool Information + +* [ ] Does the tool perform Rust verification? +* [ ] Does the tool deal with *unsafe* Rust code? +* [ ] Does the tool run independently in CI? +* [ ] Is the tool open source? +* [ ] Is the tool under development? +* [ ] Will you or your team be able to provide support for the tool? + +## Licenses +_Please list the license(s) that are used by your tool, and if to your knowledge they conflict with the Rust standard library license(s)._ + +## Steps to Use the Tool + +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._ + +## CI & Versioning +_Please describe how you version the tool and how it will be supported in CI pipelines._ diff --git a/README.md b/README.md index b718f3fc6b1cd..c3c9712cb2669 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,8 @@ This repository is a fork of the official Rust programming language repository, created solely to verify the Rust standard library. It should not be used as an alternative to the official -Rust releases. +Rust releases. The repository is tool agnostic and welcomes the addition of +new tools. The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe. 1. Contributing to the core mechanism of verifying the rust standard library @@ -36,12 +37,14 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more ## License ### Kani - Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0). See [LICENSE-APACHE](https://github.com/model-checking/kani/blob/main/LICENSE-APACHE) and [LICENSE-MIT](https://github.com/model-checking/kani/blob/main/LICENSE-MIT) for details. ## Rust - Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses. See [the Rust repository](https://github.com/rust-lang/rust) for details. + +## Introducing a New Tool + +Please use the [template available in this repository](.github/TOOL_REQUEST_TEMPLATE.md) to introduce a new verification tool. From b3fb221733f86d1ab3df63b54accc3691af14390 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Thu, 22 Aug 2024 11:27:11 -0700 Subject: [PATCH 4/5] Fix challenge number (#63) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- doc/src/challenges/0010-string.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0010-string.md b/doc/src/challenges/0010-string.md index 1e7020c52cf53..cb12bfe9fdfbd 100644 --- a/doc/src/challenges/0010-string.md +++ b/doc/src/challenges/0010-string.md @@ -1,4 +1,4 @@ -# Challenge X: Memory safety of String +# Challenge 10: Memory safety of String - **Status:** Open - **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/61) From 957d2bb75b4d2caafd72e74917f1ec8a51fdf4c6 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Thu, 22 Aug 2024 18:30:03 -0400 Subject: [PATCH 5/5] Add "ranjitjhala" and "carolynzech" to commitee (#68) Add "ranjitjhala" and "carolynzech" to commitee toml By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/pull_requests.toml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml index 979d2ad13b80e..45a38b3cc2307 100644 --- a/.github/pull_requests.toml +++ b/.github/pull_requests.toml @@ -10,5 +10,7 @@ members = [ "qinheping", "tautschnig", "jaisnan", - "patricklam" + "patricklam", + "ranjitjhala", + "carolynzech" ]