Does formal verification protect against buffer overflows? (it's a serious question)
Author here: No, symbolic verification does not protect from buffer overflows. Writing the implementation in Rust does
We are investigating ways how to do more formal verification for the implementation itself.
> No, symbolic verification does not protect from buffer overflows. Writing the implementation in Rust does
I don't believe writing the implementation in Rust does that: https://blog.rust-lang.org/2018/09/21/Security-advisory-for-...
One would think that this would be fixed in the last five years?
Certainly. What I don't believe is certain is that only one such vulnerability has ever existed and none exist in Rust today.
It's not pedantic to differentiate between mitigating a thing and preventing a thing.
You can add `#![forbid(unsafe_code)]` to your codebase to avoid any unsafe Rust, which should prevent buffer overflows. Obviously it may make writing a codebase somewhat harder.
Will that restriction also be applied transitively to all dependencies?