Object aliasing violations are not detected

[danielsn]

Rust requires that the borrow checker rules be enforced at all times, including in unsafe code. We do not currently have any checks for this in RMC.

Likelihood:

If code contains this bug, RMC will not detect it. We have manually found at least one possible instance of this case in Firecracker. We do not have any data as to how often this occurs in practice.

Mitigation:

• Warn users that this class of UB is outside the current scope of RMC.

Path to soundness:

• Add a check for this, likely based off the “stacked borrows” work.

Documentation:

https://plv.mpi-sws.org/Rustbelt/stacked-borrows/

[zhassan-aws]

This is more of a feature request to implement stacked borrows.