Formal Modeling and Verification of Deep Reinforcement Learning Agents for Secure and Available Autonomous Cyber Defense

This paper presents a hybrid Formal Verification (FV) methodology for Deep Reinforcement Learning (DRL) agents for Autonomous Cyber Defense (ACD) in dynamic cyber threat environments. The approach verifies multiple dependability properties, including safety, robustness, availability, and fairness, under adversarial uncertainty. To enable tractable probabilistic model checking, the methodology models only the stochastic attacker behavior in the formal model, while the defender's deterministic policy is executed externally. This separation allows the construction of a policy-induced Markov chain that captures adversarial dynamics under uncertainty. To further improve scalability, we apply a design-for-verification principle that replaces dynamic deception with a static strategy at episode start, preserving defender performance and preventing statespace explosion. The methodology is instantiated in the CAGE Challenge 2 environment, implemented in the CybORG and CybORG++ simulators. Across these environments, we analyze how defender policies and deception strategies influence verified dependability guarantees. Results show that dependability properties are sensitive to attacker success probabilities and deception strategies, revealing quantifiable trade-offs between cybersecurity objectives and system functionality. These findings demonstrate the practical value of the methodology for strengthening DRLbased ACD agents in critical network environments.