Resiliency analysis of mission-critical systems using formal methods

Abstract

Mission-critical systems, such as navigational spacecraft and drone surveillance systems, play a crucial role in a nation's safety and security. These systems consist of heterogeneous systems that work together to accomplish critical missions. However, they are susceptible to cyberattacks and physical incidents that can have devastating consequences. Thus, missions must be designed so that mission-critical systems can withstand adverse events and continue to operate effectively, even with the occurrence of adverse events. In other words, critical mission engineers must specify, analyze, and anticipate potential threats, identify where adverse events may occur, and develop mitigation strategies before deploying a mission-critical system. This work presents an end-to-end methodology for analyzing the resiliency of critical missions. The methodology first specifies a mission in the form of a workflow. The mission workflow is then converted into a formal representation using Colored Petri Nets (CPN). Threat models are also extracted from the mission specification to tackle the CPN mission with various attack scenarios. These threat models are represented as CPN attacks. The methodology exploits the state transitions of the CPN mission attached to CPN attacks to analyze the resiliency of the mission. The analysis identifies which states the mission succeeds, fails, and is incomplete. We established a mission for a mission-critical formation consisting of a military vehicle and two route reconnaissance drones that collaborate to monitor a national border and respond promptly to physical threats. The effectiveness of the methodology is demonstrated in identifying vulnerabilities, modeling adversarial conditions, and evaluating mission continuity under disruptions. The result shows how to refine the mission to enhance the resilience of such formations. The findings contribute to the early-stage resilience analysis framework and help address the limitations associated with manual verification of mission-critical systems.