New Publication in IEEE Transactions on Reliability
On January 31, an article by Prof. Wojciech Penczek, Łukasz Maśko and Teofil Sidoruk, written in collaboration with Prof. Laure Petrucci, Carlos Olarte, and Jaime Arias from Université Sorbonne Paris Nord, was published in IEEE Transactions on Reliability. The paper "Optimal Scheduling of Agents in ADTrees: Specialized Algorithm and Declarative Models" follows earlier work [1] that proposed representing attack-defence trees (ADTrees) as multi-agent systems. ADTrees are a popular formalism for studying security scenarios where two opposing parties attempt to achieve sub-goals (tree nodes) comprising the overall objective (tree root), or try to prevent the other group from doing so. With the translation to an agent-based formalism, one can additionally consider the attackers and defenders in these scenarios as agent coalitions. As such, not only do they have a particular number of agents, but also specific assignment to sub-goals. This can determine not only the feasibility of an attack or defence, but also its time, cost, or other quantitative metrics of interest.
Thus, minimising the number of agents and optimally scheduling their assignments in attacking and defending coalitions is of interest. The paper proposes and analyses two distinct approaches to solving this problem. First, it puts forward a specialised algorithm running in quadratic time that synthesises an optimal assignment using the minimal number of agents for a given ADTree. Second, it shows how to leverage rewriting logic (RL) to construct a declarative set of rules, called a rewriting theory, that specifies the exact requirements for a valid and optimal assignment for a given ADTree. This declarative approach, while slower than the specialised algorithm, nonetheless enjoys the advantages of being much more general, and thus easily adaptable to other scenarios such as extensions of the ADTree formalism or even other representations.
With the security of computer systems being a major ongoing challenge, the results on one hand allow for better studying relevant attack/defence scenarios on a new level, while on the other they are also important in the context of multi-agent systems and containing the problem of state explosion by reducing the number of required agents. Furthermore, the authors identify several avenues for further research, including using timed temporal-strategic logics such as TATL or the recently proposed STCTL [2] to allow for specifying more elaborate goals. This ties neatly into their ongoing scientific collaboration with Prof. Petrucci's team at Université Sorbonne Paris Nord (co-financed by PAS in IEA projects), which aims, among others, to unify the aspects of strategic ability and time in the context of model checking and satisfiability checking over asychronous multi-agent systems.
The work is an extended version of an ICECCS 2022 conference paper [3], adding a new approach to the problem based on rewriting logic and comparing it against the previously proposed specialised algorithm. Its near-final version can also be accessed at arXiv [4], differing only in a few very minor, editorial revisions.
- J. Arias, C. E. Budde, L. Petrucci, W. Penczek, T. Sidoruk, M. Stoelinga: Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems. Proceedings of the 22nd International Conference on Formal Engineering Methods (ICFEM 2020), Singapore, March 1–3, 2021, pp. 3-19
- J. Arias, W. Jamroga, L. Petrucci, W. Penczek, T. Sidoruk: Strategic (Timed) Computation Tree Logic. Proceedings of the 22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2023), London, United Kingdom, May 29-June 2, 2023, pp. 382-390
- J. Arias, Ł. Maśko, L. Petrucci, W. Penczek, T. Sidoruk: Minimal Schedule with Minimal Number of Agents in Attack-Defence Trees. Proceedings of the 26th International Conference on Engineering of Complex Computer Systems (ICECCS 2022), Hiroshima, Japan, March 26-30, 2022, pages 1-10
- https://arxiv.org/abs/2305.04616