Defense Policy Optimization With Linear Temporal Logic Specifications for Interconnected Networks
Armita Kazeminajafabadi, Derya Aksaray, Mahdi Imani · 2025
The increasing interconnection of aerospace systems presents significant security challenges. The protection of these systems must be achieved with minimal disruptions to system operations while ensuring the desired specifications and network security. This paper presents network security through Bayesian attack graphs (BAGs), a powerful class of models that captures stochasticity in attacks and their propagation. The security objective involves dynamically defending the network with limited available resources to ensure the network is secure and stop the propagation of any potential intrusions. Despite the development of several defense and security solutions for BAGs, these methods mostly optimize specific security metrics without providing guarantees in terms of violations of practical security constraints, making them unsafe or inapplicable to sensitive and complex aerospace systems. This paper models security constraints using temporal logic (TL) specifications. Specifically, we formalize a set of specifications regarding resource availability, network security, servers’ maintenance requirements, and more as Linear Temporal Logic (LTL) specifications. An automaton-theoretic approach is used to compute feasible policies that guarantee the satisfaction of the desired LTL specifications. Since feasible policies achieve different security performances, this paper develops an efficient security algorithm that selects a policy (among a set of desired feasible policies) yielding the highest expected lookahead security performance in every horizon of a specified length. Numerical experiments demonstrate the effectiveness of the proposed framework in proactively responding to threats and meeting specifications under various conditions.