Symbolic verification for the identification of critical failure-chain scenarios in flight control systems

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.