Handling of message refinements in sessions

[treiher]

Context and Problem Statement

Renaming declarations are intended to provide a simple and efficient access to inner messages. The idea is to create an alias for an inner message. (The relation between the message and the inner message must be defined by a refinement.)

Client_Hello_Message : TLS_Handshake::Client_Hello renames Client_Hello_Handshake_Message.Payload;

In the given example, Client_Hello_Handshake_Message is a variable of type TLS_Handshake::Handshake. The renaming declaration defines an alias Client_Hello_Message to the Payload field of Client_Hello_Handshake_Message that is interpreted as TLS_Handshake::Client_Hello message. Thus, when Client_Hello_Message is accessed, actually a part of Client_Hello_Handshake_Message is accessed. Client_Hello_Handshake_Message can still be used after the renaming declaration.

I think this construct could lead to confusions in complex specifications. The implementation of the code generation will also be difficult, even if only allowing read only access to the inner message. In the most obvious implementation, for each access to the inner message, the parser context would need to be switched to the inner message before the access and switched back after the access, to still allow the use of the outer message. This approach will be inefficient, as the parser state of the inner message will most probably be lost after switching back. The functionality for switching back is not implemented yet (#72).

The only currently supported option for handling message refinements are the use of conversions in assignments:

Client_Hello_Message := TLS_Handshake::Client_Hello (Client_Hello_Handshake_Message.Payload);

The drawback of this approach is the creation of a copy: Client_Hello_Message is a copy of Client_Hello_Handshake_Message.Payload interpreted as TLS_Handshake::Client_Hello.

Considered Options

O1 Keep renaming declarations

− Possibly confusing behavior
− Inefficient (at least with most obvious implementation)

O2 Just use conversions and remove renaming declarations

+ Clear behavior
− Inefficient (at least with current implementation)

O3 Add language construct for switching between inner and outer message explicitly

• O3.1 One statement for context switching
• O3.2 Two separate statements for context switching: one for switching to inner message and one for switching back
• O3.3 Scoped block: Switching to inner message when entering block, switching back when leaving block:
• O3.4 Generic declare block + refinement declaration: Switching to inner message when entering declare lock, switching back when leaving declare block:

declare
   Client_Hello_Message : TLS_Handshake::Client_Hello refines Client_Hello_Handshake_Message.Payload;
begin
   --  Inner message Client_Hello_Message can be accessed
   --  Access to outer message Client_Hello_Handshake_Message is disallowed
end;

+ Clear behavior
+ Efficient (no copy and no unnecessary context switches)
+ O3.4: Similar to SPARK's borrowing semantics

Decision Outcome

O3.4

[sttaft]

When you talk about the parser context, I am unsure whether this is the (compile time) parser for the RecordFlux source language, or the run-time parser for messages. An example would be helpful!

[treiher]

For the sake of completeness, the example described above assumes the following refinement in the RecordFlux specification:

package TLS_Handshake is

   [...]

   type Handshake is
      message
         Tag : Handshake_Type;
         Length : Length;
         Payload : Opaque
            with Size => Length * 8;
      end message;

   type Client_Hello is
      message
         [...]
      end message;

   for Handshake use (Payload => Client_Hello)
      if Tag = HT_CLIENT_HELLO;

   [...]

The term "parser context" refers to the generated SPARK code. A record type named Context is used to store the buffer (containing the to be parsed message) and the current state of the parser (e.g., location, validity and parsed values of fields). Here is an example how the parser contexts are used for the given refinement:

Handshake_Context    : TLS_Handshake.Handshake.Context;     --  corresponds to Client_Hello_Handshake_Message
Client_Hello_Context : TLS_Handshake.Client_Hello.Context;  --  corresponds to Client_Hello_Message

TLS_Handshake.Handshake.Verify_Message (Handshake_Context);
if TLS_Handshake.Handshake.Structural_Valid_Message (Handshake_Context) then
   if TLS_Handshake.Contains.TLS_Handshake_Client_Hello_In_TLS_Handshake_Handshake_Payload (Handshake_Context) then
      --  Condition of type refinement is fulfilled (i.e. Tag = HT_CLIENT_HELLO)
      TLS_Handshake.Contains.Switch_To_Payload (Handshake_Context, Client_Hello_Context);
      --  Client_Hello_Context is initialized, buffer was moved from Handshake_Context into Client_Hello_Context
      --  Client_Hello_Context can now be used to parse/access content of Client_Hello_Message
      --  Handshake_Context cannot be used now, as buffer was moved
      TLS_Handshake.Contains.Update_Payload (Handshake_Context, Client_Hello_Context);
      --  Buffer was moved back from Client_Hello_Context into Handshake_Context
      --  Handshake_Context can be used again
      --  Client_Hello_Context cannot be used anymore, as buffer was moved
   end if;  
end if;  

[sttaft]

This feels like a problem that might best be addressed by a stack discipline, similar to a pushdown finite state automaton.