We aim to make the following promise: zerocopy and any code produced by zerocopy-derive are sound on any supported toolchain/target, and will remain sound under any future compiler changes; in other words, this soundness is forwards-compatible.

This issue tracks all efforts related to proving that we uphold this guarantee, preventing regressions, documenting this guarantee, and ensuring that our documentation properly frames zerocopy's role in the broader Rust safety ecosystem.

As of this writing, there are a few known gaps:

We prove our soundness in terms of the Rust reference and stdlib docs, and these docs are wrong on some target architectures (see #383). We don't intend to do anything about this in the short-term other than document that it's a gap.
While Rust's memory model for pointer operations will likely never be stricter than "strict provenance", this isn't actually guaranteed. While we're currently compliant with strict provenance, we can't say that that's sufficient for complete forwards-compatible soundness until this is a guarantee provided by the reference. See #181 for more details.
- In terms of how we message this, we have two options:
- Document that we "aim to be" sound under any future compiler version, and cite our adherence to strict provenance as an example of this work.
- Don't mention soundness under any future compiler version, and just cite our adherence to strict provenance as general evidence of how seriously we take soundness.
As written, our custom derives can be "tricked" into emitting unsound code (#388).
It may be possible to use the trivial_bounds feature to break our derives (#500).

Safety comments

429 tracks ensuring that each `unsafe` block is annotated with a safety comment that proves its soundness, and that these proofs are anchored only on guarantees made by the reference or stdlib docs.

Strict provenance

181 tracks abiding by "strict provenance", which is a model for pointer operations which is likely as strict as any future Rust memory model will be.

Formal modeling/verification

378 tracks using formal modeling/verification tools to test or prove the correctness of some of our core algorithms.

Target architectures

Some target architectures have nonstandard semantics which may make some of our soundness arguments invalid. #383 tracks making it clear in our documentation that zerocopy may be unsound on architectures whose semantics fails to satisfy the guarantees provided by the Rust reference and stdlib docs.

Proc macro execution model

As described in #388, there are currently soundness holes in our custom derives. Some have been confirmed, and others have been hypothesized but not confirmed. This issue tracks identifying the remaining soundness holes and fixing them.

`trivial_bounds`

As described in #500, it may be possible to use the trivial_bounds feature to break our derives.

Document our security "ethos"

482 tracks documenting our security "ethos" - the approach we take to ensuring that our code is correct and secure.

Document our relationship to the Safe Transmute project

480 tracks documenting the relationship between zerocopy and the Rust project's Safe Transmute project.

Use Safe Transmute in our custom derives (behind a feature flag)

481 tracks allowing users to opt-in to our derives only supporting types which pass both our analysis and the analysis implemented by the (unstable) `BikeshedIntrinsicFrom` feature (the placeholder name for the analysis implemented by the Safe Transmute project).

google / zerocopy

Tracking issue for proving soundness, preventing regressions, and documenting security ethos #61

Safety comments

429 tracks ensuring that each `unsafe` block is annotated with a safety comment that proves its soundness, and that these proofs are anchored only on guarantees made by the reference or stdlib docs.

Strict provenance

181 tracks abiding by "strict provenance", which is a model for pointer operations which is likely as strict as any future Rust memory model will be.

Formal modeling/verification

378 tracks using formal modeling/verification tools to test or prove the correctness of some of our core algorithms.

Target architectures

Proc macro execution model

`trivial_bounds`

Document our security "ethos"

482 tracks documenting our security "ethos" - the approach we take to ensuring that our code is correct and secure.

Document our relationship to the Safe Transmute project

480 tracks documenting the relationship between zerocopy and the Rust project's Safe Transmute project.

Use Safe Transmute in our custom derives (behind a feature flag)

481 tracks allowing users to opt-in to our derives only supporting types which pass both our analysis and the analysis implemented by the (unstable) `BikeshedIntrinsicFrom` feature (the placeholder name for the analysis implemented by the Safe Transmute project).

google / zerocopy

Tracking issue for proving soundness, preventing regressions, and documenting security ethos #61

Safety comments

429 tracks ensuring that each unsafe block is annotated with a safety comment that proves its soundness, and that these proofs are anchored only on guarantees made by the reference or stdlib docs.

Strict provenance

181 tracks abiding by "strict provenance", which is a model for pointer operations which is likely as strict as any future Rust memory model will be.

Formal modeling/verification

378 tracks using formal modeling/verification tools to test or prove the correctness of some of our core algorithms.

Target architectures

Proc macro execution model

trivial_bounds

Document our security "ethos"

482 tracks documenting our security "ethos" - the approach we take to ensuring that our code is correct and secure.

Document our relationship to the Safe Transmute project

480 tracks documenting the relationship between zerocopy and the Rust project's Safe Transmute project.

Use Safe Transmute in our custom derives (behind a feature flag)

481 tracks allowing users to opt-in to our derives only supporting types which pass both our analysis and the analysis implemented by the (unstable) BikeshedIntrinsicFrom feature (the placeholder name for the analysis implemented by the Safe Transmute project).

429 tracks ensuring that each `unsafe` block is annotated with a safety comment that proves its soundness, and that these proofs are anchored only on guarantees made by the reference or stdlib docs.

`trivial_bounds`

481 tracks allowing users to opt-in to our derives only supporting types which pass both our analysis and the analysis implemented by the (unstable) `BikeshedIntrinsicFrom` feature (the placeholder name for the analysis implemented by the Safe Transmute project).