Mealy Verifier: An Automated, Exhaustive, and Explainable Methodology for Analyzing State Machines in Protocol Implementations

Many network protocol specifications are long and lack clarity, which paves the way to implementation errors. Such errors have led to vulnerabilities for secure protocols such as SSH and TLS. Active automata learning, a black-box method, is an efficient method to discover discrepancies between a specification and its implementation. It consists in extracting state machines by interacting with a network stack. It can be (and has been) combined with model checking to analyze the obtained state machines. Model checking is designed for exhibiting a single model violation instead of all model violations and thus leads to a limited understanding of implementation errors. As far as we are aware, there is only one specialized exhaustive method available for analyzing the outcomes of active automata learning applied to network protocols,Fiterau-Brostean's method. We propose an alternative method, to improve the discovery of new bugs and vulnerabilities and enhance the exhaustiveness of model verification processes. In this article, we apply our method to two use cases: SSH, where we focus on the analysis of existing state machines and OPC UA, for which we present a full workflow from state machine inference to state machine analysis.