Snapshots, architectures, audits, validation, and verification of crypto libraries
Source snapshots are all in the src directory. They are orgranized by language then library, then version directories. Our goal for snapshots is breadth. Please let us know if there is anything that we are missing!
Quick audits of some of the libraries in AUDITS.md.
BON specifications for the hacrypto library can be found in the arch folder, along with a HTML view of the architecture, and generated tests.
The TestGen contains a project that generates test cases and harnesses for crypto libraries. A primary goal is to generate CAVP tests and hopefully find some insufficiencies in the testing.
The Verification/VST/sha folder contains experiments with building, calling, and running frama-c value analysis on SHA256 implementations from NSS, Sodium, and a macro expanded and verified in Coq OpenSSL.