一句话：提出基于 Quality Calculus 的保护分析，可发现攻击、按代价量化最廉价攻击并生成攻击树。
软件与信息物理系统安全常被视为定性需求，但实际只能定量达成；分布式组件使攻击难以预测，且需向非专家沟通以辅助决策。本文提出面向 Quality Calculus 的保护分析：先计算攻击者到达系统指定位置所需的所有数据集合，再在给定代价概念下找出最廉价攻击集合，并导出攻击树进行图形化展示。该分析先在定性设定下建立，再扩展到定量设定；定量形式被编码为可满足性模理论（SMT）中的优化问题，以处理复杂代价结构。作者用 Java 实现框架，并在国家级认证系统上验证其有效性。
In the design of software and cyber-physical systems, security is often perceived as a qualitative need, but can only be attained quantitatively. Especially when distributed components are involved, it is hard to predict and confront all possible attacks. A main challenge in the development of complex systems is therefore to discover attacks, quantify them to comprehend their likelihood, and communicate them to non-experts for facilitating the decision process. To address this three-sided challenge we propose a protection analysis over the Quality Calculus that (i) computes all the sets of data required by an attacker to reach a given location in a system, (ii) determines the cheapest set of such attacks for a given notion of cost, and (iii) derives an attack tree that displays the attacks graphically. The protection analysis is first developed in a qualitative setting, and then extended to quantitative settings following an approach applicable to a great many contexts. The quantitative formulation is implemented as an optimisation problem encoded into Satisfiability Modulo Theories, allowing us to deal with complex cost structures. The usefulness of the framework is demonstrated on a national-scale authentication system, studied through a Java implementation of the framework.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{VigoNN16,
title = {Discovering, quantifying, and displaying attacks},
author = {Roberto Vigo and Flemming Nielson and Hanne Riis Nielson},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 4},
year = {2017},
doi = {10.2168/lmcs-12(4:5)2016}
}