Language-Based Protocol Testing

TL;DR

This paper introduces language-based protocol testing, the first approach to specify, automatically test, and systematically cover the full state and input space of protocol implementations, as part of the FANDANGO test generator.

Abstract

Over the past decade, the automated generation of test inputs has made significant advances. Modern fuzzers and test generators easily produce complex input formats that do systematically cover the input and execution space. Testing _protocols_, though, has remained a frontier for automated testing, as a test generator has to _interact_ with the program under test, producing messages that conform to the current state of the system. In this paper, we introduce _language-based protocol testing_, the first approach to specify, automatically test, and systematically cover the full state and input space of protocol implementations. We specify protocols as _interaction grammars_ -- an extension of context-free grammars that tag each message element with the communication party that is in charge of producing it. Interaction grammars embed classical state models by unifying states, messages, and transitions all into nonterminals, and can be used for _producing_ interactions as well as _parsing_ them, making them ideally suited for testing protocols. Additional _constraints_ over grammar elements allow us to specify and test _semantic features_ such as binary message formats, checksums, encodings, and the many ways that message features induce states and vice versa. To evaluate the effectiveness of language-based protocol testing, we have implemented it as part of the FANDANGO test generator. We specify several protocols as interaction grammars, including features such as human-readable interactions (SMTP), bit-level encodings (DNS), and dynamic port assignments (FTP), and use them to test the corresponding protocol implementations. By systematically covering the interaction grammar and solving the associated constraints, FANDANGO achieves comprehensive coverage of the protocol interactions, resulting in high code coverage and a thorough assessment of the program under test.

Figures (15)

• Figure 1: A simple SMTP interaction
• Figure 2: A state model for the SMTP protocol, specifying possible sequences of client and server messages. The concrete messages exchanged have been replaced with symbolic placeholders such as $\langle$server:id$\rangle$ or $\langle$client:HELO$\rangle$ to indicate which party is sending the message. The model does not specify the actual content or format of these messages.
• Figure 3: An grammar for the interaction in \ref{['fig:smtp-sequence']}. email and hostname are defined externally; message is a regular expression.
• Figure 4: Processing grammars. After parsing an grammar specification, 1 initializes party definitions and generates an empty derivation tree. The forecaster2 predicts possible upcoming protocol message types. If these include messages from fuzzer-controlled parties and no external messages have been received, our coverage guidance 3 selects message types for generation 4. If no external message is received, 5 a generated message is transmitted. Otherwise, if an external message is received, 6 it is parsed immediately. Finally, 7 the resulting derivation tree is validated. The process repeats until the forecaster predicts no further messages.
• Figure 5: Partial derivation tree produced by the grammar in \ref{['fig:smtp-grammar']}. Each node inherits the sender and receiver from $\pi(A)$, and maintains a mutable read_only flag ().

Theorems & Definitions (3)

• Definition 1: Grammar
• Definition 2: Grammar
• Definition 3: Constrained Grammar