Skip to content

Commit

Permalink
Nits in README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
catalin-hritcu committed Sep 16, 2017
1 parent d9fc094 commit 6ed275f
Showing 1 changed file with 11 additions and 11 deletions.
22 changes: 11 additions & 11 deletions README.md
Expand Up @@ -2,7 +2,7 @@ HACL*
=====

HACL* is a formally verified cryptographic library in [F\*],
developed by the [Prosecco](http://prosecco.inria.fr) team in
developed by the [Prosecco](http://prosecco.inria.fr) team at
[INRIA Paris](https://www.inria.fr/en/centre/paris) in collaboration
with Microsoft Research, as part of [Project Everest].

Expand All @@ -12,7 +12,7 @@ The goal of this library is to develop verified C reference implementations
for popular cryptographic primitives and to verify them for memory safety,
functional correctness, and secret independence.

More details about the library and its design can be found in our ACM CCS 2017 research paper:
More details about the HACL* library and its design can be found in our ACM CCS 2017 research paper:
https://eprint.iacr.org/2017/536

All our code is written and verified in [F\*] and then compiled to C via
Expand Down Expand Up @@ -50,7 +50,7 @@ appears in the IEEE S&P 2017 paper: https://eprint.iacr.org/2016/1178.pdf
[NaCl API]: https://nacl.cr.yp.to
[libsodium]: https://github.com/jedisct1/libsodium
[Project Everest]: https://github.com/project-everest

[secure_api/]: https://github.com/mitls/hacl-star/tree/master/secure_api

# Warning

Expand Down Expand Up @@ -95,20 +95,20 @@ If you want to verify the F* code and regenerate the C library:
- 'make clean' will remove all artifacts created by other targets
```

Verification and C code generation requires F* and KreMLin.
Benchmarking performance in `test-all` requires OpenSSL and Libsodium.
Verification and C code generation requires [F\*] and [KreMLin].
Benchmarking performance in `test-all` requires [openssl] and [libsodium].
An additional CMake build is available and can be run with `make build-cmake`.


# Performance

To measure see the performance of HACL* primitives on your platform and C compiler,
run the targets from `test/Makefile` if you have dependencies installed. (experimental)
To compare its performance with the C reference code (not the assembly versions) in libsodium and openssl,
run the targets from `test/Makefile` if you have the dependencies installed. (experimental)
To compare its performance with the C reference code (not the assembly versions) in [libsodium] and [openssl],
download and compile [libsodium] with the `--disable-asm` flag and [openssl] with the `-no-asm` flag.

While HACL* is typically as fast as hand-written C code, it is typically 1.1-5.7x slower than
assembly code in our experiments. In future, we hope to close this gap by using verified assembly implementations
assembly code in our experiments. In the future, we hope to close this gap by using verified assembly implementations
like [Vale](https://github.com/project-everest/vale) for some primitives.

[openssl]: https://github.com/openssl/openssl
Expand All @@ -122,15 +122,15 @@ The [code/experimental](code/experimental) directory includes other (partially v
* MACs: GCM
* Key Derivation: HKDF

We are also working on a JavaScript backend to F* that would enable us to extract HACL* as a JavaScript library.
We are also working on a JavaScript backend for F* that would enable us to extract HACL* as a JavaScript library.


# Authors and Maintainers

HACL* was originially developed as part of the Ph.D. thesis of Jean Karim Zinzindohoué
at the [Prosecco](http://prosecco.inria.fr) team at [INRIA Paris](https://www.inria.fr/en/centre/paris).
in the [Prosecco](http://prosecco.inria.fr) team at [INRIA Paris](https://www.inria.fr/en/centre/paris).
It contains contributions from many researchers at INRIA and Microsoft Research, and is
being actively developed and maintained within [Project Everest].
being actively developed and maintained within [Project Everest].

For questions and comments, or if you want to contribute to the project, do contact the current maintainers at:
* Benjamin Beurdouche (benjamin.beurdouche@inria.fr)
Expand Down

0 comments on commit 6ed275f

Please sign in to comment.