Skip to main content

Browse the archive

Revision 855bc8b8f798a6734b8e90f2b2190327f7769105 authored by Jay Bosamiya on 11 June 2019, 21:33:57 UTC, committed by Jay Bosamiya on 11 June 2019, 21:33:57 UTC 
Fix up [lemma_locations_complete]. See msg.
 
Previously, we had an assumption in proof of
[lemma_locations_complete] that was unprovable since it was false. By
refining the statement that the lemma proves, we no longer need this
false assumption, and are able to prove things. This does come with
the additional cost of a few "observe" assertions in the
[InstrReordering] proofs, but all is well and good :)
1 parent f3ec0c6
Raw File
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).
back to top