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.