Syntax for protocol sessions

[senier]

Design a syntax for the sessions model created in #47. Sessions should be a first-class citizen of RecordFlux specifications. External entities like channels and functions could be declared in a generic block (to be discussed). We also need a place to declare variables and renames (a declare block inside the session type, maybe sessions should not be a type but some separate entity like Ada tasks with an own specification section?).

generic
   Record_Data_Channel : Channel with => Readable, Writable;
   with function Decrypt(...);
session My_Session is
   OID_Filters_Received : Boolean := False;
begin
   ...
end session;

---

• Design syntax
• Add parser
• Allow creating text representation from model

[treiher]

I also think that sessions should a first-class citizen. That is why I would propose a flat structure:

with GreenTLS;
with TLS_Alert;

package TLS_Handshake is

   type Supported_Version is
      message
         Version : Protocol_Version;
      end message;

   for CH_Extension use (Data => Supported_Versions)
      if Tag = EXTENSION_SUPPORTED_VERSIONS;

   Record_Data_Channel : Channel with Readable, Writable;
   Record_Control_Channel : Channel with Writable;
   Configuration_Channel : Channel with Readable;

   type Hash_Context is private;

   Application_Layer_Protocol_Negotiation_Received : Boolean := False;
   Binders : TLS_Handshake.PSK_Binder_Entries;

   Certificate_Message : TLS_Handshake.Certificate renames CCR_Handshake_Message.Payload;
   Server_Hello_Message : TLS_Handshake.Server_Hello renames Server_Hello_Handshake_Message.Payload;

   function Calculate_Binders_Length (PSKs : GreenTLS.PSKs) return RFLX.Types.Bit_Length;

   state Create_Client_Hello_Extensions is
      Supported_Version : TLS_Handshake.Supported_Version;
      Supported_Versions_Extension : TLS_Handshake.CH_Extension;
   begin
      Supported_Version := TLS_Handshake.Supported_Version'(Version => TLS_Handshake.TLS_1_3);
      Supported_Versions_Extension := TLS_Handshake.CH_Extension'(Tag => TLS_Handshake.EXTENSION_SUPPORTED_VERSIONS, Data_Length => Supported_Version'Length, Data => Supported_Version);
      Extensions_List'Append (Supported_Versions_Extension);
      Extensions_List'Extend (Create_Client_Hello_Extensions (Configuration));
   end Create_Client_Hello_Extensions
      then ERROR_INTERNAL_ERROR
         if Extensions_List'Valid = False
         with Desc => "rfc8446.txt+1234:56-1235:46",
      then START_POST_HANDSHAKE_AUTH_EXTENSION
         if Configuration.Post_Handshake_Auth_Enabled = True,
      then START_DHE
         if TLS_Handshake.PSK_DHE_KE in Configuration.PSK_Key_Exchange_Modes,
      then START_PSK
         if TLS_Handshake.PSK_KE in Configuration.PSK_Key_Exchange_Modes,
      then ERROR_INTERNAL_ERROR;

   state Final with Final is null state;

end TLS_Handshake;

[senier]

Thinking about it a bit more, I'm still uneasy with not having a session type. Here are my thoughts:

• Pro:
  • Fewer syntactic constructs
  • Saves space
• Con:
  • States can be sprinkled across the package and mixed with types making the session hard to understand
  • It's not intuitive that the function declaration is actually a generic parameter to the session (coming from Ada, I'd expected an implementation to follow somewhere further down the spec)
  • So far, packages were just containers of types. When creating the 1:1 relation with sessions, they gain a semantics which I'm not sure is preferable
  • You cannot have multiple sessions in one package. While I don't have a specific use case, I think it's unnecessary limitation.
  • Sessions don't have a dedicated name. Of cause we can take the package name, but again I think this is an unnecessary mixing of orthogonal concepts.
  • Instantiating generic sessions (for shared sub-automata) may become more messy than necessary.
  • We once had the idea to associate an automaton with an array of messages to define valid sequences. This could be a situation where you want to define multiple sessions together with messages in the same package

[treiher]

As basis for discussion a variant with session block:

with GreenTLS;
with TLS_Alert;

package TLS_Handshake is

   type Supported_Version is
      message
         Version : Protocol_Version;
      end message;

   for CH_Extension use (Data => Supported_Versions)
      if Tag = EXTENSION_SUPPORTED_VERSIONS;

   generic
      Record_Data_Channel : Channel with Readable, Writable;
      Record_Control_Channel : Channel with Writable;
      Configuration_Channel : Channel with Readable;
      type Hash_Context is private;
      with function Calculate_Binders_Length (PSKs : GreenTLS.PSKs) return RFLX.Types.Bit_Length;
   session Session is
      Application_Layer_Protocol_Negotiation_Received : Boolean := False;
      Binders : TLS_Handshake.PSK_Binder_Entries;

      Certificate_Message : TLS_Handshake.Certificate renames CCR_Handshake_Message.Payload;
      Server_Hello_Message : TLS_Handshake.Server_Hello renames Server_Hello_Handshake_Message.Payload;
   begin
      state Create_Client_Hello_Extensions is
         Supported_Version : TLS_Handshake.Supported_Version;
         Supported_Versions_Extension : TLS_Handshake.CH_Extension;
      begin
         Supported_Version := TLS_Handshake.Supported_Version'(Version => TLS_Handshake.TLS_1_3);
         Supported_Versions_Extension := TLS_Handshake.CH_Extension'(Tag => TLS_Handshake.EXTENSION_SUPPORTED_VERSIONS, Data_Length => Supported_Version'Length, Data => Supported_Version);
         Extensions_List'Append (Supported_Versions_Extension);
         Extensions_List'Extend (Create_Client_Hello_Extensions (Configuration));
      transition
         then ERROR_INTERNAL_ERROR
            if Extensions_List'Valid = False
            with Desc => "rfc8446.txt+1234:56-1235:46"
         then START_POST_HANDSHAKE_AUTH_EXTENSION
            if Configuration.Post_Handshake_Auth_Enabled = True
         then START_DHE
            if TLS_Handshake.PSK_DHE_KE in Configuration.PSK_Key_Exchange_Modes
         then START_PSK
            if TLS_Handshake.PSK_KE in Configuration.PSK_Key_Exchange_Modes
         then ERROR_INTERNAL_ERROR
      end Create_Client_Hello_Extensions;

      state Final with Final is null state;
   end Session;

end TLS_Handshake;

[treiher]

I think we should move the Intial and Final aspect from the state declaration to the session declaration. This would prevent the duplicate annotation of states. Here is an example:

generic                                                                                                   
session Session with                                                                                      
   Initial => A,                                                                                          
   Final => C                                                                                             
is                                                                                                        
begin                                                                                                     
   state A is                                                                                             
   begin                                                                                                  
   transition                                                                                             
      then B                                                                                              
   end A;                                                                                                 
                                                                                                          
   state B is                                                                                             
   begin                                                                                                  
   transition                                                                                             
      then C                                                                                              
   end B;                                                                                                 
                                                                                                          
   state C is null state;                                                                                 
end Session;

[senier]

I think we should move the Intial and Final aspect from the state declaration to the session declaration. This would prevent the duplicate annotation of states. Here is an example:

I agree - this is better.