Testing Protocols with Formal Languages

Summary

Communication protocols involve stateful interactions between multiple parties, which makes systematic testing of their implementations challenging. Test inputs are not single messages, but sequences of syntactically and semantically dependent exchanges whose validity depends on prior communication and protocol state. This work proposes a protocol testing approach that systematically explores a protocol specification. We extend the specification format of fandango such that it is able to specify protocol state, syntax, and semantics within a single file. The format combines context-free grammars with Turing-complete constraints and role-annotated nonterminals to describe multi-party behavior and cross-message dependencies. Specifications are role-neutral and can be applied to any participant in the protocol. We applied our technique to dns, smtp, ftp, a rest-style api, and a ChatGPT interaction grammar. Initial results show that our approach is able to drive communication with a system under test and that the k-path-guided exploration technique quickly achieves coverage across grammar structure, inputs, outputs, and protocol state.