权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Verifiably Correct Swarm Attestation

可验证正确的群体证明

基本信息

批准号：
EP/V038915/1
负责人：
Brijesh Dongol
金额：
$ 65.51万
依托单位：
University of Surrey
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2021
资助国家：
英国
起止时间：
2021 至无数据
项目状态：
未结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FV038915%2F1
关键词：
Verifiably Correct Swarm Attestation

项目摘要

Attacks such as Stuxnet have shown that malware can cause widespread damage in critical devices, industrial control systems and national infrastructure. The 2019 global cost of cyber-crime is estimated to be over $500 billion; 30% of these are estimated to be malware-based attacks. As digital devices become more complex, connected and commonplace, the frequency and ferocity of such attacks is only likely to increase. What can be done to protect from such attacks? One solution is the use of attestation services, which provides a mechanism for establishing a trust relationship between a verifier and prover. Attestation is used in a wide range of commercial deployments (e.g., Android Key Attestation, Azure Cloud Attestation, Samsung Knox, Windows Server etc), where devices are required to authenticate their identity, ensure the integrity and trust of the system software, and certify that they are running a trusted code base. There are many forms of attestation providing services ranging from static (e.g., boot time) to dynamic (e.g., run-time) guarantees. We are interested in remote attestation, where a verifier checks the internal state of a prover on a different machine across a network. Remote attestation has many applications in future systems involving SMART, internet of things (IoT) and other embedded devices, however, also suffers from scalability issues. Therefore, researchers have developed swarm attestation services that are designed attest a large number of medium/low-end devices. Here, protocol designers must address issues such as device heterogeneity, allowing seamless integration and security across different types of hardware (e.g., smart sensors, car navigation systems, routers, etc). Given a particular implementation of a protocol, how can one ensure that the system is correct, i.e., works as intended by the protocol designer? Our work will consider formal verification of the attestation protocols, which allows one to prove correctness using formal logic and mathematically rigorous arguments. Formal verification will be applied to top-level swarm attestation protocols, and we use a correct-by-construction methodology to develop executable implementations. Then simulation will be used to show applicability of the swarm attestation protocols across real-world applications; our case studies include a vehicular simulation involving intelligent transport systems and a industrial control system developed in collaboration with our project partners.

Stuxnet等攻击表明，恶意软件可能对关键设备、工业控制系统和国家基础设施造成广泛破坏。据估计，2019年全球网络犯罪的成本超过5000亿美元;其中30%估计是基于恶意软件的攻击。随着数字设备变得更加复杂、连接和普遍，此类攻击的频率和猛烈程度只会增加。我们可以做些什么来保护这些攻击？一种解决方案是使用证明服务，它提供了一种在验证者和证明者之间建立信任关系的机制。证明用于广泛的商业部署（例如，Android密钥认证、Azure云认证、Samsung Knox、Windows Server等），其中设备需要验证其身份，确保系统软件的完整性和可信度，并证明它们正在运行可信的代码库。有许多形式的证明提供服务，范围从静态（例如，靴子时间）到动态（例如，运行时）保证。我们感兴趣的是远程证明，其中验证器检查网络上不同机器上的证明器的内部状态。远程证明在涉及智能、物联网（IoT）和其他嵌入式设备的未来系统中有许多应用，然而，也存在可扩展性问题。因此，研究人员已经开发了群认证服务，旨在证明大量的中/低端设备。在这里，协议设计者必须解决诸如设备异构性之类的问题，允许跨不同类型的硬件（例如，智能传感器、汽车导航系统、路由器等）。给定协议的特定实现，如何确保系统是正确的，即，按照协议设计者的预期工作？我们的工作将考虑证明协议的形式验证，它允许使用形式逻辑和数学上严格的参数来证明正确性。形式化验证将应用于顶级的群体认证协议，我们使用正确的建设方法来开发可执行的实现。然后，模拟将被用来显示群体认证协议在现实世界中的应用的适用性;我们的案例研究包括涉及智能交通系统的车辆模拟和与我们的项目合作伙伴合作开发的工业控制系统。