Symbolic verification for the identification of critical failure-chain scenarios in flight control systems
Lade...
Autor:in (Körperschaft)
Publikationsdatum
2025
Typ der Arbeit
Studiengang
Typ
04B - Beitrag Konferenzschrift
Herausgeber:innen
Herausgeber:in (Körperschaft)
Betreuer:in
Übergeordnetes Werk
Deutscher Luft- und Raumfahrtkongress Publications
Themenheft
DOI der Originalpublikation
Link
Reihe / Serie
Reihennummer
Jahrgang / Band
Ausgabe / Nummer
Seiten / Dauer
Patentnummer
Verlag / Herausgebende Institution
Deutsche Gesellschaft für Luft-und Raumfahrt
Verlagsort / Veranstaltungsort
Bonn
Auflage
Version
Programmiersprache
Abtretungsempfänger:in
Praxispartner:in/Auftraggeber:in
Zusammenfassung
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.
Schlagwörter
Veranstaltung
74. Deutscher Luft-und Raumfahrtkongress 2025
Startdatum der Ausstellung
Enddatum der Ausstellung
Startdatum der Konferenz
23.09.2025
Enddatum der Konferenz
25.09.2025
Datum der letzten Prüfung
ISBN
ISSN
Sprache
Englisch
Während FHNW Zugehörigkeit erstellt
Ja
Zukunftsfelder FHNW
Publikationsstatus
Veröffentlicht
Begutachtung
Peer-Review des Abstracts
Open Access-Status
Closed
Lizenz
Zitation
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