Representation of DSTs and fat pointers

[danielsn]

Rust allows user-defined objects to contain a single dynamically sized field, similar to how C supports flexible arrays as the final field of a struct. Although this feature is not conceptually complicated, its implementation involves many corner cases.

Likelihood:

We have repeatedly run into cases where new RMC tests failed due to unexpected corner-cases involving dynamically sized objects. We have solved all known issues, but the rate of bug discovery in this area to date suggests that there are additional latent bugs.

Mitigation:

• The CBMC type-system has been effective in detecting issues caused by incorrectly handling dynamically sized objects.

Path to soundness:

• Develop a detailed doc formally specifying how Rust handles dynamically sized types.
• A full audit of the responsible code, ideally with a member of the Rust compiler team

[zhassan-aws]

Mostly mitigated other than #327

[celinval]

@zhassan-aws can we close this one now?

[zhassan-aws]

Yes