  We propose a framework for cyber risk assessment and mitigation which models
attackers as formal planners and defenders as interdicting such plans. We
illustrate the value of plan interdiction problems by first modeling network
cyber risk through the use of formal planning, and subsequently formalizing an
important question of prioritizing vulnerabilities for patching in the plan
interdiction framework. In particular, we show that selectively patching
relatively few vulnerabilities allows a network administrator to significantly
reduce exposure to cyber risk. More broadly, we have developed a number of
scalable approaches for plan interdiction problems, making especially
significant advances when attack plans involve uncertainty about system
dynamics. However, important open problems remain, including how to effectively
capture information asymmetry between the attacker and defender, how to best
model dynamics in the attacker-defender interaction, and how to develop
scalable algorithms for solving associated plan interdiction games.
