Automated Game-Theoretic Verification of Security Systems

安全系统的自动博弈论验证

• 批准号: EP/K038575/1
• 负责人: David Parker
• 金额: $ 12.58万
• 依托单位: University of Birmingham
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2013
• 资助国家: 英国
• 起止时间: 2013 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FK038575%2F1
• 关键词: Automated; Game; Theoretic; Verification; Security

We are surrounded by computerised systems, upon whose secure and reliable operation we are increasingly dependent. Yet flaws in these systems are common, from power plants to travel cards, and these come at high costs for individuals, companies and governments alike. So, rigorous, mathematically-sound techniques to check the security of computerised systems are essential. Security, though, is not absolute: we may only be able to guarantee that an attack on a system is possible with low probability, rather than impossible. Furthermore, system designs often need to trade off the degree of security or privacy offered against other practical concerns such as response time or power consumption. So, effective methods for the analysis of security also need to take these quantitative aspects into account.This project will develop fully-automated techniques to formally verify the correctness of security systems, to identify flaws in their operation, and to fix or optimise aspects of their design. We will do so by bringing together techniques from several different areas: (i) game-theoretic methods, to reason about the interactions between a security system and its potential attackers; and (ii) automated verification and synthesis techniques, with a particular emphasis on quantitative aspects such as probability or resource usage. Building upon recent advances in these fields, and upon existing efforts to create efficient and scalable verification methods, this project will develop novel techniques to verify security systems, implement them in freely-available software tools and apply them to a variety of security applications, from electronic voting schemes to anonymous communication networks.

我们被计算机化系统包围，我们越来越依赖其安全可靠的运行。然而，从发电厂到旅行卡，这些系统的缺陷很常见，而这些缺陷给个人、公司和政府带来了高昂的成本。因此，严格的、数学上合理的技术来检查计算机系统的安全性至关重要。然而，安全性并不是绝对的：我们可能只能保证对系统的攻击是可能的，但概率很低，而不是不可能。此外，系统设计通常需要权衡所提供的安全性或隐私程度与其他实际问题（例如响应时间或功耗）。因此，有效的安全分析方法也需要考虑这些定量方面。该项目将开发全自动技术来正式验证安全系统的正确性，识别其运行中的缺陷，并修复或优化安全系统的各个方面。他们的设计。为此，我们将汇集几个不同领域的技术：（i）博弈论方法，推理安全系统与其潜在攻击者之间的交互； (ii) 自动验证和综合技术，特别强调概率或资源使用等定量方面。基于这些领域的最新进展，以及创建高效且可扩展的验证方法的现有努力，该项目将开发验证安全系统的新技术，在免费提供的软件工具中实施它们，并将它们应用于各种安全应用程序，从匿名通信网络的电子投票方案。

项目成果

Automated Game-Theoretic Verification of Security Systems

安全系统的自动博弈论验证

• 发表时间: 2019
• 作者: Mu C

Quantitative Evaluation of Systems - 16th International Conference, QEST 2019, Glasgow, UK, September 10-12, 2019, Proceedings

系统定量评估 - 第 16 届国际会议，QEST ​​2019，英国格拉斯哥，2019 年 9 月 10-12 日，会议记录

• DOI: 10.1007/978-3-030-30281-8_14
• 发表时间: 2019
• 作者: Mu C

Tools and Algorithms for the Construction and Analysis of Systems

用于系统构建和分析的工具和算法

• DOI: 10.1007/978-3-642-28756-5_47
• 发表时间: 2012
• 作者: Basler G

Verification and control of partially observable probabilistic systems

• DOI: 10.1007/s11241-017-9269-4
• 发表时间: 2017-05-01
• 期刊: REAL-TIME SYSTEMS
• 影响因子: 1.3
• 作者: Norman, Gethin;Parker, David;Zou, Xueyi
• 通讯作者: Zou, Xueyi