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

排名风险和制定对策是量化安全分析的首要目标之一。攻击-防御树是用于此任务的流行框架之一，也在工业实践中使用。攻击-防御树的标准量化分析可以区分可能和不可能的漏洞。我们提供了一种工具，可以轻松合成和分析这些模型，还包括概率、成本和时间。此外，它提供了多种接口到现有的模型检查器和分析工具。不幸的是，目前可用的工具依赖于精确的定量输入（攻击的概率、时间或成本），这些输入很少可用。相反，通常只有统计的、不精确的信息可用，使我们只能得到实际数量的大致正确（PAC）估计。作为我们工具的一部分，我们扩展了标准分析技术，使它们能够处理PAC输入，并对分析结果的不精确性和不确定性产生严格的界限。

攻击防御树的概率分析工具通常需要精确的量化输入，但实际上只有统计模糊信息。本论文旨在扩展标准分析技术，以处理可能大致正确的输入，并对分析结果的不确定性进行严格的边界估计。

本论文提出了一种攻击防御树的概率分析工具，可以处理模糊的统计信息，并扩展了标准分析技术以处理可能大致正确的输入，并对分析结果的不确定性进行严格的边界估计。

本工具提供了多种接口，可与现有的模型检查器和分析工具配合使用。实验结果表明，该工具可以在处理模糊的统计信息时提供准确的结果。

相关研究包括攻击防御树的其他概率分析工具，如PRISM-ADT和CPAchecker-ADT。