安全问题的实用形式化方法综述
A Survey of Practical Formal Methods for Security
摘要：
在当今世界，关键基础设施通常由计算系统控制。这为网络攻击带来了新的风险，可能会危及这些系统的安全性并破坏其功能。因此，有必要建立这样的系统，以强有力的保证抵御网络攻击。实现这种保证级别的一种方法是使用形式化验证，它提供系统符合所需网络安全属性的证据。本文综述了形式化方法在网络安全和安全关键系统中的应用。我们将FM分为三类：定理证明、模型检验和轻量级FM。为了比较FM的不同用法，我们定义了一组通用术语。我们进一步开发类别的基础上的类型的计算系统FM应用。每一类和类别的解决方案，提出，讨论，比较和总结。我们描述了历史的亮点和发展，并提出了一个国家的最先进的审查，在该地区的调频网络安全。这篇评论是从FM从业者和研究人员的角度提出的，评论了每个类别和类别的趋势。这是通过考虑所有类型的FM，几种类型的安全和安全关键系统，并相应地构建分类来实现的。因此，本文为安全关键系统的系统设计人员提供了FM和可用技术的全面概述，简化了为任务选择正确工具的过程。文章最后总结了审查的讨论，重点是最佳实践，挑战，一般的未来趋势和研究方向在这一领域。
英文摘要：
In today's world, critical infrastructure is often controlled by computing systems. This introduces new risks for cyber attacks, which can compromise the security and disrupt the functionality of these systems. It is therefore necessary to build such systems with strong guarantees of resiliency against cyber attacks. One way to achieve this level of assurance is using formal verification, which provides proofs of system compliance with desired cyber security properties. The use of Formal Methods (FM) in aspects of cyber security and safety-critical systems are reviewed in this article. We split FM into the three main classes: theorem proving, model checking and lightweight FM. To allow the different uses of FM to be compared, we define a common set of terms. We further develop categories based on the type of computing system FM are applied in. Solutions in each class and category are presented, discussed, compared and summarised. We describe historical highlights and developments and present a state-of-the-art review in the area of FM in cyber security. This review is presented from the point of view of FM practitioners and researchers, commenting on the trends in each of the classes and categories. This is achieved by considering all types of FM, several types of security and safety critical systems and by structuring the taxonomy accordingly. The article hence provides a comprehensive overview of FM and techniques available to system designers of security-critical systems, simplifying the process of choosing the right tool for the task. The article concludes by summarising the discussion of the review, focusing on best practices, challenges, general future trends and directions of research within this field.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
