Open oberstet opened 8 years ago
This looks great (it generates formally verified C which we could reuse / expose):
This repository contains verified code for a library of modern cryptographic algorithms, including Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC, and HKDF. This set of algorithms is enough to support the full NaCl API and several TLS 1.3 ciphersuites. The code for all of these algorithms is formally verified using the F* verification framework for memory safety, functional correctness, and secret independence (resistance to some types of timing side-channels).b
Not a short term goal, but it would be awesome to have WAMP-cryptosign (and possibly WAMP-cryptobox) in AutobahnC later.
Besides NaCl/libsodium, look at these: