Next wave of integration from Vale & HACL*/dev

[msprotz]

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

Hello,

After a somewhat lengthy discussion and a review of all the moving pieces, here is an updated list of tasks and sub-tasks along with tentative assignments. The logistics of this integration effort are as follows:

• all developments to be merged into the branch fstar-master (which posts notifications to #hacl-build); please branch off, get a green, then merge back into this branch -- ask Jonathan for help if CI is acting up
• we are aiming for an alpha release with only inevitable assumes leftover for April 2nd; the short deadline is due to an upcoming blog post & magazine article.

First, a list of completed sub-tasks (thanks to all who participated already!).

• --admit_smt_queries true in lib/Lib.ByteBuffer.fst (line 77 onwards)
• fill_blocks regression in Lib.Buffer.fst (Santiago)
• use right bundling arguments (Jonathan)
• drop old poly1305 (Jonathan)
• two admit() in FastMul_helpers (Chris?)
• two assume(false) in AES128.vaf and AES256.vaf (Chris?)
• numerous occurrences of --admit_smt_queries true in X64.GCMencrypt.vaf and X64.GCMdecrypt.fst (Chris?)
• avx + avx2 CPUID detection (Aymeric)
• modifies_none on cpuid functions to remove an assume in EverCrypt.AutoConfig2 (Jonathan)
• multiplex Poly1305 + drop old call + fix callers (Jonathan)

For alpha1:

• LowStar.Endianness, a library to collect all your endianness-related needs (A unified LowStar.Endianness module FStarLang/FStar#1664) -- please go ahead and push on my branch!
  • monotonic stateful operators (Aseem)
  • fix n_to_le to take nat instead of uint32 (Jonathan)
  • interfaces (Jonathan)
  • kremlin fixes (Jonathan)
  • reveal / opaque (Santiago) (not doing; let's add lemmas instead)
  • one leftover assume (Tahina?) from a proof that regressed
• bringing poly1305, verified libraries from _dev and chacha20 in the same scope
  • backport improved proofs from poly1305 in _dev_combinators into sn_evercrypt_integration (Marina)
  • backport updated libraries from _dev (also in _dev_combinators) (Marina or Santiago)
  • cherry-pick chacha20 from protz_failed_integration and enable it in sn_evercrypt_integration (Marina or Santiago); note: pick files in code/chacha20, specs/Spec.Chacha20.fst, specs/test/Spec.Test.Chacha20.fst, then it suffices to add chacha20 in Makefile.common https://github.com/project-everest/hacl-star/blob/sn_evercrypt_integration/Makefile.common#L22
  • fix chacha20 proof regressions
  • once verification is going through, fix Makefiles, linking, distribution, packaging (Jonathan)
  • once this is done, rewire EverCrypt to use the new chacha20, with the understanding that the old one will remain for old-chacha-poly purposes until Aymeric comes in (see below) (Jonathan)
• attempt AEAD-ChachaPoly (Aymeric)
• poly1305 spec equivalences
  • Vale <-> Hacl spec equivalence proof (Chris) https://github.com/project-everest/hacl-star/blob/sn_evercrypt_integration/providers/evercrypt/fst/EverCrypt.Poly1305.fst#L30
• more EverCrypt tests (Jonathan)
  • test vectors for Poly1305 (Jonathan)
  • test vectors for Curve25519 (Jonathan)
  • test vectors for ChachaPoly (Jonathan)
  • test vectors for Aes128Gcm (Jonathan)
  • can someone run the tests on a Goldmont machine to at least confirm that the SHA-EXT implementation works fine? update: they don't
• AES-GCM/Vale
  • finish proof (Bryan)
  • Low* (?) wrapper for non-block-multiple data (?)
  • interop wrapper (Aymeric)
• AEAD (Jonathan)
  • integrate AES-GCM from Chris with his spec (leaving off the HACL* spec for now)
  • an agile AEAD operational spec for the time being (we'll leave PRF-MAC higher-order specs to later)
  • fixup #ifdef compilation schemes (done in kremlin)
  • implement #ifdef-based code specialization
  • monotonic invariant for multiplexing underneath the expanded key
  • make encrypt / decrypt call into HACL*
  • make encrypt / decrypt call into Vale
  • rewire legacy EverCrypt.fst to call (unverified) into new AEAD ChachaPoly (possibly via a dirty assumed symbol in EverCrypt.Hacl)
  • kill code/old/chacha20, code/old/poly1305, code/old/api and remove C files from the build
  • remove _new suffix for Hacl_Chacha20Poly1305
  • change API to take a separate buffer for the tag (high priority)
• Curve25519 (Jonathan)
  • finish proof (Marina)
  • integrate the development as it currently stands (Jonathan)
  • kremlin c89/ifdef bug (Jonathan)
  • propagate has_abm /\ has_bmi2 throughout the HACL* development instead of assuming it (Aymeric)
  • multiplex, CPU detection, proper usage of ifdefs (Jonathan)
  • complete missing proofs in Hacl.Impl.Curve25519.Field64.Core.fst (Aymeric)
  • improve robustness of proofs: FInv seems to take a substantial amount of time; a regression in Hacl.Spec.Curve25519.Field51.Definition.fst (Marina) (moved to: general proof robustness improvement)
  • in generated inline assembly: add #ifndef FOOBAR_H #define FOOBAR_H etc. + #include <inttypes.h> (and remove Makefile hack) (Aymeric)
  • in generated inline assembly: remove const (and remove Makefile hack) (Aymeric)
  • in generated inline assembly: error: initialization of ‘uint64_t *’ {aka ‘long unsigned int *’} from ‘uint64_t’ {aka ‘long unsigned int’} makes pointer from integer without a cast (Aymeric)
  • in generated inline assembly: curve25519-inline.h:28:1: error: no return statement in function returning non-void (Aymeric)
  • fix symbol collisions (Jonathan)
  • tests for curve25519 (direct HACL*) (Jonathan)
• two assume leftover in EverCrypt.Hash https://github.com/project-everest/hacl-star/blob/sn_evercrypt_integration/providers/evercrypt/fst/EverCrypt.Hash.fst#L139 (Tahina)
• two assume leftover in X64.BufferViewStore https://github.com/project-everest/hacl-star/blob/sn_evercrypt_integration/vale/code/arch/x64/X64.BufferViewStore.fst#L48
• Improve the stack model (Aymeric)
• cleanup READMEs and landing pages (Jonathan)
  • terminology ("provider")
  • up-to-date lists of algorithms
  • fixup install instructions + docker container
• https://project-everest.github.io/ to be updated to mention EverCrypt (Bryan)
• merge sn_evercrypt_integration (Jonathan)
  • fix src/windows/evercrypt/makefile.vs (again! can we auto-generate it?)
  • #ifdef GNUC in inline asm
  • open_out_binary to avoid host endlines in inline asm (and regular asm too?) (now FStar_IO is a victim of OCaml's built-in line-ending conversion FStarLang/FStar#1683)
• Assume left in X64.AESGCM.vaf (Bryan)
• Stabilize proof in thirdPartyPorts/X64.AESGCM.vaf, and remove assume false (Bryan)
• performance regression in Curve (Karthik)
• Merkle Tree proofs
  • serialization (Aseem)
• add @type: true fsdoc annotations for the generated C code to have types (Jonathan)
• fix windows assembly error (Jonathan)

For alpha2:

See #176

[s-zanella]

I removed all remaining assumptions from lib in the _dev branch and fixed a few regressions.
Lib.IntVector.fst is still broken but it seems to be in a better state in _dev_combinators.

I believe the 3 assumes in Hacl.Test.SHA3.fst are harmless. The test vectors are written as immutable buffers but the SHA3 API takes mutable buffers, so the harness allocates a fresh buffer and copies over the contents of the immutable buffer before calling into SHA3. The test harness can be rewritten to avoid the assume, but this is low priority.

Besides completing the implementation of Lib.IntTypes using FStar.ConstantTime.Integers in the santiago_inttypes branch I can help integrating SHA3 into EverCrypt and verifying the map_blocks combinators for Chacha20.

[msprotz]

That would be wonderful. Can I let you be the libraries wizard and handle:

• the "merge" of their version in _dev into either fstar-master or protz_integration2, and
• hooking them up to LowStar.Endianness once we land it?

Thanks!

[s-zanella]

Will do.

[msprotz]

Closing in favor of #176