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