完全異步BFT算法 為分佈式系統提供最強保護

完全異步BFT算法 為分佈式系統提供最強保護

系統安全在現今強勢的網絡攻擊，你該如何抵擋？。下一代分佈式公共總賬Hedera Hashgraph日前宣布，通過使用Coq系統計算機對算法證明進行檢查，hashgraph consensus算法已被證實是異步拜占庭容錯 (aBFT)。這證明了hashgraph技術報告中提出的聲明，即hashgraph是aBFT -算術上分佈式系統可能獲得的最高安全性級別。本月30日，Dr. Leemon Baird將在首次hashgraph開發人員會議——Hedera18上舉辦正式方法的講習會。

Coq是正式證明驗證系統。 Coq提供了一種形式化語言，用於編寫數學定義、可執行算法和定理。以及用於機器校驗證明的半交互式開發環境。它經常被用於驗證程序、編程語言和數學的屬性。與大多數由人檢查的數學證明不同，Coq證明實際上由計算機來檢查。這避免了人類在閱讀證據時所犯的一些錯誤。

驗證由Coq Proof Assistant執行，這會檢查證明是否正確，同時由卡內基梅隆大學計算機科學副教授Karl Crary完成。

Hedera首席科學家Dr. Leemon Baird說。 「對於安全和信任非常關鍵的軟件來說，類似這些經計算機驗證了正確性的數學證明的形式化方法是它們的未來。」

Hedera計劃繼續創建額外的Coq系統證明，以證明額外效率改進的正確性，並最終確保實施算法的軟件也是正確的。

異步拜占庭容錯

30多年來，拜占庭容錯 (BFT) 一直是分佈式系統安全的標準。拜占庭容錯意味著，即使惡意成員（拜占庭節點）試圖阻止這種共識，或欺騙他們得出不同的結論，網絡中的誠實成員也可以保證就共同的共識達成一致。如果能夠保證在某個時刻所有節點都同意共識，並且知道它們已經達成共識，並且總是一致的共識，則係統是BFT。

BFT意味著，即使在允許大量錯誤或攻擊的情況下也能做到這一點。拜占庭錯誤包括說謊、串通、選擇性不參與等行為。顯然，在這種類型的錯誤下，一組節點很難達成有效的共識，而在更簡單的情況下，節點可能會崩潰。

BFT最強的形式是異步。aBFT系統允許誠實成員之間的一些消息可能被任意地延遲很長的時間，或者根本就沒有發送給預期的收件人。對手甚至可能控製網絡本身，至少部分控制。這是分佈式共識的黃金標準。一個真正安全的分佈式總賬技術 (DLT) 必須能夠在這個假設下達成共識。

算法可能聲稱支持部分異步BFT，在這種情況下，消息不會延遲超過一定的時間，並且總是在截止日期之前通過。但如今的現實是，許多類型的攻擊者都能完全利用這一假設，或者讓網絡癱瘓，或者擾亂交易秩序。殭屍網絡、分佈式拒絕服務 (DDoS) 攻擊和惡意防火牆都可能干擾消息。因此，從長遠來看，「部分」異步BFT無法提供可靠的、真實世界的系統。