Message format defined by prior negotiation

[treiher]

Context and Problem Statement

There are multiple existing communication protocols where the message format is defined by prior negotiation. The field length (Componolit/systematization-binary-schemas#28) as well as the field type (Componolit/systematization-binary-schemas#53) can be affected.

Considered Options

O1 Generic message type with types as formal parameters (#133)

+ Also usable for different purposes (cf. #133)
− Not directly applicable for variable-length opaque field in DTLS 1.3, NTP, QUIC
− Probably only instances of generic type could be verified

O2 Variant message type with scalars as discriminants

The discriminant could be used in conditions (SPDM, TLS 1.3) and in length aspects (DTLS 1.3, NTP, QUIC).

+ Applicable in all known instances
+ Extension of message verification is simple: references to discriminants can be handled similar as references to fields

Decision Outcome

O2 is the only viable option.

Tasks

• Decide naming: variant messages, discriminated messages or parameterized messages.
  • Decision: Parameterized Messages
• How could a condition on the discriminants/parameters be defined (restricting allowed parameter values or parameter combinations before evaluation of first message field)?
  • Options:
    • Condition on link to first field (conflicts with Condition from Initial to first field #425)
  • Decision: Use existing functionality for now
• Decide: Allow the definition of the first field by a parameter value?
  • Not yet, maybe in the future (Allow definition of first message field by parameter value #764)
• Extend specification parser
• Extend message model
• Extend code generator for messages
• Extend session model
• Extend code generator for sessions
• Support use of parameterized messages as field types
• Amend documentation

The support for parameterized messages in PyRFLX will be added in a subsequent issue (#743).

[treiher]

package Test is

   type Length is range 1 .. 2**14 - 1 with Size => 16;

   type Message (Length : Length; Extended : Boolean) is··
      message
         Data : Opaque
            with Size => Length * 8
            then Extension
                if Extended = True
            then null
                if Extended = False;
         Extension : Opaque
            with Size => Length * 8;
      end message;

   generic
      C : Channel with Readable, Writable;
   session Session with
      Initial => Receive,
      Final => Terminated
   is
      M_R : Message;
   begin
      state Receive
      is
      begin
         M_R'Reset (Length => 2, Extended => False);
         C'Read (M_R);
      transition
         then Reply
            if M_R'Valid
         then Terminated
      end Receive;

      state Reply
      is
      begin
         C'Write (Message'(Length => M_R.Length, Extended => True, Data => M_R.Data, Extension => [3, 4]));
      transition
         then Terminated
      exception
         then Error
      end Reply;

      state Error
      is
      begin
         transition
            then Terminated
      end Error;

      state Terminated is null state;
   end Session;

end Test;