What is it about?
This research presents a method for automatically learning behavioral models of black-box communication protocols and transforming them into formally verifiable security models. By combining automata learning, model checking, and automated test generation, the approach enables the systematic analysis of proprietary systems without requiring source code or design documentation. The method was demonstrated on both automotive ECUs and electronic passports, showing its applicability across different domains.
Featured Image
Photo by Privecstasy on Unsplash
Why is it important?
Many security-critical systems are proprietary black boxes, making rigorous security assessment difficult and expensive. This work enables formal security verification without requiring source code, design documentation, or labor-intensive manual modeling by automatically learning verifiable models from observed behavior. As a result, security properties can be checked systematically, vulnerabilities can be identified earlier, and test cases can be generated automatically, increasing assurance while reducing analysis effort for systems such as vehicles and electronic passports.
Perspectives
My research focuses on enabling trustworthy security guarantees for complex systems whose internal design is unavailable or prohibitively expensive to model manually. By combining automated model acquisition, formal methods, and security engineering, I investigate how observable system behavior can be transformed into analyzable artifacts that support verification, validation, testing, and continuous security assurance.
Stefan Marksteiner
AIT Austrian Institute of Technology
Read the Original
This page is a summary of: From automata learning to model checking: Formal security verification of black-box protocols, Computers & Security, January 2027, Elsevier,
DOI: 10.1016/j.cose.2026.105168.
You can read the full text:
Contributors
The following have contributed to this page
