Active Cyber Defense Strategy through Multi-Agent Systems Verification
Active cyber defense offers a promising approach to addressing the longstanding asymmetry between rapidly evolving cyber threats and static defense systems. However, active cyber defense requires fast responses and proactive reconfigurations that must be verified and tailored to observed attacker behaviour. Formal methods rely on rigorous mathematical and logical frameworks for verifying system specifications under welldefined assumptions. In particular, multi-agent system (MAS) verification, which examines formal properties of open systems, is well-suited for cybersecurity where attacker-defender interactions are central. This paper bridges the gap between system security modelling and MAS verification, providing active defense orchestration with formal guarantees. Our contributions are (i) a general methodology for controlling active cyber defenses with formally verified specifications based on the attack-defense movement model (ADM), a new model of attacker and defender actions, (ii) an application of this methodology for adaptive honeypot control, which relies on a MAS logic contribution to express strategic properties such as attacker attribution, and (iii) VeriPot, a tool which implements the honeypot adaptation strategy extraction from the ADM.