Does formal verification protect against buffer overflows? (it's a serious question)
The question is too broad to be answered, there are many different formal verification techniques (including static formal verification techniques, and also dynamic formal verification techniques which happen at runtime), and you could be formally verifying only specific properties of the system.
Now, if your formal verification technique forces you to check that each index you use is within bounds (for instance, by forcing you to write loop invariants for each loop, but that's not sufficient because you can index buffers outside a loop or with something unrelated to the loop invariant), then yes, you have proved that you will not overflow buffers.
But those pesky implementations are always imperfect and never totally proved correct, what's more they run on pesky hardware which could have flaws and which is usually not itself perfectly verified, so…
And then you have model checking, which is also a formal verification technique. You can prove that you won't overflow buffers… in the model (which is a spec). That proves that your spec is sound and that you can implement it without flaws, but it does not actually check that your implementation is correct, of course. Unless your model checking tool can also build the implementation and this feature is proved correct.
edit: it seems my model checking paragraph is more relevant than I expected, this submission is actually about model checking if it checks the protocol (and not the implementation).
We are investigating ways how to do more formal verification for the implementation itself.
I don't believe writing the implementation in Rust does that: https://blog.rust-lang.org/2018/09/21/Security-advisory-for-...
It's not pedantic to differentiate between mitigating a thing and preventing a thing.
sigh, not true.
https://tgrez.github.io/posts/2022-06-19-buffer-overflow-in-... https://shnatsel.medium.com/how-rusts-standard-library-was-v... "This is a buffer overflow bug in the standard library’s implementation of a double-ended queue." "Rust will panic if you attempt to write out of bounds."
Writing the implementation will increase memory safety but only if the implementation adheres strictly to safe Rust - which means even avoiding ANY packages that use unsafe features. The fact Rust can pull in any package that has an unsafe {} block means you're not promised to be safe.
The equivalent could be said about writing the implementation in JavaScript, Python, etc... (that they protect against buffer overflows)
>It does help make it much less likely.
Yeah... To the same extent as the infamous proof of formal correctness of an example program published in a book, until the program was tested negatively by a student some months later.
It is true though that the underlying unsafe rust in std, or crates or whatnot can have errors though and sometimes we just kind of pretend it's not there since we don't see it.
>The equivalent could be said about writing the implementation in JavaScript, Python, etc... (that they protect against buffer overflows)
This is why we should be encouraging people to write in memory safe languages in general and not just rust or whatever. The overwhelming majority of software does not need to be some super optimized native-code SIMD+AVX1024 beast and would run on something like .net or the JVM, and even Python with no issues. It makes me cringe every time I see some random utils written in C that would work fine in Python.
This is still a pretty neat result! End-to-end proofs from high level protocol to low level implementation are mostly still a research topic.
And CompCert, a formally verified C compiler written in Coq: https://compcert.org/
(even then, there are parts which are not formally verified, mostly at the interfaces with the outside world)
Coq is fairly generic; it has a long history and made it possible to write some really cool proofs such as a proof of the four colors theorem, but writing crypto proofs is really hard using Coq.
For symbolic verification Tamarin and ProVerif are the tools of choice; I used ProVerif.
For proofs of security for protocols EasyCrypt and CryptoVerif can be used. CryptoVerif, ProVerif and Coq where developed at the same Institute by the way; at Inria Paris.
Not sure anyone has published such a multi-layer spec and proof effort /with crypto code in the mix/.
As with any application a small risk of critical security issues (such as buffer overflows, remote code execution) exists; the Rosenpass application is written in the Rust programming language which is much less prone to such issues.
I think their formal analysis is only security/crypto related, at least for the time being.
As WireGuard is based on a Noise construction, it seems reasonable to hope that once formally verified PQ primitives are in place, a fully verified protocol implementation could be generated?
I’ve seen some draft ideas for Noise patterns using Kyber on a slack I am on, but they’d be different since Kyber is a KEM rather than a Diffie-Hellman type construction. Noise is all built around DH.
You can use Kyber alongside Noise in a hybrid construction. Just mix it in with the PSK or something.
Essentially the answer depends on who you ask. For my part I would say both.