异步拜占庭容错 (aBFT) 是分布式系统安全性的“黄金标准”
得克萨斯州达拉斯, 2018年11月12日 – (亚太商讯) – Hedera18开发人员会议– 具有高度分布式治理的下一代分布式公共总账Hedera Hashgraph日前宣布，通过使用Coq系统计算机对算法证明进行检查，hashgraph consensus算法已被证实是异步拜占庭容错(aBFT)。这证明了hashgraph技术报告中提出的声明，即hashgraph是aBFT -算术上分布式系统可能获得的最高安全性级别。今天，Dr. Leemon Baird将在首次hashgraph开发人员会议——Hedera18上举办正式方法的讲习会。感兴趣的参与者可以免费观看直播流，网址是http://learn.hederahashgraph.com/livestream。
Coq是正式证明验证系统。 Coq提供了一种形式化语言，用于编写数学定义、可执行算法和定理。以及用于机器校验证明的半交互式开发环境。它经常被用于验证程序、编程语言和数学的属性。与大多数由人检查的数学证明不同，Coq证明实际上由计算机来检查。这避免了人类在阅读证据时所犯的一些错误。
验证由Coq Proof Assistant执行，这会检查证明是否正确，同时由卡内基梅隆大学计算机科学副教授Karl Crary完成。可在以下找到更多信息，网址是：https:/hedera.com/platform#security。
“这只是个开始，”Hedera首席科学家Dr. Leemon Baird说。 “对于安全和信任非常关键的软件来说，类似这些经计算机验证了正确性的数学证明的形式化方法是它们的未来。”
Hedera计划继续创建额外的Coq系统证明，以证明额外效率改进的正确性，并最终确保实施算法的软件也是正确的。
异步拜占庭容错
30多年来，拜占庭容错 (BFT) 一直是分布式系统安全的标准。拜占庭容错意味着，即使恶意成员（拜占庭节点）试图阻止这种共识，或欺骗他们得出不同的结论，网络中的诚实成员也可以保证就共同的共识达成一致。如果能够保证在某个时刻所有节点都同意共识，并且知道它们已经达成共识，并且总是一致的共识，则系统是BFT。
BFT意味着，即使在允许大量错误或攻击的情况下也能做到这一点。拜占庭错误包括说谎、串通、选择性不参与等行为。显然，在这种类型的错误下，一组节点很难达成有效的共识，而在更简单的情况下，节点可能会崩溃。
BFT最强的形式是异步。 aBFT系统允许诚实成员之间的一些消息可能被任意地延迟很长的时间，或者根本就没有发送给预期的收件人。对手甚至可能控制网络本身，至少部分控制。这是分布式共识的黄金标准。一个真正安全的分布式总账技术 (DLT) 必须能够在这个假设下达成共识。
算法可能声称支持部分异步BFT，在这种情况下，消息不会延迟超过一定的时间，并且总是在截止日期之前通过。但如今的现实是，许多类型的攻击者都能完全利用这一假设，或者让网络瘫痪，或者扰乱交易秩序。僵尸网络、分布式拒绝服务 (DDoS) 攻击和恶意防火墙都可能干扰消息。因此，从长远来看，“部分”异步BFT无法提供可靠的、真实世界的系统。由于Hedera建立了一个互联网范围的信任层，最终可能处理价值数万亿美元的交易，因此我们必须确保我们应用最强大的安全原则来应对此类攻击。
有了新的Coq证明，Hedera成为首个拥有计算机验证的数学证明的公共总账，证实它是真正的异步BFT。它保证了共识的达成，当它发生的时候我们会知道，我们都会达成同样的共识，甚至在对恶意节点和网络错误的现实假设下也是如此。
可在以下找到更多信息，网址是：https:/hedera.com/platform#security。
关于Hedera
Hedera hashgraph平台将提供具有高度多样化治理的分布式公共总账，任何人都可以轻松地开发全球分散的应用程序。开发人员可以在Hedera hashgraph平台上构建安全、公平、快速的分散式应用程序。更多资讯请见https://hedera.com/ ，或是关注我们的社交帐号Twitter: @hashgraph, Telegram: https://t.me/hederahashgraph或是Discord: http://hedera.com/discord 。 Hedera白皮书请见 https://hashgraph.com/whitepaper 。
媒体垂询:
Zenobia Godschalk
E: pr@hashgraph.com
T: 1.833.794.7537 x 717
News URL: https://www.acnnewswire.com/press-release/simplifiedchinese/47679/
转载请注明：牛牛网 » 由卡耐基梅隆大学教授完成的Coq证明证实Hashgraph Consensus算法是异步拜占庭容错算法