3 ms·
Maybe not in general, but there is really interesting work happening in the area of verified protocols generating safe C code (memory safe, overflow safe, timin
by thadt 4y ago
Maybe not in general, but there is really interesting work happening in the area of verified protocols generating safe C code (memory safe, overflow safe, timing safe, etc). In particular Project Everest has a set of verified primitives underlying higher level protocols like TLS and more recently all Noise variants (https://eprint.iacr.org/2022/607 https://eprint.iacr.org/2022/607).
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?
- api 4y agoAFAIK Wireguard is just Noise_IK as an IP tunneling protocol. 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.