Add Challenge 2: Verify the memory safery of core intrinsics using ra…

…w pointers (rust-lang#14)

Adds the challenge to `Verify the memory safery of core intrinsics using
raw pointers`

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 <mt@debian.org>
Co-authored-by: Celina G. Val <celinval@amazon.com>

doc/src/SUMMARY.md

@@ -4,6 +4,7 @@
 
 - [General Rules](./general-rules.md)
   - [Challenge Template](./template.md)
+  - [Tool application](./todo.md)
 
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
@@ -12,4 +13,4 @@
 ---
 
 # Challenges
-- [Coming soon](./todo.md)
+- [Memory safety of core intrinsics](./intrinsics-memory.md)

doc/src/general-rules.md

@@ -10,7 +10,7 @@ NOTE: This work is not officially affiliated, or endorsed by the Rust project or
 tracking issue where contributors can add comments and ask clarification questions.
 You can find the list of [open challenges here](https://github.com/model-checking/verify-rust-std/labels/Challenge).
 
-**Solutions:** Solutions to a problem should be submitted as a single Pull Request (PR) to this repository. 
+**Solutions:** Solutions to a problem should be submitted as a single Pull Request (PR) to this repository.
 The solution should run as part of the CI.
 See more details about [minimum requirements for each solution](general-rules.md#solution-requirements).
 
@@ -33,7 +33,7 @@ well as to track the status of the challenge.
 
 A proposed solution to a verification problem will only **be reviewed** if all the minimum requirements below are met:
 
-* Each contribution or attempt should be submitted via a pull request to be analyzed by reviewers. 
+* Each contribution or attempt should be submitted via a pull request to be analyzed by reviewers.
 * By submitting the solution, participants confirm that they can use, modify, copy, and redistribute their contribution,
   under the terms of their choice.
 * The contribution must be automated and should be checked and pass as part of the PR checks.
@@ -56,7 +56,7 @@ The type of obstacles users face may depend on which part of the standard librar
 Everyone is welcome to submit new challenge proposals for review by our committee.
 Follow the following steps to create a new proposal:
 
-1. Create a tracking issue using the Issue template [Challenge Proposal](todo.md) for your challenge.
+1. Create a tracking issue using the Issue template [Challenge Proposal](template.md) for your challenge.
 2. In your fork of this repository do the following:
     1. Copy the template file (`book/src/challenge_template.md`) to `book/src/challenges/<ID_NUMBER>-<challenge-name>.md`.
     2. Fill in the details according to the template instructions.

doc/src/intrinsics-memory.md

@@ -0,0 +1,87 @@
+# Challenge 2: Verify the memory safery of core intrinsics using raw pointers
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/16)
+- **Start date:** *24/06/12*
+- **End date:** *24/12/10*
+
+-------------------
+
+
+## Goal
+
+Annotate Rust core::intrinsics functions that manipulate raw pointers with their safety contract. Verify their usage in the standard library is in fact safe.
+
+### Success Criteria
+
+1. All the following intrinsic functions must be annotated with safety contracts.
+2. Any fallback intrinsic implementation must be verified.
+3. For intrinsics modeled in the tool of choice, explain how their implementation matches the intrinsics definition. This can either be done in the PR description or as an entry to the contest book as part of the “Tools” chapter.
+4. For each function, contestants must state clearly the list of assumptions for each proof, how the proofs can be audited, and the list of (implicit and explicit) properties that are guaranteed.
+5. The verification of each intrinsic should ensure all the documented safety conditions are met, and that meeting them is enough to guarantee safe usage.
+
+
+Intrinsic functions to be annotated with safety contracts
+
+| Function | Location |
+|---------|---------|
+|typed_swap | core::intrisics |
+|vtable_size| core::intrisics |
+|vtable_align| core::intrisics |
+|copy_nonoverlapping| core::intrisics |
+|copy| core::intrisics |
+|write_bytes| core::intrisics |
+|size_of_val| core::intrisics |
+|arith_offset| core::intrisics |
+|volatile_copy_nonoverlapping_memory| core::intrisics |
+|volatile_copy_memory| core::intrisics |
+|volatile_set_memory| core::intrisics |
+|volatile_load| core::intrisics |
+|volatile_store| core::intrisics |
+|unaligned_volatile_load| core::intrisics |
+|unaligned_volatile_store| core::intrisics |
+|compare_bytes| core::intrisics |
+|min_align_of_val| core::intrisics |
+|ptr_offset_from| core::intrisics |
+|ptr_offset_from_unsigned| core::intrisics |
+|read_via_copy| core::intrisics |
+|write_via_move| core::intrisics |
+
+
+All the following usages of intrinsics were proven safe:
+
+| Function | Location |
+|---------|---------|
+|copy_from_slice	| core::slice |
+|parse_u64_into	| std::fmt |
+|swap | core::mem |
+|align_of_val | core::mem |
+|zeroed | core::mem::maybe_uninit |
+
+
+
+Annotate and verify all the functions that below that expose intrinsics with safety contracts
+
+| Function | Location |
+|---------|---------|
+|copy_from_slice	| std::ptr |
+|parse_u64_into	| std::ptr |
+|swap | std::ptr |
+|align_of_val | std::ptr |
+|zeroed | std::ptr |
+
+
+
+### List of UBs
+
+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):
+
+* Invoking undefined behavior via compiler intrinsics.
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory except for padding or unions.
+* 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.

doc/src/template.md

@@ -25,35 +25,27 @@
 
 *Mention any assumption that users may make. Example, "assuming the usage of Stacked Borrows".*
 
-### Success Criteria*
+### Success Criteria
 
 *Here are some examples of possible criteria:*
 
 All the following unsafe functions must be annotated with safety contracts and the contracts have been verified:
 
-|Function	|Location	|
-|---	|---	|
-|	|	|
-|	|	|
-|	|	|
-|	|	|
-|	|	|
+| Function | Location |
+|---------|---------|
+|  abc   |  def    |
 
 At least N of the following usages were proven safe:
 
-|Function	|Location	|
-|---	|---	|
-|	|	|
-|	|	|
-|	|	|
-|	|	|
-|	|	|
+| Function | Location |
+|---------|---------|
+|  xyz   |  123   |
 
-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):
+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):
 
 *List of UBs*
 
 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.
 
-[^challenge_id]: The number of the challenge sorted by publication date.
+[^challenge_id]: The number of the challenge sorted by publication date.