Attack-Defence Trees in Maude

An Attack-Defense Tree (ADTree) is a tree-like representation of a security scenario. Nodes in the tree represent attacks and defensive measures [1].

This repository contains a rewriting logic specification for modeling ADTree and solve the optimal scheduling problem. That is, finding the minimal set of agents needed to perform an attack.

Getting Started

The project was tested in Maude 3.2. A script written in Python 3.10 is used to parse input files and call Maude by using the Python bindings for Maude. PrettyTable is also needed to generate the scheduling tables. You can use the script install-deps.sh to install Maude and Python3 dependencies.

Example of use:

./min-schedule.py --input ./examples/forestall.txt

./min-schedule.py --input ./examples/forestall.txt --table

Maude files

The specification includes the following files:

• syntax.maude: We have used the object-like notation in the Maude's module CONFIGURATION. This file defines the identifiers for classes (sort Cid) for the different nodes of the tree with their respective attributes (cost, duration, children, state, etc).

• semantics.maude: This file gives meaning to the different nodes using rewriting rules. In order to compute the minimal time required for an attack, the strategy solve reduces the (unnecessary) non-determinism, thus improving efficiency.

• semantics-schedule: Once the previous theory has been used to determine the minimal time and an upper bound for the number of agents, this theory finds the schedule minimizing the number of agents. For that, an iterative procedure is needed, trying a solution with i in 1..n agents (where n is the upper bound).

Python Files

The extra libraries needed are in requirements.txt. There are two files:

• adt2maude.py: implementing a simple parser from the textual representation of ADTrees to the Maude syntax.

• min-schedule.py: finding the minimal time (theory semantics) and then, iterating and calling the theory semantics-schedule to find the optimal schedule.

Examples

• steal-jewels.maude: This is a simple example that illustrates the syntax used for defining the ADTree and the queries that can be performed.

• forestall.maude (Forestalling a software release): Models an attack to the intellectual property of a company.

• gain-admin.maude: Models the attack for obtaining root privileges on a server.

• iot-dev.maude: Attack to an IoT device (via wireless or LAN).

Further details and motivations for these systems can be found in [2].

This package is free software; you can redistribute it and/or modify it under the terms of GNU Lesser General Public License (see the LICENSE file).

Refences

[1] Barbara Kordy, Sjouke Mauw, Saša Radomirović, Patrick Schweitzer: Attack–defense trees. Journal of Logic and Computation, Volume 24, Issue 1. 2004 186-198

[2] Jaime Arias, Carlos E. Budde, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk, Mariëlle Stoelinga: Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems. ICFEM 2020: 3-19