Sites Inria

Version française

Recherche

Team: PROSECCO -

HACL*

HACL*

We demonstrate HACL*, a verified cryptographic library written in F* and compiled to C. Verification guarantees that our code is memory safe, functionally correct, and free from integer overflows and certain kinds of side-channel leaks. We rely on Kremlin, a compiler from F* to C with formal correctness guarantees  and on CompCert a verified compiler for C. We demonstrate the usage of our library to build a file transfer application and a reference TLS library.

Team:  PROSECCO

Website :  https://github.com/mitls/hacl-star

Keywords: Proof Security Verification Cryptography Transport Layer Security

Top