Multi domain

Thanks to DSL technologies, the approach can be applied to several domain with little effort. The current environment is provided with the following domain as examples:

• Building: physical security
• Netspec: network security

The Building domain supports zones, different types of accesses (door with keys, door with badges, windows), alarms, pickable items.

The Netspec domain supports hosts connected by links, password protected files, sessions requiring a login, protections such as firewalls, antivirus or IDS, and attacker's skills separated in four categories (hacking, decrypting, virus utilisation and login enforcing), and measured by a level (from 0 to 3).

TODO Illustrate and write Read more. Read More ›

Textual and graphical syntaxes

Thanks to DSL technologies, the user can use either textual or graphical editor depending on his preferences.

The textual editor comes with syntax checking, autocompletion, refactoring function such as easily renaming variables.

The graphical editor allows for easier visualization, and correction of the model. Some edition functionalities are not yet implemented rely mostly on the textual syntax for experimentation.

The two editors, textual and graphical, are connected so that a modification in one editor updates the other.

TODO write Read more. Read More ›

Verification

The user is free to use his own process to draw the trees. In that case, ATSyRA provides verifications tools in order to gain confidence in the modeled trees.

We provide a DSL for goals and attack trees, and a graphical editor for attack trees.

A goal is a pair of the form (pre,post), where pre is an initial condition, and post an final condition, and (pre,post) correspond to the goal of reaching as state of "post" from a state of "pre".

An attack tree is either a leaf node of a node than combine smaller attack trees with an operator OR, AND or SAND. Additionaly, each node of an attack tree is labeled by a goal.

Given a goal, ATSyRA can query its reachability in a system, and produce witnesses.

Given an attack tree ATSyRA can query its correctness properties, i.e. answering how the goal label of a non-leaf node compare to the combinaison of the goal label of its children by the operator of the node.

The system with respect to which the verification are performed is given by the naming convention that its file name (before its extension) is the same as the name of the .atg file.

TODO Illustrate and write Read more. Read More ›

Synthesis

For some of the repetitives tasks, ATSyRA can synthetize trees. It can also suggest some optimisation or factorisation.

Before synthesizong trees, ATSyRA can synthesize attack scenarios, which are sequences of actions.

The tree synthesis part of ATSyRA is not available yet.

Based on state-of-the-art model checkers

As the verification and synthesis task are time consuming, ATSyRA is based on state of the art model checker tool.

We use the ITStool model-checker for reachability analysis and verification of the correctness properties. We use the model-checker as a blackbox, by translating our input model into Guarded Action Language (GAL), and running the analysis on the generated GAL model. Symbolic model checking allows a compact encoding of the statespace, which helps tackling the statespace explosion problem. ITStool has been shown in Model-Checking competition to be able to handle big statespaces, with up to 10^12 states

TODO Illustrate and write Read more. Read More ›