CRII: SHF: Certified Byzantine Fault-tolerant Systems

CRII：SHF：经过认证的拜占庭容错系统

• 批准号: 1657204
• 负责人: Mohsen Lesani
• 金额: $ 17.5万
• 依托单位: University of California-Riverside
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-02-15 至 2023-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1657204&HistoricalAwards=false
• 关键词: CRII; SHF; Certified; Byzantine; Fault

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.

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

项目成果

TLC: temporal logic of distributed components

TLC：分布式组件的时序逻辑

• DOI: 10.1145/3409005
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Griffin, Jeremiah;Lesani, Mohsen;Shadab, Narges;Yin, Xizhe
• 通讯作者: Yin, Xizhe

Hampa: Solver-Aided Recency-Aware Replication

• DOI: 10.1007/978-3-030-53288-8_16
• 发表时间: 2020-06-13
• 期刊: Computer Aided Verification
• 作者: Li X;Houshmand F;Lesani M
• 通讯作者: Lesani M

Learning quantitative representation synthesis

学习定量表示综合

• DOI: 10.1145/3394450.3397467
• 发表时间: 2020
• 期刊: Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages
• 作者: Patil, Mayur;Houshmand, Farzin;Lesani, Mohsen
• 通讯作者: Lesani, Mohsen

Hamsaz: Replication Coordination Analysis and Synthesis

• DOI: 10.1145/3290387
• 发表时间: 2019-01-01
• 期刊: PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL
• 影响因子: 1.8
• 作者: Houshmand, Farzin;Lesani, Mohsen
• 通讯作者: Lesani, Mohsen