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

[joshlf]

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).

[briansmith]

In issue #716, @ijackson asked for a postmortem (my characterization) which I think would be useful as part of this effort.

I think it's also important to look at how the CVE/RUSTSEC advisory and yanking for #716 affected many crates that depend on ahash (and probably other crates that depend on zerocopy), even though almost none of them had a real impact due to #716 since they weren't using the affected API in an affected way (AFAICT), but vulnerability scanning / advisory response software available to us isn't advanced enough to "see" that. The cost of these kinds of false-positive external impacts need to be accounted for in some way. I haven't seen this aspect mentioned elsewhere.