HOME: Heard-Of based Formal Modeling and Verification Environment for Consensus Protocols

Consensus protocol plays an important role in en-suring the reliability of distributed systems. How to formally model and verify it is a hot research issue. Due to the limitation of verification performance, it can usually verify consensus algorithms with a small number of processes. The Heard-Of (HO) model is well-performing in formal verification. However, existing works only support HO modeling for Crash Fault Tolerant (CFT) protocols and rely on SMT-based verification. It cannot model Byzantine Fault Tolerant (BFT) protocols, nor can it support SAT solving. This paper designs and implements an HO-based formal modeling and verification environment (HOME) for consensus protocols. We developed a modeling tool to support the HOML (HO modeling language) for formally modeling the threshold-guarded distributed BFT protocols. We get through the formal verification process from HOML to SAT/SMT solving to improve the verification performance. HOME integrates HOML's translator and SAT/SMT solvers, which can facilitate the design of consensus protocols and help discover safety issues. The evaluation results show that HOME supports the modeling and verification of various consensus protocols, and SAT solving can effectively improve the verification performance. Repo: https://github.com/tempAcc000/HOME Video: https://www.youtube.com/watchvZiaVLs-VGwE