Roadmap for a unified QUIC/TLS Multistream atop EverCrypt AEAD

[s-zanella]

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 encryption, integrating QUICstream
• Support for TLS 1.3 and TLS 1.2 AEAD ciphersuites
• Support for rekeying
• Built on packaged functionalities for AEAD, IV and PNE
• Minimal changes wrt current epoch-based TLS record layer
• Compatible with low-level TLS API for QUIC: for now a hack returning raw keys
• Ideal functionality built on top of EverCrypt specification (verified relying on functional correctness of EverCrypt AEAD)
• Compatible with a future SecureAPI security proof, notably in terms of memory management

Tasks:

• [x] Switch Mem, Idx, Pkg, and Pkg.Tree to the same modern LowStar.Buffer memory model used in EverCrypt. @ad-l and @s-zanella
• [x] Port existing KDF package an rekeying test to new memory model @ad-l or @s-zanella
• [ ] AEAD.Pkg package atop EverCrypt.AEAD.fsti in hacl-star@fstar-master. As a first step we want an AEAD.fsti module that does the buffer<->bytes conversion for keys and wraps over EverCrypt.AEAD.fsti (we'll need to add a specification for create in Spec.AEAD). AEAD.Pkg packages AEAD.fsti, extracts and passes unit tests when linked against libevercrypt. @s-zanella
• [x] PNE (QUIC packet number encryption) package with unit tests passing when linked against libevercrypt @ad-l
• [ ] Port IV package to new memory model @s-zanella
• [ ] StreamAE wrapper (combinator, not a package) for TLS streams built from AEAD and IV packages @s-zanella
• [ ] QUICStream wrapper built from AEAD, IV, and PNE packages @ad-l
• [ ] TransportSecret module creating streams from either StreamAE or QUICStream. Some other module will dispatch these streams to Multistream
• [ ] Multistream API that provides encrypt/decrypt for application and create_stream for receiving new streams created from TransportSecret. The Multistream internal state will possibly have type Seq index & Seq (Map position bytes) @fournet
• [ ] Restore protocol-level tests using the new TransportSecret module with old Handshake module

Tasks in hacl-star we depend on:

• Fix defects in Spec.AEAD
• [x] Maximum input length is too short: see https://github.com/project-everest/hacl-star/blob/fstar-master/specs/Spec.AEAD.fsti#L62. Done, but still limited by using uint32_t for lengths . Thanks @R1kM!
• [x] Input ciphertext length of decrypt is shorter than maximum output of encrypt. See https://github.com/project-everest/hacl-star/blob/fstar-master/specs/Spec.AEAD.fsti#L117 - the max size of cipher should be max_length a + tag_length a, not max_length a.
• [x] Misses key expansion. Although EverCrypt.AEAD.fsti doesn't use expand explicitly, it is part of the abstract invariant in the implementation: https://github.com/project-everest/hacl-star/blob/ca3e12f21d1879f192f19105dcc43ffe2f6e350b/providers/evercrypt/fst/EverCrypt.AEAD.fst#L61
• [x] Spec.AEAD is missing a correctness lemma decrypt k n aad (encrypt k n aad p) == Some p Added, but admitted until we prove correctness of individual algorithms.
• [ ] Portable AES-GCM (or at least AES-GCM for Arm)
• [ ] Prove Hacl* specifications are compatible with Spec.AEAD. The implementation of AES-GCM in _dev is proved memory safe only. I see this other comment that may be relevant: https://github.com/project-everest/hacl-star/blob/fstar-master/providers/evercrypt/fst/EverCrypt.AEAD.fst#L54

Issues to remember:

• Crypto reindexing messes with memory footprints (we'll ignore this to begin with).
• Lowering of packages. They still use bytes for keys; we'll need to turn them into buffers and reconcile this with the ideal implementation. (we'll do bytes<->buffer conversions for now).

[ad-l]

Starting on Mem now, locking that module

[msprotz]

We chatted about key expansion this morning. It's on the radar of @parno. I don't know if @karthikbhargavan's C implementation of AES-GCM also features key expansion.

Can you elaborate on 3. -- what does "connect to HACL*" mean?

[parno]

@protz Do you mean IVs of non-standard length? I recall talking about that. I don't remember discussing key expansion.

[msprotz]

Ah sorry, I got confused between the two. My bad. Then I don't know why Spec.AEAD misses key expansion. I see it there: https://github.com/project-everest/hacl-star/blob/fstar-master/specs/Spec.AEAD.fsti#L114

[parno]

Regarding maximum input length, for AES-GCM, I believe @R1kM has a branch where he's working on increasing that to the NIST spec's limit. I'm not sure how far along he is.

[R1kM]

Regarding maximum input length, I had started around a week ago, but I was preempted and it still needs some more work. I'll look at it in the next few days. Thanks for the reminder!

[s-zanella]

@protz: Re defects in Spec.AEAD: these were mainly raised by @fournet, so I don't know if my interpretation is accurate.

1. Maximum input length is too short: We all agree this refers to https://github.com/project-everest/hacl-star/blob/fstar-master/specs/Spec.AEAD.fsti#L62.
2. Output length is too large: I don't know what this means.
3. Connect to Hacl: I think this means proving that a portable Hacl implementation of AES-GCM satisfies Spec.AEAD. The experimental implementation I see in _dev is proved memory safe only. I see this other comment that may be relevant: https://github.com/project-everest/hacl-star/blob/fstar-master/providers/evercrypt/fst/EverCrypt.AEAD.fst#L54
4. Misses key expansion: I was under the impression that this was implemented and as Jonathan pointed out it indeed is. Maybe Cédric meant something else.

[ad-l]

2. refers to https://github.com/project-everest/hacl-star/blob/fstar-master/specs/Spec.AEAD.fsti#L117 - the max size of cipher should be max_length a + tag_length a, i.e. pow2 20 - 1.
3. Spec.AEAD has expand, but it is not used in EverCrypt.AEAD (for create).
4. Spec.AEAD is missing a correctness lemma, i.e.

   val lemma_encrypt_decrypt: #a:supported_alg -> k:kva -> n:iv a -> aad:ad a -> p:plain a ->
   Lemma (decrypt k n aad (encrypt k n aad p) == Some p)

[ad-l]

Tasks for upgrading the memory model:

• [x] Mem
• [x] DefineTable (new, combines the end of Mem and the assumed lemmas in Pkg)
• [ ] FStar.Monotonic.DependenMap
• [x] Idx
• [x] Pkg
• [x] Pkg.Tree
• [x] KDF
• [ ] KDF.Rekey

[s-zanella]

@ad-l

2. refers to https://github.com/project-everest/hacl-star/blob/fstar-master/specs/Spec.AEAD.fsti#L117 - the max size of cipher should be max_length a + tag_length a, i.e. pow2 20 - 1.

I don't see how this relates to

2. Output length is too large

I think this is another flaw, but also a case of 1. Maximum input length is too short.

3. Spec.AEAD has expand, but it is not used in EverCrypt.AEAD (for create).

Although EverCrypt.AEAD.fsti doesn't use expand explicitly, it is part of the abstract invariant in the implementation: https://github.com/project-everest/hacl-star/blob/ca3e12f21d1879f192f19105dcc43ffe2f6e350b/providers/evercrypt/fst/EverCrypt.AEAD.fst#L61 I'm still not sure what this point means.

I guess you meant 4 instead of 3

4. Spec.AEAD is missing a correctness lemma, i.e.

   
   val lemma_encrypt_decrypt: #a:supported_alg -> k:kva -> n:iv a -> aad:ad a -> p:plain a ->
   Lemma (decrypt k n aad (encrypt k n aad p) == Some p)```

And this is yet another defect to add to the list.

[R1kM]

@ad-l , I pushed a change to fstar-master that doesn't restrict the length of the input or output for the Vale AES-GCM, which should address points 1 and 2. Let me know if you have any other issue with this.

[ad-l]

@s-zanella in 8d0b4076260f502160999d72a29a4a11845cf6c4 Pkg, DefineTable and Mem are now fully verified. Can you take care of Idx? I'm moving to KDF now

[ad-l]

@s-zanella Some problems I identified when looking at Idx this morning:

• The honesty invariant is not useful in the case where an honest handshake secret is derived from a corrupt salt0 (i.e. the honest_idh case). I expect we may have to change the definition of DH honesty and index DH secrets by a counter (following the paper model)
• There are difficult restrictions when reasoning about witnessed properties and some lemmas are only provable in ST but not in Ghost (e.g. lemma_honest_corrupt). Another example is the application of the honesty table invariant in KDF:

  let lemma_honest_parent (i:regid) (lbl:label) (ctx:context)
  : Lemma (requires wellformed_derive i lbl ctx /\ registered (derive i lbl ctx) /\ ~(honest_idh ctx))
  (ensures honest (derive i lbl ctx) ==> honest i)

  I'm wondering what would be one axiom that could help us prove these lemmas without introducing inconsistency. The natural idea is:

  assume val give_witness: p:mem_predicate -> Ghost mem
  (requires witnessed p) (ensures fun h -> p h)

  but I recall Asseem telling me this is not sound. In any case it is not enough, for instance trying to prove the lemma_honest_parent I got stuck at:

  if model then
  let log : Idx.i_honesty_table = Idx.honesty_table in
  let h = give_witness (MDM.defined log (derive i lbl ctx)) in
  let t = MDM.repr (HS.sel h log) in
  assert((~(honest_idh ctx) /\ DM.sel t (derive i lbl ctx) <> Some false) ==> (DM.sel t i <> Some false));
  assert(MDM.contains log (derive i lbl ctx) true h ==> MDM.contains log i true h);
  admit()
  else ()

[s-zanella]

@ad-l I'm afraid that if we define honesty in terms of witnessed many lemmas will only be provable in ST because of the need to bring up the witness to testify. That said, some logical manipulations on witnesses are possible, so some lemmas will be provable without lifting to the ST effect.

lemma_honest_parent is provable in ST without any axioms:

val lemma_honest_parent (i:regid) (lbl:label) (ctx:context)
  : ST unit (requires fun h0 ->
            wellformed_derive i lbl ctx /\ 
            registered (derive i lbl ctx) /\ 
            ~(honest_idh ctx) /\ 
            honest (derive i lbl ctx))
          (ensures fun h0 _ h1 -> h0 == h1 /\ honest i)
let lemma_honest_parent i lbl ctx =
  if model then
    let log : i_honesty_table = honesty_table in
    testify (MDM.contains log (derive i lbl ctx) true);
    let x = MDM.lookup log i in
    ()
  else ()

[s-zanella]

@ad-l It's also provable as a Lemma ~assuming this very reasonable axiom (it might be actually derivable from what's in FStar.HyperStack already):~ Edit: of course it is

val lemma_witnessed_true (p:mem_predicate) :
  Lemma (requires (forall h. p h)) (ensures witnessed p)
let lemma_witnessed_true p =
  lemma_witnessed_constant True;
  weaken_witness (fun _ -> True) p

val lemma_honest_parent (i:regid) (lbl:label) (ctx:context)
  : Lemma (requires
            wellformed_derive i lbl ctx /\ 
            registered (derive i lbl ctx) /\ 
            ~(honest_idh ctx) /\ 
            honest (derive i lbl ctx))
          (ensures honest i)
let lemma_honest_parent i lbl ctx =
  if model then
    let log : i_honesty_table = honesty_table in
    lemma_witnessed_true (fun h -> MDM.contains log (derive i lbl ctx) true h ==> MDM.contains log i true h);
    lemma_witnessed_impl (MDM.contains log (derive i lbl ctx) true) (MDM.contains log i true)
  else ()

[s-zanella]

Idx.fst fully verifies (see https://github.com/project-everest/mitls-fstar/commit/a3259976e981d4c57bf4ce89f68848d4464e5f06 and https://github.com/project-everest/mitls-fstar/commit/07ab3e8ccabfdbb3829706db50dce1846ce43f4b#diff-a051a34719121d8ff29570c947d090f1). We managed to replace all required stateful lemmas with pure versions and so there are no axioms left.

We still rely on compatibility lemmas to bridge between old style (FStar.HyperStack) and new style (LowStar.Monotonic.Buffer) modifies clauses because FStar.Monotonic.DependentMap hasn't been ported yet. I added this as a new item to the list of modules to upgrade.

[ad-l]

I propagated the Idx changes. As discussed, I'm preparing to merge to dev just to ensure the other ideal functionalities like CRF use the latest memory model and libraries. I'm working on restoring extraction on adl_memory_model now