Although the use of `unsafe` blocks is not uncommon in Rust crates, writing sound `unsafe` code remains difficult. There are numerous obligations that programmers must fulfill, many of which are easy to overlook, leading to bugs that are difficult to detect. We have extended *VeriFast*, a verification tool based on *modular symbolic execution*, to verify that Rust's safety guarantees hold in programs containing `unsafe` blocks. Using this tool, we have successfully verified approximations of several well-known, fundamental components from Rust's standard library, along with other examples, all of which make use of `unsafe` code.
0 commit comments