Symbolic verification for the identification of critical failure-chain scenarios in flight control systems
Loading...
Author (Corporation)
Publication date
2025
Typ of student thesis
Course of study
Collections
Type
04B - Conference paper
Editors
Editor (Corporation)
Supervisor
Parent work
Deutscher Luft- und Raumfahrtkongress Publications
Special issue
DOI of the original publication
Link
Series
Series number
Volume
Issue / Number
Pages / Duration
Patent number
Publisher / Publishing institution
Deutsche Gesellschaft für Luft-und Raumfahrt
Place of publication / Event location
Bonn
Edition
Version
Programming language
Assignee
Practice partner / Client
Abstract
Flight control systems now integrate more digital electronics and networked subsystems than ever before, creating unprecedented opportunities for cascading failures triggered by cyber attacks. Traditional safety analysis methods fail to capture the complex interdependencies that enable attackers to orchestrate multi-component failures, particularly in safety-critical domains such as aviation. This paper presents two complementary tools for analyzing security vulnerabilities in flight control systems and other cyber-physical systems: TraceGuard, which performs taint-guided symbolic execution for efficient vulnerability discovery in individual components, and MCS Analyser, which models inter-component communication to identify system-level failure chains. TraceGuard extends the angr symbolic execution framework with intelligent path prioritization based on taint tracking, focusing computational resources on security-relevant execution paths. MCS Analyser employs a three-phase approach to discover communication patterns, analyze message flows, and construct comprehensive system models. Our evaluation demonstrates significant improvements over existing approaches. TraceGuard achieved up to 5× improvement in vulnerability discovery (finding 5 vulnerabilities versus 1 in complex test cases) while exploring only 36.8% to 75% of basic blocks. The taint-guided prioritization successfully maintains 100% vulnerability detection while dramatically reducing computational overhead. MCS Analyser analyzed a 12-component UAV simulation, discovering 42 unique message flows and identifying 15 tainted propagation paths that could enable cascading failures. The integration of these tools enables identification of edge-case attack scenarios requiring precise coordination of multiple component states—situations with negligible natural probability but achievable through deliberate attacks. Expert validation from aerospace industry confirms the practical value of automated communication path discovery and edge-case identification. The framework provides engineers with concrete evidence for security design decisions, supporting rigorous security-by-design practices in cyber-physical systems development.
Keywords
Event
74. Deutscher Luft-und Raumfahrtkongress 2025
Exhibition start date
Exhibition end date
Conference start date
23.09.2025
Conference end date
25.09.2025
Date of the last check
ISBN
ISSN
Language
English
Created during FHNW affiliation
Yes
Strategic action fields FHNW
Publication status
Published
Review
Peer review of the abstract
Open access category
Closed
License
Citation
Scherb, C., Trapp, A., Hutter, R., Bachmann, N., & Heitz, L. (2025). Symbolic verification for the identification of critical failure-chain scenarios in flight control systems. Deutscher Luft- Und Raumfahrtkongress Publications. 74. Deutscher Luft-und Raumfahrtkongress 2025. https://irf.fhnw.ch/handle/11654/53225