Why would you need a static analyzer for a language that promotes itself as safe out of the box.
Safe Rust is memory safe and data race safe. There are other forms of safety obviously, like overflow safety, numerous forms of confidentiality and security properties, etc.
Rust checks integer overflows at runtime (or not at all, if building for maximum speed). It is safer than not checking at all. But costs performance and can lead to (predictable) crashes.
This tool is a way to prove that overflows can not happen at compile time. Which is extremely hard in the general case.
Unless it overflows all the way to a valid index. Which might lead to unexpected results if the code does not expect to be using a smaller index (for instance, a code trying to access index i+2 might not be expecting it to suddenly access indexes 0 or 1).
The remaining 30% still need to be tracked down.
And from Google[1]: "memory safety bugs continue to be a top contributor of stability issues, and consistently represent ~70% of Android’s high severity security vulnerabilities."
[0] https://msrc-blog.microsoft.com/2019/07/22/why-rust-for-safe...
[1] https://security.googleblog.com/2021/04/rust-in-android-plat...
It's actually a formal verification tool. They call it a "static verifier" not a "static analyser".
Most static analysis tools seek to find potential problems in your code - generally common mistakes - but they aren't proving anything usually. They have false positives and negatives. Formal verification requires you to write properties about your code and then it proves it.
- Prusti does not require you to write any "properties". I just ran it on a piece of code, which has no annotations for Prusti, and it still found a potential integer overflow. Maybe it has some internal annotations for std, but none for my code.