4 ms·
WireGuard is a recent and prominent example of a system that has been formally verified (https://www.wireguard.com/formal-verification/ https://www.wireguard.co
by raggi 4y ago
WireGuard is a recent and prominent example of a system that has been formally verified (https://www.wireguard.com/formal-verification/ https://www.wireguard.com/formal-verification/). There are implementations in a variety of languages due to integration considerations.
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.
- ShredKazoo 4y agoOut of curiosity did the Wireguard formal verification effort end up identifying any security issues in the implementation?
- harry8 4y agoNow 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?
- KMag 4y agoThe 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.