Revision d30f091b98e9011773843299351a7360e114e1aa authored by Benjamin Beurdouche on 04 December 2019, 13:52:46 UTC, committed by Benjamin Beurdouche on 04 December 2019, 13:52:46 UTC
1 parent b3243e9
README.md
# High Performance Verified Cryptographic Code
This repository contains code from several related projects developed as part of
[Project Everest](https://project-everest.github.io/), which aims to build and
deploy a verified HTTPS stack.
We are actively developing and integrating our code on the
[fstar-master](https://github.com/project-everest/hacl-star/tree/fstar-master/)
branch, which tracks F\*'s `master` branch. See
[releases](https://github.com/project-everest/hacl-star/releases) for a preview
of our C and assembly code, including EverCrypt 0.1 (currently in **alpha**).
## HACL\*
[HACL\*](README.HACL.md), the High-Assurance Cryptographic Library, is a
formally verified cryptographic library in [F\*](https://www.fstar-lang.org).
The goal of this library is to develop highly efficient, pure C implementations
for popular cryptographic primitives and to verify them for memory safety,
functional correctness, and secret independence.
## Vale-Crypto
[Vale-Crypto](README.Vale.md) provides formally verified high-performance
cryptographic code in assembly language. It relies on the
[Vale tool](https://github.com/project-everest/vale) to produce
code and proofs in [F\*](https://github.com/FStarLang/FStar). Vale supports
multiple platforms and proves that its implementations are memory safe,
functionally correct, and that timing and memory accesses are secret
independent.
## EverCrypt
[EverCrypt](README.EverCrypt.md) is a high-performance, cross-platform, formally
verified modern cryptographic provider. EverCrypt packages implementations from
HACL\* and Vale-Crypto, and automatically picks the fastest one available,
depending on processor support and the target execution environment
(*multiplexing*). Furthermore, EverCrypt offers an (*agile*) API that makes it
simple to switch between algorithms (e.g., from SHA2 to SHA3).
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...