Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT

Attack-Defense Trees (ADTrees) are widely used in the security analysis of software systems. In this paper, we introduce a novel approach to analyze system architecture models via ADTrees and to synthesize an optimal cost defense solution using MaxSMT. We generate an ADTree from the Architecture Analysis and Design Language (AADL) model with its possible attacks, and implemented defenses. We analyze these ADTrees to see if they satisfy their cyber-requirements. We then translate the ADTree into a set of logical formulas, that encapsulate both the logical structure of the tree, and the constraints on the cost of implementing the corresponding defenses, such that a minimization query to the MaxSMT solver returns a set of defenses that mitigate all possible attacks with minimal cost. We provide an initial evaluation of our tool on a delivery drone system model which shows promising results.