哈希图一致性算法已被验证为异步拜占庭容错

HederaHashgraph在下一代公共分类帐中拥有多样化的治理。它最近宣布哈希图一致性算法已被验证为异步拜占庭容错。这是通过使用Coq系统的计算机检查的数学证明完成的。

分布式系统安全证明

这就是哈希图报告中所提出的主张的证明。有人认为哈希图在数学上是分布式系统的最高安全级别。Leemon Baird博士准备就正式方法举行一次会议。这将在Hedera18举行，它是首届哈希图开发人员会议。还有一个为感兴趣的人提供的在线直播。

Coq是一种形式化的验证证明，它提供了一种编写可执行数学定义和算法的形式语言。它还可以被用来写定理和环境的半交互式开发的机器检查证明。Coq通常用于验证程序、编程语言和数学的属性。不像数学证明是由人检查的，Coq证明是用计算机检查的。这有助于避免人们在阅读证明时可能会犯的错误。

通过使用Coq的协助证明来进行核查。它检查证明是否正确。剑桥梅隆大学的计算机科学副教授Karl Crary完成了验证工作。Leemon博士说这只是个开始。他说计算机验证的证明是未来的事，信任和安全是很重要的。

异步拜占庭容错

30多年来，拜占庭容错（BFT）一直被作为任何分布式系统的安全标准。如果一个系统能够保证所有节点都达成共识并知道他们已经达成共识，那么这个系统就被称为BFT。这种共识始终是一致的。

BFT需要在允许大量错误和攻击的同时实现这一点。这些拜占庭错误包括串通、撒谎和选择性不参与等行为。对于节点来说，通常很难对这些错误达成一致。此外，这些节点可能会崩溃。

最佳的BFT类型是异步的。在aBFT系统中，诚实的成员之间存在消息被延迟或太长的可能性。此外，他们可能无法到达其收件人。事实上，一个坏的参与者可以部分地控制网络。这是分布式共识的一个黄金立场。一个安全的分布式分类账技术需要在这样的假设下达成共识。

有些算法可能声称支持“部分”异步BFT。这就是消息不会被延迟超过给定时间段的地方。他们总是在规定的截止日期前完成任务。然而，现实是，许多攻击者可能会利用这一假设。它们既可以使网络陷入瘫痪状态，也可以扰乱交易的发生方式。

有了Coq证明，Hedera将是第一个使用计算机验证数学证明的账簿，这确实是异步的BFT。它确保了即使在网络错误和恶意节点的假设下也会出现一致。