Re:Memory Safe Languages in Android 13
by ShredKazoo on Thursday December 01, 2022 @10:39PM
(#33826470)
Out of curiosity did the Wireguard formal verification effort end up identifying any security issues in the implementation?
Now that is interesting. I didn't know that and will have to look further to understand what it means.
Wireguard seems to be written almost entirely in C, is that right?
The symbolic proofs of the protocol are independent of the implementation. The portions of the implementation that are formally verified are written in F* and Coq, and emitted as machine-generated C.
You will find at the bottom of that page C implementations of curve25519 that are proofed and derived from F* and Coq. Curve25519 is a relatively simple implementation and only one part of any system that uses it. As you can see in both of these implementations the papers recognize a team of contributors each - this should provide some insight as to the cost of such work. That doesn't make it unimportant, it just makes it rare.