Date: Tuesday July 7th and Wednesday July 8th Location: Campus Cyber (5-7 rue Bellini, La Défense, Metro 1 Station “Esplanade de la Défense”)
The workshop will take place in the Campus Cyber (5-7 rue Bellini, La Défense, Metro 1 Station “Esplanade de la Défense”)
The room for the presentation will be at the Inria floor (3rd floor).
Network protocol fingerprinting is used to identify a protocol implementation by analyzing its input-output behavior. Traditionally, fingerprinting operates under a closed-world assumption, where models of all implementations are assumed to be available. However, this assumption is unrealistic in practice. When this assumption does not hold, fingerprinting results in numerous misclassifications without indicating that a model for an implementation is missing. Therefore, we introduce an open-world variant of the fingerprinting problem, where not all models are known in advance. We propose an incremental fingerprinting approach to solve the problem by combining active automata learning with closed-world fingerprinting. Our approach quickly determines whether the implementation under consideration matches an available model using fingerprinting and conformance checking. If no match is found, it learns a new model by exploiting the structure of available models. We prove the correctness of our approach and improvements in asymptotic complexity compared to naive baselines. Moreover, experimental results on a variety of protocols demonstrate a significant reduction in misclassifications and interactions with these black boxes.
Extended version of the CSF 2026 paper
This work focuses on the application of Active Automata Learning to the Remote Desktop Protocol (RDP). The objective is to develop a mapper capable of translating abstract learning queries into valide RDP network messages and interpreting the corresponding responses, which enables the inference of protocol state machines. The resulting models provide insights into protocol behavior, implementation correctness, and fingerprinting.
Paper to be presented at WOOT 26
TCP stateful flow reconstruction is a critical aspect of network traffic analysis. We use process algebra to build midpoint finite state machine (FSM) from single TCP FSM, and then, test implementations. This presentation describes our current progress.
Symbolic formal verification of cryptographic protocols based on the Dolev-Yao (DY) attacker model—an active attacker with full network control and perfect cryptography—is well-established for finding design-level logical flaws in cryptographic protocols. Building on this, DYF enriches fuzzing with this attacker model to uncover logical bugs at the implementation level. In contrast to bit-level fuzzers (e.g., AFL), DYF leverages a formal model of messages and cryptography to generate structured, adversarial executions, such as replaying and re-signing a modified payload. However, a significant limitation of DYF is the requirement to precisely model properties to check at runtime (e.g., session parameter agreement). Defining these properties is labor-intensive and inherently non-exhaustive, often necessitating complex instrumentation of the PUTs. Consequently, typically only a subset of logical attacks is detected. We address this limitation by introducing DDYF based on a differential oracle to compare executions across different protocol implementations. By interpreting discrepancies through the DY model, it identifies semantic differences indicative of bugs or vulnerabilities, effectively minimizing false positives. We propose a generic design for DDYF, implement it within the Puffin DY fuzzer, and evaluate it on four major TLS implementations. Our results demonstrate that DDYF can detect vulnerabilities that evade state-of-the-art fuzzers, specifically those requiring DY attacker capabilities (missed by bit-level differential fuzzers) or complex objective oracles (missed by DYF). DDYF also uncovered numerous new RFC violations in OpenSSL, BoringSSL, wolfSSL, and LibreSSL, which are by-design hardly detectable with non-differential oracles. Furthermore, we show that DDYF exposes fine-grained behavioral discrepancies, enabling more precise fingerprinting of protocol implementations than prior works.
When fuzzing network protocol programs, passive automata learning can be used to infer state models. These state models can be used for several applications, including bench- marking fuzzers, differential fuzzing of multiple SUTs, and improving test case generation. In this paper, we analyse the practical challenges with this. We compare models inferred using passive and active automata learning in a case study on the FTP protocol. Our results show that, with an appropriate input abstraction function, passive learning can be used to infer state models from traces collected during fuzzing.
Over the past few years, Active Automata Learning (AAL) algorithms have been used to extract Mealy machines representing the logical behavior of various network protocol implementations. Multiple logical vulnerabilities were discovered in various implementations (e.g. TLS, SSH, TCP, OPC~UA). AAL algorithms iteratively propose a candidate automaton to an oracle which either validates the candidate or propose a counter-example which falsifies the candidate model.
A perfect oracle for an implementation does not exist, hence it is approximated with conformance testing algorithms with a fundamental trade-off between exhaustiveness and time complexity. In particular, deep states are out of reach for conformance testing algorithms, but they may hide logical bugs or voluntary backdoors. In this paper, we propose a greybox oracle named Memorix which uses memory inspection and concolic execution to build an abstract model of the implementation. By running reachability analysis on the abstract model, Memorix can identify missing deep states and encode them as I/O counter-examples for AAL.
We show that Memorix successfully identifies deep states in TLS 1.2, TLS 1.3 and SSH implementations which are out of reach for conformance testing oracles. We compare Memorix with another greybox oracle and show that Memorix models are more complete and always sound at the expense of a small runtime overhead.
We present a differential symbolic execution technique that removes reliance on an explicitly encoding requirement checks by comparing implementations on the same interaction while exploring classes of inputs. We applied our technique to the most recent versions of several widely used DTLS implementations and detected nine distinct bugs across versions, including five that were previously unknown and were later fixed or confirmed.
Active automata learning (AAL) algorithms can learn a behavioral model of a system from interacting with it. The primary challenge remains scaling to larger models, in particular in the presence of many possible inputs to the system. Modern AAL algorithms fail to scale even if, in every state, most inputs lead to errors. In various challenging problems from the literature, these errors are observable, i.e., they emit a known error output. Motivated by these problems, we study learning these systems more efficiently. Further, we consider various degrees of knowledge about which inputs are non-error producing at which state. For each level of knowledge, we provide a matching adaptation of the state-of-the-art AAL algorithm L# to make the most of this domain knowledge. Our empirical evaluation demonstrates that the methods accelerate learning by orders of magnitude with strong but realistic domain knowledge to a single order of magnitude with limited domain knowledge.
Information about the previous workshop in 2024 is available here