RecordFlux State Machines

by Fabien Chouteau – May 15, 2023

In a previous post we presented the RecordFlux specification language and toolset, illustrating how to design and generate formally proven binary protocol parsers and serializers. In this follow-up we will look at the protocol session part of RecordFlux.

Communication protocols are more than just binary packet definitions, they also define behaviors which are often modeled as state machines. In addition to the binary messages that we saw in the previous post, the RecordFlux language also allows the specification of state machines and the generation of the corresponding SPARK code.

Protocol Session

A RecordFlux protocol session is defined as follows:

generic
 <session_parameters>
session S is
 <session_declarations>
begin
 <states>
end S

The session parameters can be either channels to receive and send messages, or subprograms to provide execution of external code. States define the various protocol states and transitions between them. Although the syntax is based on Ada generic templates, this is simply to reflect the general-purpose nature of sessions; there is no analog of generic instantiation in application code.

To continue with our example from the first post, we will now specify a state machine for the server side of our protocol that uses a stack data structure for retrieving and storing messages.

For the sessions parameters we need:

A channel to read and write messages
A subprogram to store data on a stack
A subprogram to retrieve data from a stack

This is what it looks like in our specification:

type Store_Result is (Store_Ok, Store_Fail)
   with Size => 8;

   generic
  	Chan : Channel with Readable, Writable;
  	with function Store_Data (Stack_Id : Stack_Identifier; Data : Opaque) return Store_Result;
  	with function Get_Data (Stack_Id : Stack_Identifier) return Payload;
   session Server is

As you can see, a new type is declared to provide the result of a store action. Storing data on a stack can fail if the stack is full. The channel is both Readable and Writable, as we will send responses on the same channel as we receive requests. Finally, we have two functions to store and retrieve data.

We also have a few declarations that are going to be used across multiple states:

session Server is
   Request : RSP_Message;
   Answer  : RSP_Message;
   Result  : Server_Result_Kind;
begin

For example, a message is received and validated in a given state, but its content is used in another state.

Now let’s have a look at the state machine.

State Machine

A state is defined as follows:

state A is
   <state_declarations>
begin
   <state_actions>
transition
   <transitions or conditional_transitions>
exception
   <exception_transition>
end A

Here is the definition of the first state for our server:

state Receive_Request is
begin
   Chan'Read (Request);
transition
   goto Invalid_Packet_Error    if Request'Valid = False
   goto Got_Answer_Packet_Error if Request.Kind /= Request_Msg
   goto Store                   if Request.Request_Kind = Request_Store
   goto Get                     if Request.Request_Kind = Request_Get
   goto Exception_Error
end Receive_Request;

We have one action, which is to receive a message from the channel. This action is blocking until a full message is received. And then a few transitions depending on the validity and content of the message.

The other state that we are going to look at is “Store”, which is the next state if we receive a valid Request_Store message:

state Store is
   St_Result : Store_Result;
begin
   St_Result := Store_Data (Request.Request_Stack_Id,
                            Request.Request_Payload_Data);
transition
   goto Stack_Full_Error if St_Result = Store_Fail
   goto Answer_Success
exception
   goto Exception_Error
end Store;

This state is interesting because this is where one of the session functions is called. We take the stack identifier and payload data from the valid Request_Store message and pass it to “Store_Data ()”, and we get a Store_Result. In the generated code, this will translate to a call to a subprogram of the `Server.Context` abstract type.

To implement the functional part of our server, we just have to declare a type that derives from `Server.Context` and implement the two session functions:

type Context is new RFLX.RSP.Server.Context with private;

overriding
procedure Store_Data (Ctx         : in out Context;
                      Stack_Id    : RFLX.RSP.Stack_Identifier;
                      Data        : RFLX.RFLX_Types.Bytes;
                      RFLX_Result : out RFLX.RSP.Store_Result);

overriding
procedure Get_Data (Ctx         : in out Context;
                    Stack_Id    : RFLX.RSP.Stack_Identifier;
                    RFLX_Result : out RFLX.RSP.Payload.Structure);

Besides the communication boilerplate, this is the only piece of Ada/SPARK code that is required to implement the server, everything else is generated from the RecordFlux specification. If you want to have a look at the actual code for this example it is available here.

Conclusion

Similar to the message part of RecordFlux, state machine definitions allow the developer to focus on the specification of a protocol. The automated code generation saves time and effort, eliminating the need to write the lower level code, and thus increases the safety and security of the software.

If you want to see an example covering existing protocols, the RecordFlux repository contains a DHCP client implemented with the state machine specifications. Additional information about RecordFlux may be found on the AdaCore web site, including a link to a technical paper showing NVIDIA’s use of RecordFlux in implementing SPDM (Security Protocol and Data Model).

Posted in

About Fabien Chouteau

Fabien joined AdaCore in 2010 after his engineering degree at the EPITA (Paris). He is involved in real-time, embedded and hardware simulation technology. Maker/DIYer in his spare time, his projects include electronics, music and woodworking.