Abstract Existing active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines or deterministic finite automata. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this article, we present $${SL}^{\lambda }$$ SL λ , an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of membership queries required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We prove that $${SL}^{\lambda }$$ SL λ is guaranteed to learn an acceptor, in the form of a register automaton with n locations and t transitions, for a given data language of finite index, and that it can do so with at most $$O(t^2 \, (2n)^n + m t^2 \, m^m)$$ O ( t 2 ( 2 n ) n + m t 2 m m ) membership queries and O ( t ) equivalence queries, where m is the length of the longest counterexample received during learning. We have implemented $${SL}^{\lambda }$$ SL λ as a new algorithm in RALib. We evaluate its performance by comparing it against $${SL}^{*}$$ SL ∗ , the current state-of-the-art RA learning algorithm. Experiments on a series of benchmarks show that it reduces the number of membership queries by up to an order of magnitude, and also shows substantial asymptotic improvements in bigger systems.

Implementations of stateful network protocols must keep track of the presence, order and type of exchanged messages. Any errors, so-called state machine bugs, can compromise security. SMBugFinder provides an automated framework for detecting these bugs in network protocol implementations using black-box testing. It takes as input a state machine model of the protocol implementation which is tested and a catalogue of bug patterns for the protocol conveniently specified as finite automata. It then produces sequences that expose the catalogued bugs in the tested implementation. Connection to a harness allows SMBugFinder to validate these sequences. The technique behind SMBugFinder has been evaluated successfully on DTLS and SSH in prior work. In this paper, we provide a user-level view of the tool using the EDHOC protocol as an example.

Abstract Existing active automata learning (AAL) algorithms have demonstrated their potential in capturing the behavior of complex systems (e.g., in analyzing network protocol implementations). The most widely used AAL algorithms generate finite state machine models, such as Mealy machines. For many analysis tasks, however, it is crucial to generate richer classes of models that also show how relations between data parameters affect system behavior. Such models have shown potential to uncover critical bugs, but their learning algorithms do not scale beyond small and well curated experiments. In this paper, we present $${SL}^{\lambda }$$ SL λ , an effective and scalable register automata (RA) learning algorithm that significantly reduces the number of tests required for inferring models. It achieves this by combining a tree-based cost-efficient data structure with mechanisms for computing short and restricted tests. We have implemented $${SL}^{\lambda }$$ SL λ as a new algorithm in RALib. We evaluate its performance by comparing it against $${SL}^{*}$$ SL ∗ , the current state-of-the-art RA learning algorithm, in a series of experiments, and show superior performance and substantial asymptotic improvements in bigger systems.

DTLS-Fuzzer is a protocol state fuzzer for imple-mentations of DTLS clients and servers. DTLS-Fuzzer uses model learning to generate a state machine model of a DTLS implementation, capturing its input/output behavior. This model can be used for model-based testing or can be analyzed for security vulnerabilities and specification violations. This demo abstract overviews the architecture, API, and usage of the tool.