A memory and data model for miTLS

[nikswamy]

We have in several related branches a prototype implementation of the miTLS memory model https://github.com/mitls/mitls-papers/wiki/The-Memory-Model-of-miTLS (private link)

To merge this into the no_hsl branch of miTLS the following work items need to be completed

F* branch: nik_dynamic_regions to be merged to master

• [ ] Runtime support for dynamic regions in kremlin extraction (@protz )
• [x] We're starting with just a no-op runtime support for the dynamic region operations, mapping them to the existing malloc support. @aseemr
• [x] KreMLin support for const buffers (@protz)
• [x] Extending the HyperStack memory model to support the interface of dynamic regions (@aseemr )
• [x] An implementation of the witnessed_functorial lemma in LowStar.Monotonic.Buffer (@aseemr )
• [x] An implementation of a Buffer.sub variant that does not require a concrete length field, i.e., something like what's below. (thanks ! @R1kM )

assume
val sub (c:buffer 'a) (i:uint_32) (len:Ghost.erased uint_32)
  : Stack (buffer 'a)
    (requires fun h ->
      live h c /\
      U32.v i + U32.v (Ghost.reveal len) <= length c)
    (ensures fun h0 c' h1 ->
      h0 == h1 /\
      c' `sub_buffer i (Ghost.reveal len)` c)

EverParse changes

• [x] Accessors and jumpers should not take a concrete slice length. Instead they should take at most a pointer and a ghost length, as follows @tahina-pro

let accessor (p1:parser k1 t1) (p2:parser k2 t2) (g:gaccessor p1 p2 l) =
    pos:u32 -> b:buffer u8 -> len:erased u32 -> 
    Stack u32
    (requires fun h -> 
        valid (as_slice b len) p1 pos h /\ ... )
    ...

• [x] Accessors for tag of a tagged union @tahina-pro
• [x] Accessor for the discriminator of the if/then/else type @tahina-pro
• [x] Move mitls-fstar/src/tls/LowParse.Repr to lowparse @nikswamy @tahina-pro
• [ ] Support for list reprs, with combinators on it like fold, etc. @nikswamy
• [ ] QuackyDucky changes to auto-generate reprs for all types in the rfc (@ad-l @tahina-pro ?) For each type t, it should produce two type abbreviations:

let ptr = R.repr_ptr_p t t_parser
let pos (b:R.const_slice) = R.repr_pos_p t b t_parser

And for each field it should produce, either a FieldAccessor or a FieldReader

e.g.,

/// Reader for the protocol version
noextract
unfold
let version_reader =
  R.FieldReader
    CH.accessor_clientHello_version
    Parsers.ProtocolVersion.protocolVersion_reader

/// Accessor for the extensions
noextract
unfold
let extensions_field =
  R.FieldAccessor CH.accessor_clientHello_extensions
                  Parsers.ClientHelloExtensions.clientHelloExtensions_jumper
                  Parsers.ClientHelloExtensions.clientHelloExtensions_parser32

As we figure out how to do lists, we will require more things to be emitted by QD

miTLS changes

• [x] ParseFlights, Receive, Transcript use the new reprs @nikswamy
• [ ] Provide access to the ith element of a list whose element sizes are constant @nikswamy
• [ ] A selected example from Nego uses reprs @nikswamy
  • Negotiation.accept_ServerExtension
  • Negotiation.accept_ServerExtensions
• [x] A stateful API for transcript and conditional erasure of transcript values

We should maintain the functionality of no_hsl, as defined by CI

[ad-l]

Sounds like a good plan, I'm happy to take care of the QD changes as soon as LowParse.Repr.fst is moved to LowParse

[aseemr]

The support for the witnessed buffer lemma and dynamic regions is in F* master. Remaining tasks there:

• Weaken the preconditions of existing ralloc and ralloc_mm functions to work on heap regions

• Add no-op extraction for dynamic regions that defaults to malloc etc.

Hope to finish them soon.