This directory contains the Vale cryptographic libraries, i.e., formally verified high-performance cryptographic code in assembly language. They rely on the Vale tool to produce code and proofs in F*.
The code currently targets x64, but it will be expanded to support other hardware platforms, such as x86 and ARM. Our toolchain produces assembly that is suitable for Windows, Mac, and Linux, and that is compatible with both MSVC and GCC based toolchains.
Vale is part of the Everest project, which aims to build and deploy a verified HTTPS stack.
See the INSTALL file for installing Vale and its dependencies.
See the CODE file for more details on the various files in this directory.
You can see our academic papers describing Vale:
-
Vale: Verifying High-Performance Cryptographic Assembly Code
Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson. In Proceedings of the USENIX Security Symposium, 2017. Distinguished Paper Award -
A Verified, Efficient Embedding of a Verifiable Assembly Language
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy. In Proceedings of the Symposium on Principles of Programming Languages (POPL), 2019.
Our Vale code is licensed under the Apache license in the LICENSE file.
- v0.2: Vale/F* code release.
- v0.1: Initial code release, containing code written by: Andrew Baumann, Barry Bond, Andrew Ferraiuolo, Chris Hawblitzel, Jon Howell, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson.