From 723b8a1c6eca0b0729a9fafda58bf349444896c2 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 21 Nov 2024 15:54:10 -0800 Subject: [PATCH] Add reward information to the repository I also reward suggestions to a few challenges, and postponed the end date of all challenges. --- README.md | 19 +++++++++---------- doc/src/challenge_template.md | 6 ++++-- doc/src/challenges/0001-core-transmutation.md | 5 +++-- doc/src/challenges/0002-intrinsics-memory.md | 3 ++- .../challenges/0003-pointer-arithmentic.md | 4 ++-- doc/src/challenges/0004-btree-node.md | 5 +++-- doc/src/challenges/0005-linked-list.md | 3 ++- doc/src/challenges/0006-nonnull.md | 5 +++-- doc/src/challenges/0007-atomic-types.md | 5 +++-- doc/src/challenges/0008-smallsort.md | 5 +++-- doc/src/challenges/0009-duration.md | 5 +++-- doc/src/challenges/0010-string.md | 5 +++-- doc/src/challenges/0011-floats-ints.md | 5 +++-- doc/src/challenges/0012-nonzero.md | 5 +++-- doc/src/challenges/0013-cstr.md | 3 ++- doc/src/intro.md | 14 ++++++++++++-- 16 files changed, 60 insertions(+), 37 deletions(-) diff --git a/README.md b/README.md index 41cf22c3a7c7a..e304bf5e4d4d7 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ 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. The repository is tool agnostic and welcomes the addition of +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. @@ -15,16 +15,15 @@ The goal is to have a verified [Rust standard library](https://doc.rust-lang.org 2. Creating new techniques to perform scalable verification 3. Apply techniques to verify previously unverified parts of the standard library. -## [Kani](https://github.com/model-checking/kani) +For that we are launching a contest that includes a series of challenges that focus on verifying +memory safety and a subset of undefined behaviors in the Rust standard library. +Each challenge describes the goal, the success criteria, and whether it has a financial award to awarded upon its +successful completion. -The Kani Rust Verifier is a bit-precise model checker for Rust. -Kani verifies: -* Memory safety (e.g., null pointer dereferences) -* User-specified assertions (i.e `assert!(...)`) -* The absence of panics (eg., `unwrap()` on `None` values) -* The absence of some types of unexpected behavior (e.g., arithmetic overflows). +See [our book](https://model-checking.github.io/verify-rust-std/intro.html) more details on the challenge rules +and the list of existing challenges. -You can find out more about Kani from the [Kani book](https://model-checking.github.io/kani/) or the [Kani repository on Github](https://github.com/model-checking/kani). +We welcome everyone to participate! ## Contact @@ -40,7 +39,7 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more 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 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. diff --git a/doc/src/challenge_template.md b/doc/src/challenge_template.md index 50461e2a4e7c4..a39fad01050f1 100644 --- a/doc/src/challenge_template.md +++ b/doc/src/challenge_template.md @@ -3,8 +3,9 @@ - **Status:** *One of the following: \[Open | Resolved | Expired\]* - **Solution:** *Option field to point to the PR that solved this challenge.* - **Tracking Issue:** *Link to issue* -- **Start date:** *YY/MM/DD* -- **End date:** *YY/MM/DD* +- **Start date:** *YYYY/MM/DD* +- **End date:** *YYYY/MM/DD* +- **Reward:** *TBD*[^reward] ------------------- @@ -49,3 +50,4 @@ Note: All solutions to verification challenges need to satisfy the criteria esta in addition to the ones listed above. [^challenge_id]: The number of the challenge sorted by publication date. +[^reward]: Leave it as TBD when creating a new challenge. This should only be filled by the reward committee. diff --git a/doc/src/challenges/0001-core-transmutation.md b/doc/src/challenges/0001-core-transmutation.md index 2b53256b3c34e..66352a0ecb273 100644 --- a/doc/src/challenges/0001-core-transmutation.md +++ b/doc/src/challenges/0001-core-transmutation.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19) -- **Start date:** 2024-06-12 -- **End date:** 2024-12-10 +- **Start date:** *2024/06/12* +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md index 185e04e5a3e2a..9c95de04a623a 100644 --- a/doc/src/challenges/0002-intrinsics-memory.md +++ b/doc/src/challenges/0002-intrinsics-memory.md @@ -3,7 +3,8 @@ - **Status:** Open - **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16) - **Start date:** *24/06/12* -- **End date:** *24/12/10* +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md index 5362983ffe0f3..4feb2f3efeaf6 100644 --- a/doc/src/challenges/0003-pointer-arithmentic.md +++ b/doc/src/challenges/0003-pointer-arithmentic.md @@ -1,10 +1,10 @@ # Challenge 3: Verifying Raw Pointer Arithmetic Operations - **Status:** Open -- **Solution:** - **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76) - **Start date:** 24/06/24 -- **End date:** 24/12/10 +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md index 835d71365292f..9758442b67e06 100644 --- a/doc/src/challenges/0004-btree-node.md +++ b/doc/src/challenges/0004-btree-node.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#77](https://github.com/model-checking/verify-rust-std/issues/77) -- **Start date:** *2024-07-01* -- **End date:** *2024-12-10* +- **Start date:** **2024/07/01** +- **End date:** *2025/04/10* +- **Reward:** *10,000 USD* ------------------- diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md index a5c931712025a..ee5a921068c67 100644 --- a/doc/src/challenges/0005-linked-list.md +++ b/doc/src/challenges/0005-linked-list.md @@ -3,7 +3,8 @@ - **Status:** Open - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) - **Start date:** *24/07/01* -- **End date:** *24/12/10* +- **End date:** *2025/04/10* +- **Reward:** *5,000 USD* ------------------- diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md index 923e00427ad62..bd419bb6a01b6 100644 --- a/doc/src/challenges/0006-nonnull.md +++ b/doc/src/challenges/0006-nonnull.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53) -- **Start date:** *2024-08-16* -- **End date:** *2024-12-10* +- **Start date:** **2024/08/16** +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md index 69bff582f7751..12ee553ceb5d1 100644 --- a/doc/src/challenges/0007-atomic-types.md +++ b/doc/src/challenges/0007-atomic-types.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83) -- **Start date:** *2024-10-30* -- **End date:** *2024-12-10* +- **Start date:** **2024/10/30** +- **End date:** *2025/04/10* +- **Reward:** *10,000 USD* ------------------- diff --git a/doc/src/challenges/0008-smallsort.md b/doc/src/challenges/0008-smallsort.md index c6632af9af837..b49258b3e4e7c 100644 --- a/doc/src/challenges/0008-smallsort.md +++ b/doc/src/challenges/0008-smallsort.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#56](https://github.com/model-checking/verify-rust-std/issues/56) -- **Start date:** *2024-08-17* -- **End date:** *2024-12-10* +- **Start date:** **2024/08/17** +- **End date:** *2025/04/10* +- **Reward:** *10,000 USD* ------------------- diff --git a/doc/src/challenges/0009-duration.md b/doc/src/challenges/0009-duration.md index e2af60ec6c1bb..f7115d18c1097 100644 --- a/doc/src/challenges/0009-duration.md +++ b/doc/src/challenges/0009-duration.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#72](https://github.com/model-checking/verify-rust-std/issues/72) -- **Start date:** *2024-08-20* -- **End date:** *2024-12-20* +- **Start date:** **2024/08/20** +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0010-string.md b/doc/src/challenges/0010-string.md index 4783841bee429..ff4bb2e7bf924 100644 --- a/doc/src/challenges/0010-string.md +++ b/doc/src/challenges/0010-string.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#61](https://github.com/model-checking/verify-rust-std/issues/61) -- **Start date:** *2024-08-19* -- **End date:** *2024-12-10* +- **Start date:** **2024/08/19** +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0011-floats-ints.md b/doc/src/challenges/0011-floats-ints.md index 9dde411c527ca..84ba105a10c65 100644 --- a/doc/src/challenges/0011-floats-ints.md +++ b/doc/src/challenges/0011-floats-ints.md @@ -3,8 +3,9 @@ - **Status:** Open - **Tracking Issue:** [#59](https://github.com/model-checking/verify-rust-std/issues/59) -- **Start date:** *2024-08-20* -- **End date:** *2024-12-10* +- **Start date:** **2024/08/20** +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index 15d2abbb8eb3c..7daa71f3f3c17 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2024-08-23* -- **End date:** *2024-12-10* +- **Start date:** **2024/08/23** +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0013-cstr.md b/doc/src/challenges/0013-cstr.md index ff6048701e50f..c4fbfe144bd3b 100644 --- a/doc/src/challenges/0013-cstr.md +++ b/doc/src/challenges/0013-cstr.md @@ -4,7 +4,8 @@ - **Solution:** - **Tracking Issue:** [#150](https://github.com/model-checking/verify-rust-std/issues/150) - **Start date:** 2024/11/04 -- **End date:** 2025/01/31 +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- ## Goal diff --git a/doc/src/intro.md b/doc/src/intro.md index 441d339dcf72d..98065f85d0d1f 100644 --- a/doc/src/intro.md +++ b/doc/src/intro.md @@ -6,12 +6,22 @@ library](https://doc.rust-lang.org/std/). The goal of this is to provide automated verification that can be used to verify that a given Rust standard library implementation is safe. +Verifying the Rust libraries is difficult because: +1. Lack of a specification, +2. Lack of an existing verification mechanism in the Rust ecosystem, +3. Lhe large size of the verification problem, +4. The unknowns of scalable verification. + +Given the magnitude and scope of the effort, we believe this should be a community owned effort. +For that, we are launching a contest that includes a series of challenges that focus on verifying +memory safety and a subset of undefined behaviors in the Rust standard library. + Efforts are largely classified in the following areas: 1. Contributing to the core mechanism of verifying the rust standard library 2. Creating new techniques to perform scalable verification 3. Apply techniques to verify previously unverified parts of the standard library. +There is a financial award tied to each challenge per its specification, which is awarded upon its successful completion. -We encourage everyone to watch this repository to be notified of any -changes. \ No newline at end of file +We encourage everyone to watch this repository to be notified of any changes. \ No newline at end of file