Santiago Zanella-Beguelin
Santiago Zanella-Beguelin
`OpKDF` targets use `malloc` to allocate arbitrarily large chunks of memory upfront to store the output of `EVP_PKEY_derive`, but `EVP_PKEY_derive` may fail without every using that memory because the requested...
Commit afe04c947f55a81f48af6c4e99d4b0bd5abee488 weakens the preconditions of Diffie-Hellman functions on P-256. I didn't think that change would spark such a heated debate, because: 1. the extracted code is identical; 2. it's...
Hi there, With reference to #35, I realized that the hacl-star is not the same as the `fstar-master` branch, and is most likely the `master` branch. Is there anyway to...
Conditionals that branch on a boolean variable marked as `@CIfDef` may extract to code that redefines variables. ```FStar [@CIfDef] assume val b : bool assume val f : unit ->...
The following program outputs `z = 255` despite `assert (z == 1uy)` being provable in F*: ```F# module M open FStar.HyperStack.All open FStar.UInt8 val discard: bool -> St unit let...
This adds support for verification of modules in `mitls-fstar` without having to first build `hacl-star`. The trick is to verify dependencies in `hacl-star`, if needed, without `providers/evercrypt/fst` in scope. The...
We want to implement a unified Multistream API atop EverCrypt AEAD that can be used for both QUIC and TLS. Requirements: - Algorithm agility - Support for QUIC packet number...
# Requirements We need to maintain a table of connections, mapping a unique connection ID to the connection state. Each connection evolves monotonically according to the reflexive transitive closure of...
We should have a target for testing the health of our test client and server, and their interoperability with OpenSSL. We need to cover at least these scenarios, initially with...
## 🐛 Bug The `__len__()` method of a `BatchSplittingSampler` that wraps a `DPDataLoader` is meant to return the number of physical (as opposed to logical) batches in its iterator. Because...