RMC aims to be a bit-precise model checker for Rust. It would be useful to check if it can detect bugs previously found by the community in the Rust Standard Library. A possible way to go about this would be to pick up a version of the library before and after then change and test the vulnerable example.

This issue aims to track this exercise. Some initial CVEs which might be interesting to look at are :

• Buffer Overflow vulnerability in std::collections::vec_deque::VecDeque::reserve() CVE-2018-1000657
• Use-after-free or double free in VecDeque CVE-2020-36318

Repository with Rust CVEs: Link