哈希圖一致性算法已被驗證為異步拜占庭容錯

HederaHashgraph在下一代公共分類帳中擁有多樣化的治理。它最近宣布哈希圖一致性算法已被驗證為異步拜占庭容錯。這是通過使用Coq系統(tǒng)的計算機檢查的數(shù)學證明完成的。

?

分布式系統(tǒng)安全證明

這就是哈希圖報告中所提出的主張的證明。有人認為哈希圖在數(shù)學上是分布式系統(tǒng)的最高安全級別。Leemon Baird博士準備就正式方法舉行一次會議。這將在Hedera18舉行，它是首屆哈希圖開發(fā)人員會議。還有一個為感興趣的人提供的在線直播。

Coq是一種形式化的驗證證明，它提供了一種編寫可執(zhí)行數(shù)學定義和算法的形式語言。它還可以被用來寫定理和環(huán)境的半交互式開發(fā)的機器檢查證明。Coq通常用于驗證程序、編程語言和數(shù)學的屬性。不像數(shù)學證明是由人檢查的，Coq證明是用計算機檢查的。這有助于避免人們在閱讀證明時可能會犯的錯誤。

通過使用Coq的協(xié)助證明來進行核查。它檢查證明是否正確。劍橋梅隆大學的計算機科學副教授Karl Crary完成了驗證工作。Leemon博士說這只是個開始。他說計算機驗證的證明是未來的事，信任和安全是很重要的。

異步拜占庭容錯

30多年來，拜占庭容錯（BFT）一直被作為任何分布式系統(tǒng)的安全標準。如果一個系統(tǒng)能夠保證所有節(jié)點都達成共識并知道他們已經(jīng)達成共識，那么這個系統(tǒng)就被稱為BFT。這種共識始終是一致的。

BFT需要在允許大量錯誤和攻擊的同時實現(xiàn)這一點。這些拜占庭錯誤包括串通、撒謊和選擇性不參與等行為。對于節(jié)點來說，通常很難對這些錯誤達成一致。此外，這些節(jié)點可能會崩潰。

最佳的BFT類型是異步的。在aBFT系統(tǒng)中，誠實的成員之間存在消息被延遲或太長的可能性。此外，他們可能無法到達其收件人。事實上，一個壞的參與者可以部分地控制網(wǎng)絡。這是分布式共識的一個黃金立場。一個安全的分布式分類賬技術需要在這樣的假設下達成共識。

有些算法可能聲稱支持“部分”異步BFT。這就是消息不會被延遲超過給定時間段的地方。他們總是在規(guī)定的截止日期前完成任務。然而，現(xiàn)實是，許多攻擊者可能會利用這一假設。它們既可以使網(wǎng)絡陷入癱瘓狀態(tài)，也可以擾亂交易的發(fā)生方式。

有了Coq證明，Hedera將是第一個使用計算機驗證數(shù)學證明的賬簿，這確實是異步的BFT。它確保了即使在網(wǎng)絡錯誤和惡意節(jié)點的假設下也會出現(xiàn)一致。