|
|
|
|
|
|
by catalin_hritcu
3153 days ago
|
|
|
One can always look at the empty part of the glass, but the quote does continue with a big full part: "The TLS 1.3 handshake verification is work in progress and still relies on the OCaml extraction mechanism of F* ; thus, the C library still encapsulates the OCaml runtime system. We have completed verification of the TLS 1.3 record layer it currently extracts to C. The AES and SHA2 cryptographic assembly routines are verified and extract to assembly via Vale. HaCl* provides verified C code for multiple other primitives such as Curve25519, Chacha20, Poly1305 or HMAC. Our test client implements TLS 1.2 + TLS 1.3 Draft 18 and successfully connects to TLS 1.3 test servers. We have a prototype integration of miTLS within libcurl that one can use to git clone a remote repository." |
|
|