From f40c10a29faa15fe43f0894c65bafb83217a08cc Mon Sep 17 00:00:00 2001 From: Jack Wrenn Date: Tue, 10 Oct 2023 14:48:42 -0400 Subject: [PATCH] Document zerocopy's design ethos. (#405) Co-authored-by: Joshua Liebow-Feeser --- README.md | 21 +++++++++++++++++++++ src/lib.rs | 21 +++++++++++++++++++++ 2 files changed, 42 insertions(+) diff --git a/README.md b/README.md index d9d3d907d2..143b4674c3 100644 --- a/README.md +++ b/README.md @@ -86,6 +86,27 @@ for network parsing. [simd-layout]: https://rust-lang.github.io/unsafe-code-guidelines/layout/packed-simd-vectors.html +## Security Ethos + +Zerocopy is expressly designed for use in security-critical contexts. We +strive to ensure that that zerocopy code is sound under Rust's current +memory model, and *any future memory model*. We ensure this by: +- **...not 'guessing' about Rust's semantics.** + We annotate `unsafe` code with a precise rationale for its soundness that + cites a relevant section of Rust's official documentation. When Rust's + documented semantics are unclear, we work with the Rust Operational + Semantics Team to clarify Rust's documentation. +- **...rigorously testing our implementation.** + We run tests using [Miri], ensuring that zerocopy is sound across a wide + array of supported target platforms of varying endianness and pointer + width, and across both current and experimental memory models of Rust. +- **...formally proving the correctness of our implementation.** + We apply formal verification tools like [Kani][kani] to prove zerocopy's + correctness. + +[Miri]: https://github.com/rust-lang/miri +[Kani]: https://github.com/model-checking/kani + ## Disclaimer Disclaimer: Zerocopy is not an officially supported Google product. diff --git a/src/lib.rs b/src/lib.rs index bce3e6df4c..c7c0899979 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -84,6 +84,27 @@ //! may be removed at any point in the future. //! //! [simd-layout]: https://rust-lang.github.io/unsafe-code-guidelines/layout/packed-simd-vectors.html +//! +//! # Security Ethos +//! +//! Zerocopy is expressly designed for use in security-critical contexts. We +//! strive to ensure that that zerocopy code is sound under Rust's current +//! memory model, and *any future memory model*. We ensure this by: +//! - **...not 'guessing' about Rust's semantics.** +//! We annotate `unsafe` code with a precise rationale for its soundness that +//! cites a relevant section of Rust's official documentation. When Rust's +//! documented semantics are unclear, we work with the Rust Operational +//! Semantics Team to clarify Rust's documentation. +//! - **...rigorously testing our implementation.** +//! We run tests using [Miri], ensuring that zerocopy is sound across a wide +//! array of supported target platforms of varying endianness and pointer +//! width, and across both current and experimental memory models of Rust. +//! - **...formally proving the correctness of our implementation.** +//! We apply formal verification tools like [Kani][kani] to prove zerocopy's +//! correctness. +//! +//! [Miri]: https://github.com/rust-lang/miri +//! [Kani]: https://github.com/model-checking/kani // Sometimes we want to use lints which were added after our MSRV. // `unknown_lints` is `warn` by default and we deny warnings in CI, so without