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.
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.
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.
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).