Verification and Synthesis of Assured Dynamic Cyber Defense with Deception and Counter Deception
Abstract
Cyber networks are frequently targeted by resourceful attackers, who identify system vulnerabilities through network reconnaissance and craft customized, multistage attacks. To counter the sophisticated attackers, traditional network security mechanisms (e.g., intrusion detection and firewalls) are often complemented by dynamic defenses including cyber deception and moving target defense (MTD) techniques. Such defenses aim to increase uncertainty and complexity for the attacker by either preventing the attacker from identifying and attacking weak points in the network, increasing the cost of attacks, or distracting the attacker from compromising critical nodes in the network with decoys. However, it is often difficult to assess the effectiveness of such defense mechanisms and to design defense systems with provable performance guarantees. The lack of performance assurance and security guarantees in defense strategies can potentially hinder the use of novel dynamic defense with deception. This project will research and develop formal methods approach and algorithmic game theory for modeling, verifying, and synthesizing provably correct dynamic cyber defense systems with deception and counter-deception. The key goals are: 1) Develop a game-theoretic modeling framework for cyber networks equipped with dynamic defense and deception mechanisms. The modeling framework will enable the development of novel algorithms for verifying and synthesizing proactive defense systems given security specifications in high-level formal logic; 2) Develop game-theoretic synthesis methods for constructing assured active cyber defense strategies with novel deception mechanisms; 3) Develop effective dynamic defense strategies against learning-based attacks in repeated interactions. To achieve these goals, the project will introduce new formal graphical security models to capture uncertainty and unpredictable changes created by shuffling, diversification, and randomization using MTD techniques and decoy-based deception. It will develop a model of hypergames to capture the attackerÕs misperception created by decoy systems and incomplete information about the defender s action capabilities. By investigating the solutions of hypergames and Stackelberg games, it will develop methods for synthesizing autonomous proactive and active dynamic defense strategies with respect to formal security constraints. To achieve effective cyber deception over repeated interactions, it will leverage the unlearnability results from automata learning theory to construct dynamic defense strategies adversarial to learning-based attacks. Based on the insights gained from game-theoretic deception, novel counter-deception methods will be investigated to detect and probe the intention of the deceptive attackers. The immediate impact will be providing tools and algorithms to verify and assess the dynamic defense-with-deception strategies in cyber networks with respect to formal security constraints, and to synthesize autonomous network defense systems with security guarantees. These methods contribute to improving the security in cyber networks and provide assurance for military communication systems. The principled game-theoretic planning with deception will generalize to other military operations where stringent safety and security constraints must be satisfied against adversarial attacks.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jul 14, 2022
- Source ID
- W911NF2210166
Entities
People
- Jie Fu
Organizations
- Army Contracting Command
- United States Army
- University of Florida