Skip to content

Commit 1926ee3

Browse files
celinvalcelinval
committed
Merge remote-tracking branch 'origin/main' into verify-intrinsics
Since intrinsics file has been deleted, we will have to reapply the patch. Conflicts: - library/core/src/intrinsics.rs
2 parents 5e24d04 + a52b65a commit 1926ee3

File tree

616 files changed

+28903
-14023
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

616 files changed

+28903
-14023
lines changed

‎.github/pull_requests.toml

+7-1
Original file line numberDiff line numberDiff line change
@@ -12,5 +12,11 @@ members = [
1212
"jaisnan",
1313
"patricklam",
1414
"ranjitjhala",
15-
"carolynzech"
15+
"carolynzech",
16+
"robdockins",
17+
"HuStmpHrrr",
18+
"Eh2406",
19+
"jswrenn",
20+
"havelund",
21+
"jorajeev"
1622
]

‎.github/workflows/kani.yml

+14
Original file line numberDiff line numberDiff line change
@@ -65,3 +65,17 @@ jobs:
6565
- name: Test Kani script (In Repo Directory)
6666
working-directory: ${{github.workspace}}/head
6767
run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse
68+
69+
# Step 4: Run list on the std library and add output to job summary
70+
- name: Run Kani List
71+
run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
72+
73+
- name: Add Kani List output to job summary
74+
uses: actions/github-script@v6
75+
with:
76+
script: |
77+
const fs = require('fs');
78+
const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8');
79+
await core.summary
80+
.addRaw(kaniOutput)
81+
.write();

‎README.md

+9-10
Original file line numberDiff line numberDiff line change
@@ -7,24 +7,23 @@
77
This repository is a fork of the official Rust programming
88
language repository, created solely to verify the Rust standard
99
library. It should not be used as an alternative to the official
10-
Rust releases. The repository is tool agnostic and welcomes the addition of
10+
Rust releases. The repository is tool agnostic and welcomes the addition of
1111
new tools.
1212

1313
The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
1414
1. Contributing to the core mechanism of verifying the rust standard library
1515
2. Creating new techniques to perform scalable verification
1616
3. Apply techniques to verify previously unverified parts of the standard library.
1717

18-
## [Kani](https://github.com/model-checking/kani)
18+
For that we are launching a contest that includes a series of challenges that focus on verifying
19+
memory safety and a subset of undefined behaviors in the Rust standard library.
20+
Each challenge describes the goal, the success criteria, and whether it has a financial award to be awarded upon its
21+
successful completion.
1922

20-
The Kani Rust Verifier is a bit-precise model checker for Rust.
21-
Kani verifies:
22-
* Memory safety (e.g., null pointer dereferences)
23-
* User-specified assertions (i.e `assert!(...)`)
24-
* The absence of panics (eg., `unwrap()` on `None` values)
25-
* The absence of some types of unexpected behavior (e.g., arithmetic overflows).
23+
See [our book](https://model-checking.github.io/verify-rust-std/intro.html) for more details on the challenge rules
24+
and the list of existing challenges.
2625

27-
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).
26+
We welcome everyone to participate!
2827

2928
## Contact
3029

@@ -40,7 +39,7 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more
4039
Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
4140
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.
4241

43-
## Rust
42+
### Rust
4443
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.
4544

4645
See [the Rust repository](https://github.com/rust-lang/rust) for details.

‎doc/src/SUMMARY.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -25,5 +25,5 @@
2525
- [10: Memory safety of String](./challenges/0010-string.md)
2626
- [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md)
2727
- [12: Safety of `NonZero`](./challenges/0012-nonzero.md)
28-
28+
- [13: Safety of `CStr`](./challenges/0013-cstr.md)
2929

‎doc/src/challenge_template.md

+4-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,9 @@
33
- **Status:** *One of the following: \[Open | Resolved | Expired\]*
44
- **Solution:** *Option field to point to the PR that solved this challenge.*
55
- **Tracking Issue:** *Link to issue*
6-
- **Start date:** *YY/MM/DD*
7-
- **End date:** *YY/MM/DD*
6+
- **Start date:** *YYYY/MM/DD*
7+
- **End date:** *YYYY/MM/DD*
8+
- **Reward:** *TBD*[^reward]
89

910
-------------------
1011

@@ -49,3 +50,4 @@ Note: All solutions to verification challenges need to satisfy the criteria esta
4950
in addition to the ones listed above.
5051

5152
[^challenge_id]: The number of the challenge sorted by publication date.
53+
[^reward]: Leave it as TBD when creating a new challenge. This should only be filled by the reward committee.

‎doc/src/challenges/0001-core-transmutation.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19)
5-
- **Start date:** 2024-06-12
6-
- **End date:** 2024-12-10
5+
- **Start date:** *2024/06/12*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *N/A*
78

89
-------------------
910

‎doc/src/challenges/0002-intrinsics-memory.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16)
5-
- **Start date:** *24/06/12*
6-
- **End date:** *24/12/10*
5+
- **Start date:** *2024/06/12*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *N/A*
78

89
-------------------
910

‎doc/src/challenges/0003-pointer-arithmentic.md

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
# Challenge 3: Verifying Raw Pointer Arithmetic Operations
22

33
- **Status:** Open
4-
- **Solution:**
54
- **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76)
6-
- **Start date:** 24/06/24
7-
- **End date:** 24/12/10
5+
- **Start date:** *2024/06/24*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *N/A*
88

99
-------------------
1010

‎doc/src/challenges/0004-btree-node.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#77](https://github.com/model-checking/verify-rust-std/issues/77)
5-
- **Start date:** *2024-07-01*
6-
- **End date:** *2024-12-10*
5+
- **Start date:** *2024/07/01*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *10,000 USD*
78

89
-------------------
910

‎doc/src/challenges/0005-linked-list.md

+4-3
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
5-
- **Start date:** *24/07/01*
6-
- **End date:** *24/12/10*
5+
- **Start date:** *2024/07/01*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *5,000 USD*
78

89
-------------------
910

@@ -23,7 +24,7 @@ The memory safety of the following public functions that iterating over the inte
2324

2425
| Function | Location |
2526
|---------|---------|
26-
|clearn | alloc::collections::linked_list |
27+
|clear| alloc::collections::linked_list |
2728
|contains| alloc::collections::linked_list |
2829
|split_off| alloc::collections::linked_list |
2930
|remove| alloc::collections::linked_list |

‎doc/src/challenges/0006-nonnull.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53)
5-
- **Start date:** *2024-08-16*
6-
- **End date:** *2024-12-10*
5+
- **Start date:** *2024/08/16*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *N/A*
78

89
-------------------
910

‎doc/src/challenges/0007-atomic-types.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83)
5-
- **Start date:** *2024-10-30*
6-
- **End date:** *2024-12-10*
5+
- **Start date:** *2024/10/30*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *10,000 USD*
78

89
-------------------
910

‎doc/src/challenges/0008-smallsort.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#56](https://github.com/model-checking/verify-rust-std/issues/56)
5-
- **Start date:** *2024-08-17*
6-
- **End date:** *2024-12-10*
5+
- **Start date:** *2024/08/17*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *10,000 USD*
78

89
-------------------
910

‎doc/src/challenges/0009-duration.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#72](https://github.com/model-checking/verify-rust-std/issues/72)
5-
- **Start date:** *2024-08-20*
6-
- **End date:** *2024-12-20*
5+
- **Start date:** *2024/08/20*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *N/A*
78

89
-------------------
910

‎doc/src/challenges/0010-string.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#61](https://github.com/model-checking/verify-rust-std/issues/61)
5-
- **Start date:** *2024-08-19*
6-
- **End date:** *2024-12-10*
5+
- **Start date:** *2024/08/19*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *N/A*
78

89
-------------------
910

‎doc/src/challenges/0011-floats-ints.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,9 @@
33

44
- **Status:** Open
55
- **Tracking Issue:** [#59](https://github.com/model-checking/verify-rust-std/issues/59)
6-
- **Start date:** *2024-08-20*
7-
- **End date:** *2024-12-10*
6+
- **Start date:** *2024/08/20*
7+
- **End date:** *2025/04/10*
8+
- **Reward:** *N/A*
89

910
-------------------
1011

‎doc/src/challenges/0012-nonzero.md

+3-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71)
5-
- **Start date:** *2024-08-23*
6-
- **End date:** *2024-12-10*
5+
- **Start date:** *2024/08/23*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *N/A*
78

89
-------------------
910

‎doc/src/challenges/0013-cstr.md

+86
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
# Challenge 13: Safety of `CStr`
2+
3+
- **Status:** Open
4+
- **Solution:**
5+
- **Tracking Issue:** [#150](https://github.com/model-checking/verify-rust-std/issues/150)
6+
- **Start date:** *2024/11/04*
7+
- **End date:** *2025/04/10*
8+
- **Reward:** *N/A*
9+
10+
-------------------
11+
## Goal
12+
13+
Verify that `CStr` safely represents a borrowed reference to a null-terminated array of bytes sequences similar to
14+
the C string representation.
15+
16+
## Motivation
17+
18+
The `CStr` structure is meant to be used to build safe wrappers of FFI functions that may leverage `CStr::as_ptr`
19+
and the unsafe `CStr::from_ptr` constructor to provide a safe interface to other consumers.
20+
It provides safe methods to convert `CStr` to a Rust `&str` by performing UTF-8 validation, or into an owned `CString`.
21+
22+
Any issue with this structure or misusage of its unsafe methods could trigger an invalid memory access, which poses
23+
a security risk for their users.
24+
25+
## Description
26+
27+
The goal of this challenge is to ensure the safety of the `CStr` struct implementation.
28+
First, we need to specify a safety invariant that captures the essential safety properties that must be maintained.
29+
30+
Next, we should verify that all the safe, public methods respect this invariant.
31+
For example, we can check that creating a `CStr` from a byte slice with method `from_bytes_with_nul` will only yield
32+
safe values of `CStr`.
33+
34+
Finally, for unsafe methods like `from_ptr()` and `from_bytes_with_nul_unchecked`, we need to specify appropriate safety contracts.
35+
These contracts should ensure no undefined behavior occurs within the unsafe methods themselves,
36+
and that they maintain the overall safety invariant of `CStr` when called correctly.
37+
38+
### Assumptions
39+
40+
- Harnesses may be bounded.
41+
42+
### Success Criteria
43+
44+
1. Implement the `Invariant` trait for `CStr`.
45+
46+
2. Verify that the `CStr` safety invariant holds after calling any of the following public safe methods.
47+
48+
| Function | Location |
49+
|------------------------|--------------------|
50+
| `from_bytes_until_nul` | `core::ffi::c_str` |
51+
| `from_bytes_with_nul` | `core::ffi::c_str` |
52+
| `count_bytes` | `core::ffi::c_str` |
53+
| `is_empty` | `core::ffi::c_str` |
54+
| `to_bytes` | `core::ffi::c_str` |
55+
| `to_bytes_with_nul` | `core::ffi::c_str` |
56+
| `bytes` | `core::ffi::c_str` |
57+
| `to_str` | `core::ffi::c_str` |
58+
| `as_ptr` | `core::ffi::c_str` |
59+
60+
3. Annotate and verify the safety contracts for the following unsafe functions:
61+
62+
| Function | Location |
63+
|--------------------------------|---------------------|
64+
| `from_ptr` | `core::ffi::c_str` |
65+
| `from_bytes_with_nul_uncheked` | `core::ffi::c_str` |
66+
| `strlen` | `core::ffi::c_str` |
67+
68+
4. Verify that the following trait implementations for the `CStr` type are safe:
69+
70+
71+
| Trait | Implementation Location |
72+
|-------------------------------------|-------------------------|
73+
| `CloneToUninit` [^unsafe-fn] | `core::clone` |
74+
| `ops::Index<ops::RangeFrom<usize>>` | `core::ffi::c_str` |
75+
76+
[^unsafe-fn]: Unsafe functions will require safety contracts.
77+
78+
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):
79+
80+
- Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
81+
- Performing a place projection that violates the requirements of in-bounds pointer arithmetic.
82+
- Mutating immutable bytes.
83+
- Accessing uninitialized memory.
84+
85+
Note: All solutions to verification challenges need to satisfy the criteria established in the
86+
[challenge book](../general-rules.md) in addition to the ones listed above.

‎doc/src/intro.md

+12-2
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,22 @@ library](https://doc.rust-lang.org/std/). The goal of this is
66
to provide automated verification that can be used to verify that a
77
given Rust standard library implementation is safe.
88

9+
Verifying the Rust libraries is difficult because:
10+
1. Lack of a specification,
11+
2. Lack of an existing verification mechanism in the Rust ecosystem,
12+
3. The large size of the verification problem,
13+
4. The unknowns of scalable verification.
14+
15+
Given the magnitude and scope of the effort, we believe this should be a community owned effort.
16+
For that, we are launching a contest that includes a series of challenges that focus on verifying
17+
memory safety and a subset of undefined behaviors in the Rust standard library.
18+
919
Efforts are largely classified in the following areas:
1020

1121
1. Contributing to the core mechanism of verifying the rust standard library
1222
2. Creating new techniques to perform scalable verification
1323
3. Apply techniques to verify previously unverified parts of the standard library.
1424

25+
There is a financial award tied to each challenge per its specification, which is awarded upon its successful completion.
1526

16-
We encourage everyone to watch this repository to be notified of any
17-
changes.
27+
We encourage everyone to watch this repository to be notified of any changes.

‎doc/src/tool_template.md

+4-4
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,12 @@ _Please list the license(s) that are used by your tool, and if to your knowledge
2020

2121
## Steps to Use the Tool
2222

23-
1. [First Step]
24-
2. [Second Step]
25-
3. [and so on...]
23+
1. \[First Step\]
24+
2. \[Second Step\]
25+
3. \[and so on...\]
2626

2727
## Artifacts
28-
_If there are noteworthy examples of using the tool to perform verificaiton, please include them in this section.Links, papers, etc._
28+
_If there are noteworthy examples of using the tool to perform verification, please include them in this section.Links, papers, etc._
2929

3030
## CI & Versioning
3131
_Please describe how you version the tool and how it will be supported in CI pipelines._

0 commit comments

Comments
 (0)