Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Next wave of integration from Vale & HACL*/dev #145

msprotz opened this Issue Feb 20, 2019 · 3 comments


None yet
2 participants
Copy link

msprotz commented Feb 20, 2019

always close the page then reopen it before editing this issue


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 (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
    • 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
  • 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 (Tahina)
  • two assume leftover in X64.BufferViewStore
  • Improve the stack model (Aymeric)
  • cleanup READMEs and landing pages (Jonathan)
    • terminology ("provider")
    • up-to-date lists of algorithms
    • fixup install instructions + docker container
  • 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 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:

  • AES-CTR (Bryan)
    • exposing Low* interfaces + spec in specs/
    • EverCrypt idiomatic API with state and framing (Jonathan)
    • tests (?)
  • 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")
  • 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 (Jonathan)
    • functional correctness
  • 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)
    • FStarLang/kremlin#9 -- otherwise evercrypt-external-header is unusable (Jonathan)
    • unified order of arguments across evercrypt (Jonathan)
    • abstract interface on top of EverCrypt.Hash.Incremental to make sure this doesn't defeat the CAbstractStruct of EverCrypt.Hash (Jonathan)
    • find a way to check through CI that the internal struct type is not made visible in the generated .h!
  • 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, after rewiring Lib.ByteSequence to FStar.Endianness)
    • 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?)
  • rewire HACL* libraries to use LowStar.Endianness (Santiago)
    • 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
  • 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" (
    • 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
  • 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
  • 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
  • complete the implementation of Lib.IntTypes using FStar.ConstantTime.Integers (Santiago)
  • 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 (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
  • propagate preconditions on X64.avx2 everything in HACL*, starting from Lib.IntVector and up through its callers
  • 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
  • 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)

For later.

  • specifications using cryptographic constructions
    • higher-order specs for CTR, 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 msprotz changed the title Integrating SHA3 and Poly1305 Next wave of integration from Vale & HACL*/dev Feb 21, 2019


This comment has been minimized.

Copy link

s-zanella commented Feb 26, 2019

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.


This comment has been minimized.

Copy link
Member Author

msprotz commented Feb 26, 2019

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?



This comment has been minimized.

Copy link

s-zanella commented Feb 27, 2019

Will do.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.