diff --git a/README.md b/README.md index d9d3d907d23..f12534f7167 100644 --- a/README.md +++ b/README.md @@ -86,6 +86,31 @@ for network parsing. [simd-layout]: https://rust-lang.github.io/unsafe-code-guidelines/layout/packed-simd-vectors.html +## Zerocopy's Ethos + +Much like cryptographic primitives, `unsafe` Rust is a fractal of +security-critical subtleties. Absent hundreds of engineering hours of expert +scruitiny, `unsafe` can silently introduce undefined behavior into your +codebase. We have invested those engineering hours so you don't need to. + +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` with a precise rationale for its soundness that + quotes a relevant section of the 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 62005ad6a68..4f8f5d1234e 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -84,6 +84,31 @@ //! may be removed at any point in the future. //! //! [simd-layout]: https://rust-lang.github.io/unsafe-code-guidelines/layout/packed-simd-vectors.html +//! +//! # Zerocopy's Ethos +//! +//! Much like cryptographic primitives, `unsafe` Rust is a fractal of +//! security-critical subtleties. Absent hundreds of engineering hours of expert +//! scruitiny, `unsafe` can silently introduce undefined behavior into your +//! codebase. We have invested those engineering hours so you don't need to. +//! +//! 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` with a precise rationale for its soundness that +//! quotes a relevant section of the 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