Upgrading configurations

[nikswamy]

The end of TLSConstants defines a type called config. It contains both

• ordinary configuration data
• and application callbacks, e.g., ticket_callback, nego_callback,
  etc.

This is passed to create a connection and used primarily in
Negotiation and Handshake

There are several problems:

1. This is a high-level datatype with fields like named_groups that
   are lists, incurring memory overhead, GC, etc.

2. It's also not the type used from the C api. Instead we currently
   have many functions to read and write many fields of the
   configuration before getting started. For example, see FFI.fst
   FFI.updatecfg FFI.ffiSetCipherSuites

3. The same type is used by clients and servers, although some values
   are only used on the client and others only on the server. An
   additional wringle is that in order to configure a client, the
   application needs to construct both a config object as well as a
   Negotiation.resumeInfo.

4. Server configuration is getting more dynamic: the configuration is
   passed later, via a callback.

5. Various datastructures and refinements are not aligned to QD types,
   e.g., we pass a pair of min_version and max_version, which then
   must be turned into a list of supported versions in QD. We would
   like to match wireformats for these fields.

New design

We distinguish two forms of configurations.

• Outer configurations: untrusted configurations passed by the application.

• Inner configurations: Value-like configurations used within the TLS implementation, e.g., in Nego.

Outer configurations need to be validated and then stashed, yielding inner configuration.
The outer configuration contains:

• the list of cipher suites, just a vlbytes, but it needs to be validated and stashed, before negotiation. (using EverParse, reprs etc.)

• encrypted key materials (aka "seals"), that need to be decrypted and parsed before negotiation.

  • See TLS.Store for details about seals. Briefly, for resumption, the client application passes a list of encrypted bytes (aka seals) whose decryption yields agility parameters, resumption master secret and tickets.

Work in progress towards this design

See experiments/TLS.Config.fst.

It is meant to be a complete translation of TLSConstants.config

It factors the type into shared parts (between client and server) and role-specific parts

For the shared parts, it has

• a spec-level (inner) configuration, that is a pure value.

• a low-level (outer) configuration, with a relation between the two

  e.g., shared is a spec-level inner configuration
  shared_low is its low-level outer counterpart

  There is some duplication between these for fields that are need
  not be validated in the outer config. We could refactor to share
  these between the outer and inner types.

  We also need a low-level inner configuration (i.e., the repr counterpart of the outer config)

  We need a function to convert from outer to inner low-level configs

  One downside is that we configure the server per connnection, which will involve copying and stashing values for each connection. But we will not address this for now.

We need something similar for the role-specific parts

Because it is part of the public API, the extraction of the outer configuration has to be beautiful. May have to tweak by hand ...

We need to provide default configurations: this helps for testing etc. It is currently in TLSInfo, but it should move here. We need to construct low-level outer configurations (i.e., byte buffer representations of cipher suites etc.).

• We could statically generate constants and validate them to build
  inner configs.

• More high tech: We have experiments that allow us to normalize
  using serialize32 high-level values during typechecking to
  low-level constants. TODO: find the experiment with Tahina

Uncertainties:

• Callbacks:

  • contain an application context (as opaque pointers) that
    is passed in the config. This could be cleaned up.

  • their types will evolve as needed by Nego etc.

• Replace config from TLSConstants by promoting TLS.Config.fst

• Expect to iterate on the details of config as Nego is finished