Mohsen LesaniAssociate ProfessorComputer Science & Engineering lesani@ucr.edu(951) 827-5639
CRII: SHF: Certified Byzantine Fault-tolerant Systems
|
AWARD NUMBER
008815-002
FUND NUMBER
33325
STATUS
Active
AWARD TYPE
3-Grant
|
AWARD EXECUTION DATE
2/9/2017
BEGIN DATE
2/15/2017
END DATE
1/31/2019
AWARD AMOUNT
$174,999
|
Sponsor Information
SPONSOR AWARD NUMBER
SPONSOR
SPONSOR TYPE
FUNCTION
Organized Research
PROGRAM NAME
Proposal Information
PROPOSAL NUMBER
17060792
PROPOSAL TYPE
New
ACTIVITY TYPE
Basic Research
PI Information
PI
Lesani, Mohsen
PI TITLE
Other
PI DEPTARTMENT
Computer Science & Engineering
PI COLLEGE/SCHOOL
Bourns College of Engineering
CO PIs
Project Information
ABSTRACT
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.(Abstract from NSF)
|