VeriFrodo is an implementation of FrodoKEM-640-SHAKE in Jasmin accompanied by correctness proofs in EasyCrypt.
Jasmin is an assembly-like programming language with a view to making programs written in it amenable to formal verification. The assembly-like syntax means programmers control many low-level details that are performance-critical, such as instruction selection and scheduling, what registers to spill and when, etc.
The Jasmin compiler is formally verified and transforms source code to x86-64 assembly. Jasmin programs can also be automatically checked for safety and termination using a bundled static analyzer.
Jasmin leverages the EasyCrypt proof assistant for formal verification: Jasmin source can be extracted to the corresponding EasyCrypt, thereby making it possible to prove functional correctness, cryptographic security, and security against side-channel attacks.
FrodoKEM is a post-quantum key encapsulation algorithm whose security is based on the Learning with Errors (LWE) problem. VeriFrodo is an implementation in Jasmin of FrodoKEM-640-SHAKE, an instantiation that uses SHAKE128 and has 128-bit security. This Jasmin code is accompanied by correctness proofs in EasyCrypt.
-
Ensure your Docker installation is able to use at least 5 GB of memory.
-
To build and test the code, run:
docker build -t verifrodo-test .Contributions are gratefully welcomed. See the list of good first issues for ideas.