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

?

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

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

Coq是一種形式化的驗(yàn)證證明，它提供了一種編寫(xiě)可執(zhí)行數(shù)學(xué)定義和算法的形式語(yǔ)言。它還可以被用來(lái)寫(xiě)定理和環(huán)境的半交互式開(kāi)發(fā)的機(jī)器檢查證明。Coq通常用于驗(yàn)證程序、編程語(yǔ)言和數(shù)學(xué)的屬性。不像數(shù)學(xué)證明是由人檢查的，Coq證明是用計(jì)算機(jī)檢查的。這有助于避免人們?cè)陂喿x證明時(shí)可能會(huì)犯的錯(cuò)誤。

通過(guò)使用Coq的協(xié)助證明來(lái)進(jìn)行核查。它檢查證明是否正確。劍橋梅隆大學(xué)的計(jì)算機(jī)科學(xué)副教授Karl Crary完成了驗(yàn)證工作。Leemon博士說(shuō)這只是個(gè)開(kāi)始。他說(shuō)計(jì)算機(jī)驗(yàn)證的證明是未來(lái)的事，信任和安全是很重要的。

異步拜占庭容錯(cuò)

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

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

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

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

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