EverCrypt alpha2

[msprotz]

⚠️⚠️⚠️
always close the page then reopen it before editing this issue
⚠️⚠️⚠️

List of tasks for EverCrypt alpha2 and beyond:

(previously: #145)

• AES-CTR (Bryan)
  • exposing Low* interfaces + spec in specs/ (Aymeric)
• how about longer IVs for AES-GCM?
• ed25519 (Team-Karthik)
  • SHA2-512 callable from HACL-lib-style code (Jonathan)
  • an unverified prototype that computes proper results
  • prototype rewritten to get the performance we want
  • memory safety
  • integrate and ditch old code (Christoph)
  • two assumes added while integrating to fix (should be trivial) (Jonathan)
  • functional correctness (Aymeric)
• more idiomatic C code (Jonathan)
  • move lib/c/evercrypt_targetconfig.h to providers/evercrypt/c
  • unify error codes into a single EverCrypt.Error type? (Jonathan)
  • Feature request: DExtern should support names for parameters, not just types FStarLang/karamel#9 -- otherwise evercrypt-external-header is unusable (Jonathan)
  • unified order of arguments across evercrypt (Jonathan)
    • Antoine to come up with a proposal
  • abstract interface on top of EverCrypt.Hash.Incremental
  • restore C abstract structs and put it under CI to make sure it doesn't regress again
• merge poly1305 spec equivalence proof (Marina)
  • merge on fstar-master
  • remove Aymeric's proof and use the generic one instead
  • fix EverCrypt.Poly1305 calls
• missing proofs
  • pesky constant-time carry (?)
  • three endianness assumes (Marina)
  • Lib admits: Lib.Buffer.fst (1) + Lib.ByteSequence (1)
  • Admits left in SHA_helpers.fst(i) (Chris)
  • MerkleTree.New.High.Correct.Rhs.fst (Joonwon, can anyone help?)
• fragile proofs (Marina redid poly specs)
  • Hacl.Spec.Poly1305.Equiv.fst(301,21-301,33): (Error 19) Subtyping check failed
  • Hacl.Impl.Poly1305.fst(365,27-365,29): (Error 19) Subtyping check failed
  • Vale.AsLowStar.Wrapper.fst(431,4-453,9): (Error 19) could not prove post-condition (Jonathan)
• performance (C) tests (Christoph)
  • clean up C tests to be reusable, then measure Curve25519, Poly1305, Chacha20Poly1305, AES-GCM (128+256), hash, HMAC, HKDF
  • multiple test vectors to avoid spurious optimizations for a single test input
  • compare perf against OpenSSL; BCrypt; "rfc" (https://github.com/armfazh/rfc7748_precomputed)
  • have tests go through both the "direct C" API and EverCrypt APIs to measure the cost of multiplexing (but beware of illegal instruction errors)
    • lift aesgcm-encrypt and aes-gcm-decrypt as separate standalone C functions in EverCrypt.AEAD, just like for key expansion (Jonathan)
  • generate performance graphs automatically in CSV
  • a top-level test driver (in python) that runs all desired / available combinations of C compiler / flags
  • put them under CI and make sure they're compiled (Tahina)
• functional (Low*) tests (Tahina)
  • use auto-generated Test.Vectors.Chacha20Poly1305; do the same for AES-GCM
  • test vectors for SHA3
  • understand how to make sure we get all the coverage we want
  • test_chacha20poly1305 direct through EverCrypt.Chacha20Poly1305
  • negative tests for Curve
  • much more test vectors / put their generation as a build step rather than putting the generated files under version control
  • spec tests: AEAD, Poly1305, Curve25519, etc. possibly using the tool to generate test vectors for spec
• HMAC and HKDF specs moved to the specs/ directory and made Tot instead of GTot (Jonathan)
• EverCrypt.AEAD: abstract footprint and the whole shebang (Jonathan) + idiomatic destination-address key expansion (rename to: create_in)
• EverCrypt.Poly1305: use the same tricks as AES-GCM to pass an extra buffer with the right size for the last few bits of data to avoid copying the entire input (Chris)
• EverCrypt.Cipher: stateful API with footprints for Chacha20 & AES-CTR (Jonathan)
  • Agile CTR spec (Karthik)
  • land Agile CTR on fstar-master (Jonathan)
  • confirm it works (Antoine)
  • implement EverCrypt.Cipher using Spec.CTR (Jonathan)
  • tests (?)
  • move chacha20 to EverCrypt.Chacha20 (Jonathan)
• do we want to offer individual algorithms, standalone when they are already covered by agile APIs? (EverCrypt.Chacha20Poly1305, EverCrypt.AESGCM)?
• complete the implementation of Lib.IntTypes using FStar.ConstantTime.Integers (Santiago) (FStar.ConstantTime.Integers abandoned)
• integrating hashes
  • pass CI on Karthik's branch
  • take a look at the shortcomings of Lib.IntTypes (Nik)
  • how to make hashes use constbuffer?
• integrate sha3 into EverCrypt
  • update agile hash specs to take into account SHA3 & fix spec predicates such as maximum length (there's none for SHA3) (Santiago)
  • modify specs of sha2, sha1 and md5 to be in terms of constant-time integers, for compatibility with sha3 (done on _dev) (Karthik)
  • if item above skipped, we can friend Lib.IntTypes in EverCrypt.Hash and leave switching agile hash specs to FStar.ConstantTime.Integers later on
• EverCrypt interface for chacha20poly1305
• speed improvements
  • chacha20poly1305 optimized (tiled?) (ask Cédric)
  • Optimised AES-GCM decryption (Bryan)
• bringing Hash and AEAD to the latest style of stateful invariants (Tahina)
  • merge hash invariants into a single one
  • move useful helpers (loc_not_in, etc.) to ulib
  • add patterns (taking inspiration from HSL.Transcript) for framing lemmas (Jonathan, on Hash Incremental only... since this is expected to be the entry point)
• auto-generated OCaml bindings
• compilation to aarch32 and aarch64 under CI (cross-compiling from Linux ?)
• code that works on non-x64 platforms
• WebAssembly version (Jonathan)
  • WASM compilation of unions in KreMLin
  • implement general treatment of top-level constants including arrays of structures, with static layouts in the data segment and load-time initializers for symbol locations determined at WASM module load-time
  • implement missing desugarings
  • separate stack-based tests into a separate module in EverCrypt + verify these Low* tests
  • run and add tests to CI (hashes)
  • figure out why there's a void* in the generated test code (drive-by fix)
  • run and add tests to CI (poly1305, chacha20poly1305, curve25519, chacha20)
• Curve25519 API that does not use HACL* buffers; use same trick as Poly1305?
• see if we can convert frozen_preorder into immutable_buffer (Aseem, Nik, Tahina?) (switched to regular abstract stateful predicate)
• /Users/jonathan/Code/hacl-star/code/curve25519/Hacl.Spec.Curve25519.Field51.Lemmas.fst(917,2-934,35): (Error 16) Unknown assertion failed proof is not robust and platform-dependent (Jonathan)
• figure out why SHA-EXT doesn't work on the chromebook we have ssh access to (Jonathan)

Alpha3

• come up with a plan to get rid of random number generation and have fallbacks for ECDH and DH -- need to remove EverCrypt.fsti!
  • use and clean up Karthik's code that links onto system interfaces (Jonathan)
  • review Lib_RandomBuffer.c (Antoine)
  • add HMAC-DRBG on top of it (Antoine)
• const pointers (Jonathan)
  • write LowStar.ConstBuffer (Nik)
  • implement support for LowStar.ConstBuffer in F*
  • implement support for LowStar.ConstBuffer in KreMLin
  • experiment with hashes see if we can use this
  • chat with Karthik and understand how this relates to Lib.Buffer
• propagate preconditions on X64.avx2 everything in HACL*, starting from Lib.IntVector and up through its callers

For later.

• quic_provider in C (Antoine)
  • need AES-CTR and AES-EBC with proper specs (see above)
  • memory safety
  • functional correctness
  • integration with benchmarks for packet encryption on top of the QUIC implementation
  • full packet encryption and crypto modeling ("stretch goal")
• rewire HACL* libraries to use LowStar.Endianness
  • extend FStar.Endianness with more facts inspired from Hacl.Impl.Poly1305.Lemmas, e.g. le_to_n (append s1 s2) = le_to_n s1 + le_to_n s2 * pow2 (length s1 * 8)(or whatever is correct)
  • missing nat_from[to]_bytes[intseq]_le and uints_from[to]_bytes_le in Lib.ByteSequence, see leftover assumes in poly1035 to see which ones are missing
  • specify total byte-swapping operations
• specifications using cryptographic constructions
  • higher-order specs for CTR (done), PRF and MAC
  • spec-equivalence proofs between HACL* new specs and higher-order specs
  • switch AEAD spec to use the higher-order ones
• abstract idealization over the opaque AEAD spec (Santiago and/or Cédric) -- the mythical switch?
• review multiplexing style that is local to HACL* and investigate one based on type classes, possibly automated with tactics (Jonathan)
  • chacha20poly1305 parameterized over poly1305 and chacha20 using that style
• spec equivalence proof for curve25519 re. "pure" mathematical specification
• Refactor Vale taint analysis (Aymeric)
• a mountain of: (Warning 271) Pattern Lib.Sequence.index s i contains illegal sub-term ((ite (is-Hacl.Impl.Poly1305.Fields.M32 (BoundV 0)) (BoxInt (Integer 1)) (ite (is-Hacl.Impl.Poly1305.Fields.M128 (BoundV 0)) (BoxInt (Integer 2)) (ite (is-Hacl.Impl.Poly1305.Fields.M256 (BoundV 0)) (BoxInt (Integer 4)) (Tm_unit ))))); dropping it (see also /home/jonathan/Code/hacl-star/lib/Lib.Sequence.fsti(49,14-49,25))
• three assume in Hacl.Test.SHA3.fst; this is benign
• using the fully specification of the tot functions, write a model for LowStar.Endianness, and hide it behind an fsti
• proof performance improvements

Missing algorithms:

• AES-CBC (eventually)
• AES-GCM / C (who?)

[msprotz]

Reviewing this with @polubelova and @R1kM

• order of arguments tracked in a separate isue (Define a consistant API #675)
• no need to move evercrypt_targetconfig.h
• tests handled in hacl-packages, all issues are obsolete
• no desire to offer multiplexing non-agile APIs in EverCrypt
• const-correctness tracked in a separate issue (Use LowStar.ConstBuffer, all the way up to the top-level EverCrypt APIs #334)
• shortcomings of Lib.IntTypes: several improvements over time
• chachapoly optimization: let's wait until someone asks for it
• endianness: no-op, HACL* is the main customer of those endianness specifications, probably best to leave them in lib/
• Cédric-style crypto specifications with modular combinations of e.g. PRF and MAC to obtain AEAD, along with proofs of equivalence with concrete spec and possibly idealization and switch (in the style of the secure_api of yore): separate project, revive later
• pattern issues: Aymeric to open up a new issue and/or consult with F* team about the best way to fix this
• assumes in tests: not a priority
• model of endianness: also not a priority