Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

QuADTool: Attack-Defense-Tree Synthesis, Analysis and Bridge to Verification

Florian Dorfhuber, Julia Eisentraut, Katharina Klioba, Jan Kretinsky

TL;DR

QuADTool tackles risk ranking under imprecise quantitative inputs in attack-defense trees by providing $({\epsilon},{\delta})$-PAC-aware bottom-up analyses that bound the final results. It offers a complete workflow with a GUI and CLI, supports imports/exports to DOT/XML, and exports to UPPAAL, PRISM, MODEST, and PRISM-games for verification, along with an automated feedback system to check modeling assumptions. The work's main contribution is extending ADT analysis to PAC inputs, enabling explicit bounds on input and output uncertainty with minimal additional computation. An ATBEST benchmark suite plus extensive experiments demonstrate scalability and practical usefulness in risk assessment and verification contexts.

Abstract

Ranking risks and countermeasures is one of the foremost goals of quantitative security analysis. One of the popular frameworks, used also in industrial practice, for this task are attack-defense trees. Standard quantitative analyses available for attack-defense trees can distinguish likely from unlikely vulnerabilities. We provide a tool that allows for easy synthesis and analysis of those models, also featuring probabilities, costs and time. Furthermore, it provides a variety of interfaces to existing model checkers and analysis tools. Unfortunately, currently available tools rely on precise quantitative inputs (probabilities, timing, or costs of attacks), which are rarely available. Instead, only statistical, imprecise information is typically available, leaving us with probably approximately correct (PAC) estimates of the real quantities. As a part of our tool, we extend the standard analysis techniques so they can handle the PAC input and yield rigorous bounds on the imprecision and uncertainty of the final result of the analysis.

QuADTool: Attack-Defense-Tree Synthesis, Analysis and Bridge to Verification

TL;DR

QuADTool tackles risk ranking under imprecise quantitative inputs in attack-defense trees by providing -PAC-aware bottom-up analyses that bound the final results. It offers a complete workflow with a GUI and CLI, supports imports/exports to DOT/XML, and exports to UPPAAL, PRISM, MODEST, and PRISM-games for verification, along with an automated feedback system to check modeling assumptions. The work's main contribution is extending ADT analysis to PAC inputs, enabling explicit bounds on input and output uncertainty with minimal additional computation. An ATBEST benchmark suite plus extensive experiments demonstrate scalability and practical usefulness in risk assessment and verification contexts.

Abstract

Ranking risks and countermeasures is one of the foremost goals of quantitative security analysis. One of the popular frameworks, used also in industrial practice, for this task are attack-defense trees. Standard quantitative analyses available for attack-defense trees can distinguish likely from unlikely vulnerabilities. We provide a tool that allows for easy synthesis and analysis of those models, also featuring probabilities, costs and time. Furthermore, it provides a variety of interfaces to existing model checkers and analysis tools. Unfortunately, currently available tools rely on precise quantitative inputs (probabilities, timing, or costs of attacks), which are rarely available. Instead, only statistical, imprecise information is typically available, leaving us with probably approximately correct (PAC) estimates of the real quantities. As a part of our tool, we extend the standard analysis techniques so they can handle the PAC input and yield rigorous bounds on the imprecision and uncertainty of the final result of the analysis.
Paper Structure (2 sections, 1 figure)

This paper contains 2 sections, 1 figure.

Table of Contents

  1. Introduction
  2. Attack-Defense Trees

Figures (1)

  • Figure 1: The $\mathsf{ADT}_{}^{}{}$ from fila2019 represents ways to gain access to a power meter. We will use this model also in sec:pacanalysis. In sec:experiments we evaluate our tool on more complex attack-defense trees.

Theorems & Definitions (1)

  • definition thmcounterdefinition: Attack-Defense Trees hermanns2016