Ensuring object properties in protocol session states

[treiher]

Context and Problem Statement

In many cases, certain properties of an object must be fulfilled before the object can be used for specific actions.

Examples

E1

         Network_Channel'Write
            (TLS_Record::TLS_Record'(Tag => TLS_Record::Alert,
                                     Legacy_Record_Version => TLS_Record::TLS_1_2,
                                     Length => Alert_Message'Size / 8,
                                     Fragment => Alert_Message'Opaque));

Ensure: Alert_Message'Size / 8 <= 16384

E2

            GreenTLS_Alert_Message := GreenTLS::Alert_Message (Handshake_Control_Message.Data);
            Description := GreenTLS_Alert_Message.Description;
            Alert := TLS_Alert::Alert'(Level => TLS_Alert::Fatal, Description => Description);

Ensure: Handshake_Control_Message'Valid, GreenTLS_Alert_Message'Valid and Description /= Close_Notify and Description /= User_Canceled

E3

            TLS_Inner_Plaintext := Decrypt (Server_Key_Update_Message, Server_Sequence_Number, TLS_Record_Message.Encrypted_Record);

Ensure: Server_Key_Update_Message'Valid and TLS_Record_Message'Valid and TLS_Record_Message.Tag = Application_Data and TLS_Record_Message.Legacy_Record_Version = TLS_1_2

E4-6

#292 (comment)

E7 Integer overflows

#687

Considered Options

O1 State contracts

• Use pre- and post-conditions to ensure properties in and between states
• Pre-conditions must be explicitly defined
• Post-conditions correspond to conditions of transitions
• Verification: All conditions of incoming transitions of state must fulfill pre-condition
• Example based on E2:

      state A with
         Pre => Handshake_Control_Message'Valid
      is
      begin
            GreenTLS_Alert_Message = GreenTLS::Alert_Message (Handshake_Control_Message.Data);
      transition
         then B
            if GreenTLS_Alert_Message'Valid
         then Error_State
      end A;

      state B with
         Pre => GreenTLS_Alert_Message'Valid
      is
      begin
            Description := GreenTLS_Alert_Message.Description;
      transition
         then C
            if Description /= Close_Notify and Description /= User_Canceled
         then Error_State
      end B;

      state C with
         Pre => Description = Close_Notify and Description = User_Canceled
      is
      begin
            Alert := TLS_Alert::Alert'(Level => TLS_Alert::Fatal, Description => Description);
            [...]
      end C;            

+ Contracts are well-known concept
− Many small states needed for common operations

O2 Conditional transitions

• Use statement to check condition and change state: transition TARGET_STATE if CONDITION
• Example based on E2:

            transition Error_State if not Handshake_Control_Message'Valid;
            GreenTLS_Alert_Message := GreenTLS::Alert_Message (Handshake_Control_Message.Data);
            transition Error_State if not GreenTLS_Alert_Message'Valid;
            Description := GreenTLS_Alert_Message.Description;
            transition Error_State if Description = Close_Notify or Description = User_Canceled;
            Alert := TLS_Alert::Alert'(Level => TLS_Alert::Fatal, Description => Description);

• Could replace transition block completely by having a mandatory transition TARGET_STATE as last statement in a state

+ Simple and flexible
+ Enables transitions as early as possible
+ Avoids additional states just for checking conditions
− Repetition of already defined properties
− Repetitive declaration of transitions to the same error state

O3 Exceptions

         begin
            GreenTLS_Alert_Message = GreenTLS::Alert_Message (Handshake_Control_Message.Data);
            Description := GreenTLS_Alert_Message.Description;
            Alert := TLS_Alert::Alert'(Level => TLS_Alert::Fatal, Description => Description);
            [...]
         transition
            then Next_State_1
               if Description = Foo
            then Next_State_2
         exception
            then Error_State
               when Constraint_Error
            then Fatal_Error_State
               when Fatal_Error
         end [...];

+ Good readability (no repetition of already defined properties or splitting in multiple states necessary)
+ Extendable by more expressive exceptions (i.e., matching constraints which led to the exception)

Decision Outcome

O3

Tasks

• Generation of VCs for state actions #861
• Implicit preconditions for states #862

[sttaft]

Having transitions interspersed among other statements is simpler in one sense, but it certainly results in more complex overall control flow, with partial sets of effects executed within a state depending on when the transition out of the state is encountered. One question is whether transition statements could occur anywhere, including within the body of a loop (if such a notion exists in RecordFlux). Should a transition statement be treated roughly the same as a "return" or "exit" statement in Ada?

If a state is treated like a function that returns the identity of the next state to be visited, then interspersing conditional transition statements would be analogous to what you could do in Ada with conditional return statements. There are coding conventions that frown on such "early" return statements, and they can cause maintenance headaches if you add some code at the end of a function presuming that it will be reached on every execution of the function. Similarly, allowing "early" transition statements means that it is less clear which statements within the state are executed on every "visit" of the state.

Some sort of special indenting of transition statements might be justified so they don't just disappear when occurring within a long block of statements.

[treiher]

One question is whether transition statements could occur anywhere, including within the body of a loop (if such a notion exists in RecordFlux).

There are no loop statements or other "block" statements in RecordFlux. So I do not see the need to restrict the occurrence of transition statements.

Should a transition statement be treated roughly the same as a "return" or "exit" statement in Ada?

Yes, I think so.

If a state is treated like a function that returns the identity of the next state to be visited, then interspersing conditional transition statements would be analogous to what you could do in Ada with conditional return statements. There are coding conventions that frown on such "early" return statements, and they can cause maintenance headaches if you add some code at the end of a function presuming that it will be reached on every execution of the function. Similarly, allowing "early" transition statements means that it is less clear which statements within the state are executed on every "visit" of the state.

I see that there are advantages and disadvantages of "early" return statements. Personally, I have the feeling that the advantages of "early" return statements outweigh their disadvantages.

Some sort of special indenting of transition statements might be justified so they don't just disappear when occurring within a long block of statements.

That makes sense, although indenting such a statement seems uncommon to me. At least, I'm not aware of a similar convention in any programming language. I think having syntax highlighting where transition is emphasized would also significantly improve the readability.

[sttaft]

As an example of indenting/outdenting, I have seen the Ada "exit" statement outdented as follows:

   loop
        Do_Something;
   exit when A > B;
        Do_More;
   end loop;

Something like this might be useful for transition statements.

I am not a fan of relying on syntax highlighting as the only indicator of something significant, since there are plenty of contexts where the highlighting will not be available.