Design and Verification of Time-Critical Byzantine Fault-Tolerant Systems

时间关键拜占庭容错系统的设计和验证

基本信息

  • 批准号:
    EP/W034514/1
  • 负责人:
  • 金额:
    $ 50.53万
  • 依托单位:
  • 依托单位国家:
    英国
  • 项目类别:
    Research Grant
  • 财政年份:
    2023
  • 资助国家:
    英国
  • 起止时间:
    2023 至 无数据
  • 项目状态:
    未结题

项目摘要

Our society strongly depends on critical information infrastructures such as electrical grids, autonomous vehicles, blockchain applications, IoT critical infrastructures, etc. Not only do we increasingly rely on such complex infrastructures for the correct functioning of our society, in many occasions, even our lives depend on them being safe and secure.Critical infrastructures are the target of attacks aiming at stealing critical assets such as money and data. Vulnerabilities in software components used by these infrastructures are regularly found and exploited, sometimes allowing attackers to control physical components of SCADA (Supervisory Control And Data Acquisition) systems such as the New York Dam or Ukraine's Power Grid. As we keep seeing in the news, failures of such systems can be catastrophic.The decentralized nature of some of these infrastructures require complex mechanisms to guarantee that the data they handle is safe and secure. For example, blockchain systems allow remote users to agree on and maintain a digital ledger of transactions. They rely on complex agreement algorithms to provide those guarantees and ensure the correct functioning of the systems while users interact remotely and propose transactions concurrently. Such systems can even work correctly when some users are faulty (possibly acting maliciously). As for SCADA systems, bugs are regularly found and exploited to steal critical assets in such systems.Among the agreement algorithms used in blockchain technology, traditional Byzantine Fault Tolerant (BFT) protocols require little computing power, and can be used to harden any (deterministic) service (e.g., a banking service). They achieve this by replicating the service across a number of machines such that the correctly functioning machines hide the behavior of the faulty ones. However, one drawback of such protocols is that they require two thirds of the users to be honest, and a large number of messages to be exchanged before transactions are accepted.While BFT techniques have primarily been used in blockchain systems, other infrastructures could benefit from it if it was delivering the required properties. For example, in order to use BFT protocols in SCADA systems, they would have to guarantee that operations that need to be agreed upon between multiple remote components, can be achieved in a timely manner.These issues call for (1) developing generic, yet efficient defence mechanisms that can be applied to a wide range of infrastructures, and(2) provide strong correctness guarantees.First, in this project we propose to develop efficient BFT protocols that can be applied to a wide range of infrastructures. More precisely, we propose to develop novel BFT techniques that are less costly (less replicas and less exchanged messages) than state-of-the-art solutions by relying on trusted components (e.g., secure hardware components such as Intel SGX), and to apply these techniques to develop more efficient and reliable blockchain systems. Moreover, we also propose to develop techniques to turn state-of-the-art BFT protocols into protocols that achieve timeliness guarantees, allowing their integration in real-time applications.Secondly, we propose to guarantee the correctness of these novel protocols. One way to provide strong correctness guarantees is to useformal verification methods, such as theorem provers to automatically or interactively prove that a piece of software or hardware behaves asintended. Many theorem provers have been developed and improved over the years allowing to do just that, such as Agda, Coq, Isabelle, etc.Our project will make use of the highly expressive Coq prover to ensure the correctness of these protocols. More precisely, we propose to develop within Coq, support to implement BFT protocols, models to capture the environments in which those protocols execute, as well asproof techniques to guarantee their correctness.
我们的社会强烈依赖于关键的信息基础设施,如电网,自动驾驶汽车,区块链应用,物联网关键基础设施等,我们不仅越来越依赖这些复杂的基础设施来确保我们社会的正常运作,而且在许多情况下,甚至我们的生命也依赖于它们的安全和保障。关键基础设施是攻击的目标,攻击的目的是窃取关键资产,如金钱和数据这些基础设施使用的软件组件中的漏洞经常被发现和利用,有时允许攻击者控制SCADA(监督控制和数据采集)系统的物理组件,例如纽约大坝或乌克兰电网。正如我们在新闻中不断看到的那样,此类系统的故障可能是灾难性的。其中一些基础设施的分散性需要复杂的机制来保证它们处理的数据是安全的。例如,区块链系统允许远程用户同意并维护交易的数字分类账。它们依靠复杂的协议算法来提供这些保证,并确保系统的正确运作,同时用户进行远程交互并同时提出交易。这样的系统甚至可以在某些用户出错(可能是恶意行为)时正常工作。至于SCADA系统,经常发现并利用漏洞窃取此类系统中的关键资产。在区块链技术中使用的协议算法中,传统的拜占庭容错(BFT)协议需要很少的计算能力,并且可以用于加固任何(确定性)服务(例如,银行服务)。他们通过在多台机器上复制服务来实现这一点,以便正确运行的机器隐藏故障机器的行为。然而,这种协议的一个缺点是,它们需要三分之二的用户是诚实的,并且在交易被接受之前需要交换大量的消息。虽然BFT技术主要用于区块链系统,但如果它提供所需的属性,其他基础设施可以从中受益。例如,为了在SCADA系统中使用BFT协议,他们必须保证需要在多个远程组件之间达成一致的操作可以及时实现。这些问题要求(1)开发通用的,但有效的防御机制,可以应用于广泛的基础设施,以及(2)提供强大的正确性保证。首先,在这个项目中,我们建议开发有效的BFT协议,可以应用于广泛的基础设施。更确切地说,我们提出开发新的BFT技术,其通过依赖于可信组件(例如,安全的硬件组件,例如英特尔SGX),并应用这些技术来开发更高效、更可靠的区块链系统。此外,我们还建议开发技术,把国家的最先进的BFT协议的协议,实现及时性保证,允许他们在实时应用程序的集成。其次,我们建议保证这些新的协议的正确性。提供强正确性保证的一种方法是使用形式验证方法,例如定理证明器自动或交互地证明软件或硬件的行为符合预期。多年来,许多定理证明器已经开发和改进,允许这样做,如Agda,Coq,Isabelle等。我们的项目将利用高度表达的Coq证明器来确保这些协议的正确性。更确切地说,我们建议在Coq中开发,支持实现BFT协议,捕获这些协议执行的环境的模型,以及保证其正确性的证明技术。

项目成果

期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ monograph.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ patent.updateTime }}

Vincent Rahli其他文献

Meeting the Challenges of Critical and Extreme Dependability and Security
应对关键和极端可靠性和安全性的挑战
Electronic Communications of the EASST Volume 72 ( 2015 ) Proceedings of the 15 th International Workshop on Automated Verification of Critical Systems ( AVoCS 2015 ) Formal Specification , Verification , and Implementation of Fault-Tolerant Systems using EventML
EASST 电子通信第 72 卷 (2015) 第 15 届关键系统自动验证国际研讨会 (AVoCS 2015) 使用 EventML 的容错系统的正式规范、验证和实现
  • DOI:
  • 发表时间:
    2015
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Vincent Rahli;D. Guaspari;M. Bickford;R. Constable
  • 通讯作者:
    R. Constable
EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems
EventML:容错状态机复制系统的规范、验证和实现
  • DOI:
    10.1016/j.scico.2017.05.009
  • 发表时间:
    2017
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Vincent Rahli;D. Guaspari;M. Bickford;R. Constable
  • 通讯作者:
    R. Constable
Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
通过模态选择构建无偏见的外延类型理论
Realizing Continuity Using Stateful Computations
使用状态计算实现连续性
  • DOI:
    10.4230/lipics.csl.2023.15
  • 发表时间:
    2023
  • 期刊:
  • 影响因子:
    0
  • 作者:
    L. Cohen;Vincent Rahli
  • 通讯作者:
    Vincent Rahli

Vincent Rahli的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

相似海外基金

POSE: Phase II: Open-Source Precision, High Accuracy and Security Environment (OpenPHASE) For Time Verification, Calibration, and Interoperability
POSE:第二阶段:用于时间验证、校准和互操作性的开源精密、高精度和安全环境 (OpenPHASE)
  • 批准号:
    2303726
  • 财政年份:
    2023
  • 资助金额:
    $ 50.53万
  • 项目类别:
    Standard Grant
Real-time Volumetric Imaging for Motion Management and Dose Delivery Verification
用于运动管理和剂量输送验证的实时体积成像
  • 批准号:
    10659842
  • 财政年份:
    2023
  • 资助金额:
    $ 50.53万
  • 项目类别:
Collaborative Research: SHF: Medium: Integrated Verification of IoT and Real-time Communication Protocols
合作研究:SHF:中:物联网和实时通信协议的集成验证
  • 批准号:
    2211996
  • 财政年份:
    2022
  • 资助金额:
    $ 50.53万
  • 项目类别:
    Standard Grant
Collaborative Research: SHF: Medium: Integrated Verification of IoT and Real-time Communication Protocols
合作研究:SHF:中:物联网和实时通信协议的集成验证
  • 批准号:
    2211997
  • 财政年份:
    2022
  • 资助金额:
    $ 50.53万
  • 项目类别:
    Standard Grant
Real-time in vivo proton range verification in proton therapy with thallium bromide detectors
使用溴化铊探测器进行质子治疗中的实时体内质子范围验证
  • 批准号:
    10390443
  • 财政年份:
    2021
  • 资助金额:
    $ 50.53万
  • 项目类别:
Verification study and therapeutical utilization for implementation of real time monitoring in oral cancer
口腔癌实时监测的验证研究和治疗应用
  • 批准号:
    21H03143
  • 财政年份:
    2021
  • 资助金额:
    $ 50.53万
  • 项目类别:
    Grant-in-Aid for Scientific Research (B)
Real-time in vivo proton range verification in proton therapy with thallium bromide detectors
使用溴化铊探测器进行质子治疗中的实时体内质子范围验证
  • 批准号:
    10559516
  • 财政年份:
    2021
  • 资助金额:
    $ 50.53万
  • 项目类别:
Mathematical and experimental verification of time operators
时间算子的数学和实验验证
  • 批准号:
    20K20886
  • 财政年份:
    2020
  • 资助金额:
    $ 50.53万
  • 项目类别:
    Grant-in-Aid for Challenging Research (Exploratory)
MRI: CNS: Acquisition of Real-Time Hardware-in-the-Loop Simulation for Verification of Connected and Autonomous Vehicles
MRI:CNS:获取实时硬件在环仿真以验证联网和自动驾驶车辆
  • 批准号:
    1919855
  • 财政年份:
    2019
  • 资助金额:
    $ 50.53万
  • 项目类别:
    Standard Grant
ML2C - Machine Learning for robust, real-time dosimetry and MultiLeaf Collimator verification
ML2C - 用于稳健、实时剂量测定和 MultiLeaf Collimator 验证的机器学习
  • 批准号:
    ST/T002646/1
  • 财政年份:
    2019
  • 资助金额:
    $ 50.53万
  • 项目类别:
    Research Grant
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了