Learn, Check, Test -- Security Testing Using Automata Learning and Model Checking
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866918359831937024 |
|---|---|
| author | Marksteiner, Stefan Sjödin, Mikael Sirjani, Marjan |
| author_facet | Marksteiner, Stefan Sjödin, Mikael Sirjani, Marjan |
| contents | Security verification of communication protocols in industrial and safety-critical systems is challenging because implementations are often proprietary, accessible only as black boxes, and too complex for manual modeling. As a result, existing security testing approaches usually depend on incomplete test suites and/or require labor-intensive modeling, limiting coverage, scalability, and trust. This paper addresses the problem of systematically verifying protocol security-properties without access to internal system models. We propose a flexible and scalable method for formal verification of communication protocols that combines active automata learning with model checking to enable rigorous security analysis of black-box protocol implementations. The key contributions include: (i) a method for augmenting learned protocol models with security-relevant propositions, (ii) a fully automated transformation pipeline from learned models to model-checking artifacts, (iii) reusable, generic security property templates that are instantiated in protocol-specific models, and (iv) empirical validation through case studies demonstrating applicability in different protocols and domains. The results show that the approach enables scalable and systematic discovery of security vulnerabilities in black-box systems while reducing modeling effort and improving automation compared with traditional verification workflows. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_22215 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Learn, Check, Test -- Security Testing Using Automata Learning and Model Checking Marksteiner, Stefan Sjödin, Mikael Sirjani, Marjan Cryptography and Security Formal Languages and Automata Theory D.2.4; F.3.1; K.6.5 Security verification of communication protocols in industrial and safety-critical systems is challenging because implementations are often proprietary, accessible only as black boxes, and too complex for manual modeling. As a result, existing security testing approaches usually depend on incomplete test suites and/or require labor-intensive modeling, limiting coverage, scalability, and trust. This paper addresses the problem of systematically verifying protocol security-properties without access to internal system models. We propose a flexible and scalable method for formal verification of communication protocols that combines active automata learning with model checking to enable rigorous security analysis of black-box protocol implementations. The key contributions include: (i) a method for augmenting learned protocol models with security-relevant propositions, (ii) a fully automated transformation pipeline from learned models to model-checking artifacts, (iii) reusable, generic security property templates that are instantiated in protocol-specific models, and (iv) empirical validation through case studies demonstrating applicability in different protocols and domains. The results show that the approach enables scalable and systematic discovery of security vulnerabilities in black-box systems while reducing modeling effort and improving automation compared with traditional verification workflows. |
| title | Learn, Check, Test -- Security Testing Using Automata Learning and Model Checking |
| topic | Cryptography and Security Formal Languages and Automata Theory D.2.4; F.3.1; K.6.5 |
| url | https://arxiv.org/abs/2509.22215 |