Catégorie: Conférence avec actes
Auteurs: Arthur Tran Van, Olivier Levillain et Hervé Debar
Date: juillet 2024

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.

Publié dans les actes Proceedings of the 19th International Conference on Availability, Reliability and Security (pages 1 à 10)

Présenté lors de la conférence ARES à Vienna, Austria en juillet 2024

BibTeX Document Lien vers l'article en Open Access