Members can download this article in PDF format.
What you’ll learn:
The simple steps toward developing a complex message specification using RecordFlux.
How to implement this specification in Ada/SPARK application code.
Translating a message specification from paper to code can be complicated and prone to error. In the best-case scenario, all aspects of the message specification are implemented in program code, housed in structures, with potentially thousands of lines of defensive coding and/or exception handling to catch potential errors. Each received message could become complex if conditions, case statements or subprograms may be required to verify message validity.
Not only is this process cumbersome for the application developer, it also makes maintaining the application difficult to nearly impossible. And testing and debugging… even worse! Tracing through thousands of lines of code and conditions is a time-consuming process. Any errors that slip through could expose the entire application to severe security issues as well (think cyber exploits).
Enter RecordFlux. RecordFlux is a powerful tool for implementing secure message specifications. The power in this tool lies in its ability to generate provable SPARK code from a specification and simplify the process of translating a protocol from paper to code. How does this translate to the application developer?
The message specification is isolated to a RecordFlux file. Using the RecordFlux language, developers can strictly define message flow, constraints, bounds, and so forth—all things that, if embedded into a normal application, could take up thousands of lines with defensive coding practices. The SPARK code generated from the RecordFlux file, when implemented in code, ensures that the message implementation in the application is provable, safe, and secure.
In this article, we’ll walk through the initial process of implementing a RecordFlux specification for a real-world protocol. We’ll also describe the process of putting the RecordFlux-generated code to work in a simple set of client/server applications. This provides a full picture of how to carry something from “protocol description” to “application reality.”
The Protocol (and Example Scope)
The protocol I chose to implement for this example is the Datagram Congestion Control Protocol (DCCP). I’ll only lightly describe the protocol here, since the focus for this discussion is RecordFlux, not the minutiae of DCCP.
DCCP is a transport layer protocol that provides a reliable means to negotiate connections (from connection to closure) and offers built-in congestion control mechanisms. It operates similarly to TCP but doesn’t guarantee that messages will be delivered in order.
DCCP isn’t a widely used protocol, but can offer advantages for streaming media, gaming, telemetry, and other applications in which timing (low latency) and reliability are highly valued. RFC 4340 outlines the basic protocol structure as composed of a DCCP Header followed by an Application Data Area (Fig. 1).