CRII: SHF: Certified Byzantine Fault-tolerant Systems

本项目研究了一种新的方法来验证分布式系统的可靠性和安全性，其中错误或恶意节点表现出任意或误导性的行为。分布式系统被广泛应用于从金融到飞机控制等越来越重要的应用中，以获得容错、吞吐量和响应能力。不幸的是，它们是出了名的复杂和容易出错。节点不仅可能崩溃，而且可能被恶意代理程序入侵和控制。所谓的拜占庭节点可以模拟其他节点或发送令人困惑的消息。拜占庭容错系统的形式化安全保证尚未得到具体说明和验证。该项目通过一个新的编程，验证和运行时框架进行研究，从而实现这种保证。该项目的智力优势是在网络语义和分布式系统的表示，组合和证明方法方面取得了根本性的进展。该项目更广泛的意义是一个公开可用的认证分布式系统的开源库，可以导致更快的安全和可信的分布式系统的发展。该项目包括以下关键组件：（1）分布式实现的层的精确表示和组合。基于事件的模型表示并组成分布式实现的层。一个实现的编程和验证模块化对规范的较低级别的实现。(2)拜占庭同步网络的语义和实现规范。该项目提出了一种新的拜占庭同步网络的操作语义是参数的实现。因此，实现的安全性和活性规范可以在实现实例化时被声明为语义的外部痕迹上的条件。(3)拜占庭语义学的证明原则和自动化证明。本研究发展了语义的证明原则，抽象了证明的公共部分，促进了证明的自动化。为了实现证明的自动化，本项目为原则的证明义务寻找决策和半决策程序。(4)构建可访问的拜占庭容错复制对象。该项目建立了一个可执行拜占庭容错复制对象的认证库，并通过一个可访问的接口提供给广泛的研究人员和从业人员。

This project investigates a new approach to verification of reliability and security of distributed systems where faulty or malicious nodes exhibit arbitrary or misleading behavior. Distributed systems are widely used in increasingly important applications ranging from finance to aircraft control to gain fault-tolerance, throughput and responsiveness. Unfortunately, they are notoriously complicated and prone to bugs. Nodes may not only crash but also be hacked and controlled by malicious agents. The so-called Byzantine nodes can impersonate other nodes or send confusing messages. Formal security guarantees of Byzantine fault-tolerant systems have not been specified and verified yet. This project undertakes research leading to such guarantees through a novel programming, verification and runtime framework. The intellectual merits of the project are fundamental advances in the semantics of networks and representation, composition, and proof methodologies for distributed systems. The project's broader significance is a publicly available open-source library of certified distributed systems that can lead to faster evolution of secure and trustworthy distributed systems.This project includes the following key components: (1) Precise representation and composition of layers of distributed implementations. An event-based model represents and composes layers of distributed implementations. An implementation is programmed and verified modularly against the specification of the lower-level implementation. (2) The semantics of the Byzantine synchronous network and the specifications of implementations. This project presents a novel operational semantics for Byzantine synchronous networks that is parametric in terms of the implementation. Hence, the safety and liveness specification of an implementation can be stated as conditions on the external traces of the semantics when instantiated with the implementation. (3) Proof principles for the Byzantine semantics and proof automation. This research develops proof principles for the semantics that abstract the common parts of the proofs and facilitate proof automation. To automate the proofs, this project searches for decision and semi-decision procedures for the proof obligations of the principles. (4) Building of accessible Byzantine fault-tolerant replicated objects. This project builds a certified library of executable Byzantine fault-tolerant replicated objects and makes it available to a wide range of researchers and practitioners through an accessible interface.