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.