Active Cyber Defence Strategy through Multi-Agent System Verification

Many computer and industrial systems are designed at a given point in time using the tools and knowledge available at that time, but evolve little afterwards. This static nature benefits cyberattackers, whose techniques advance frequently and who can observe the system over long periods and plan targeted attacks. Active cyber defence mechanisms reduce this vulnerability through system reconfiguration and deception, but finding effective active cyber defence strategies poses a major challenge. This talk presents recent advances in modelling systems where active cyber defences interact with attackers of diverse profiles. It describes a framework to formalise active cyber defence objectives and extract defence strategies with robust guarantees. This framework relies on a logical formalism, Capacity Alternating-time Temporal Logic (CapATL), that enables the expression and verification of strategic, temporal, and capacity (i.e. agent profile) objectives. Thus, CapATL allows the characterisation of desired behaviours for active cyber defences. This talk shows how these formalisms can model a non-trivial adaptive honeypot and derive a strategy suited to the objectives of realism, security, resource management, and attacker profiling.