Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Automated generation of attack trees with optimal shape and labelling

Olga Gadyatskaya, Sjouke Mauw, Rolando Trujillo-Rasuac, Tim A. C. Willemse

TL;DR

The paper tackles the problem of automatically generating attack trees that are sound with respect to a system specification while remaining concise and readable for analysts. It introduces a formal framework that couples a system model with SP-semantics for attack trees, and a factorisation-based optimisation to minimise tree size and labelling length. A Mixed Kripke Structure is proposed as the system model, together with a correctness criterion ensuring that all attacks in a tree satisfy the root goal. The work highlights a novel connection between attack-tree minimisation and algebraic factorisation in idempotent semirings, provides a running network-security example, and discusses future directions including model-checker integration and extending the framework to defense trees.

Abstract

This article addresses the problem of automatically generating attack trees that soundly and clearly describe the ways the system can be attacked. Soundness means that the attacks displayed by the attack tree are indeed attacks in the system; clarity means that the tree is efficient in communicating the attack scenario. To pursue clarity, we introduce an attack-tree generation algorithm that minimises the tree size and the information length of its labels without sacrificing correctness. We achieve this by i) introducing a system model that allows to reason about attacks and goals in an efficient manner, and ii) by establishing a connection between the problem of factorising algebraic expressions and the problem of minimising the tree size. To the best of our knowledge, we introduce the first attack-tree generation framework that optimises the labelling and shape of the generated trees, while guaranteeing their soundness with respect to a system specification.

Automated generation of attack trees with optimal shape and labelling

TL;DR

The paper tackles the problem of automatically generating attack trees that are sound with respect to a system specification while remaining concise and readable for analysts. It introduces a formal framework that couples a system model with SP-semantics for attack trees, and a factorisation-based optimisation to minimise tree size and labelling length. A Mixed Kripke Structure is proposed as the system model, together with a correctness criterion ensuring that all attacks in a tree satisfy the root goal. The work highlights a novel connection between attack-tree minimisation and algebraic factorisation in idempotent semirings, provides a running network-security example, and discusses future directions including model-checker integration and extending the framework to defense trees.

Abstract

This article addresses the problem of automatically generating attack trees that soundly and clearly describe the ways the system can be attacked. Soundness means that the attacks displayed by the attack tree are indeed attacks in the system; clarity means that the tree is efficient in communicating the attack scenario. To pursue clarity, we introduce an attack-tree generation algorithm that minimises the tree size and the information length of its labels without sacrificing correctness. We achieve this by i) introducing a system model that allows to reason about attacks and goals in an efficient manner, and ii) by establishing a connection between the problem of factorising algebraic expressions and the problem of minimising the tree size. To the best of our knowledge, we introduce the first attack-tree generation framework that optimises the labelling and shape of the generated trees, while guaranteeing their soundness with respect to a system specification.
Paper Structure (23 sections, 9 theorems, 14 equations, 5 figures, 5 algorithms)

This paper contains 23 sections, 9 theorems, 14 equations, 5 figures, 5 algorithms.

Table of Contents

  1. Introduction
  2. Related work
  3. The attack-tree generation problem with optimal labelling and shape
  4. $\mathtt{SAND}$ attack trees
  5. Syntax.
  6. The SP semantics
  7. The underlying graph structure of attack trees
  8. The meaning of attacks and goals
  9. The labelling of attack trees
  10. Problem statement
  11. A heuristic based on factoring to minimise the attack tree size
  12. Attack trees in the factored form
  13. Factorising homogeneous sets of SP graphs via algebraic factorisation
  14. A factorisation heuristic for expressions in idempotent semirings
  15. A factorisation heuristic for sets of homogeneous SP graphs
  16. ...and 8 more sections

Key Result

Proposition 4.1

A set of SP graphs $\mathcal{G}$ is irreducible if it contains a simple graphRecall that a simple SP graph is an SP graph of the form $\xrightarrow{b}.$ or two graphs $g, g' \in \mathcal{G}$ such that $g$ can be written as $g_1 \parallel \ldots \parallel g_n$ with $n > 1$ and $g'$ can be written a

Figures (5)

  • Figure 1: An attack tree example.
  • Figure 2: Our attack tree generation approach, where goals, attacks, and their relation are passed on to the generation algorithm.
  • Figure 3: Another way to represent the attack scenario depicted in Figure \ref{['fig:example']}.
  • Figure 4: An attack without the attack that uses an exploit.
  • Figure 5: A graphical representation of the tree generated by our approach on input the three SP graphs produced from our network example.

Theorems & Definitions (29)

  • Example 3.1
  • Definition 3.1: Series-Parallel graphs
  • Definition 3.2: The SP semantics
  • Example 3.2
  • Definition 3.3: Correctly-labelled tree
  • Definition 3.4: Optimally-labelled tree
  • Definition 3.5: The attack-tree generation problem with optimal labelling and shape
  • Definition 4.1: Reducibility and the factored form for attack trees
  • Proposition 4.1
  • proof
  • ...and 19 more