Supervised Attack Trees
摘要
Attack trees (ATs) are a popular method for modeling security threats, but they typically assume a “perfect knowledge” where all actions and the state of the systems are fully known. This is unrealistic in practice, where attackers and defenders operate with limited visibility and finite resources. We introduce Supervised Attack Trees (SATs), a framework that extends ATs to model the strategic interaction between an attacker and a defender under partial observability and simultaneous budget constraints. In an SAT, each player sees only a subset of the system’s nodes. The defender (supervisor) can dynamically allocate a limited budget to postpone attacks, while the attacker spends a budget to compromise nodes. We formalize the concept of consistent observation, a snapshot of the partially visible state of the system, and provide an algorithm to verify its validity. Finally, we show how key questions like “given SATs, a defender budget, and an attacker budget, is there a strategy for the supervisor based solely on observations that guarantees the root will never be compromised, no matter how the attacker spends?” or “What is the minimum budget needed to guarantee an attack?” can be reduced to model-checking problems.