米国カーネギーメロン大学教授がCoqによる証明を完了、ハッシュグラフの合意アルゴリズムは非同期ビザンチンフォルトトラレントであると確認

2018年10月30日 15時00分

Source: Hedera Hashgraph, LLC

非同期ビザンチンフォルトトラレント（aBFT）は分散システムで業界最高レベルのセキュリティ

米国テキサス州ダラス, 2018年10月30日 - (JCN Newswire) - Hedera18開発者カンファレンス -- 次世代の公開分散型台帳で、非常に多様なガバナンス構造を持つヘデラ・ハッシュグラフは本日、ハッシュグラフの合意アルゴリズムが、非同期ビザンチンフォルトトラレント（aBFT）であることが、Coq証明支援システムを活用するコンピュータによって検証された数学的証明により確認されたことを発表しました。これは、ハッシュグラフ技術レポートに記載された、ハッシュグラフは分散システムにおける数学的に最高レベルのセキュリティの非同期ビザンチンフォルトトラレントであるとの主張を証明するものです。初開催となるハッシュグラフ開発者カンファレンスHedera18にて、Leemon Baird 博士は本日、形式手法をセッションで発表します。ご関心のある方はライブストリーミングを無償で視聴いただけます。
http://learn.hederahashgraph.com/livestream

Coqは形式検証システムであり、数学の定義や定理、実行可能なアルゴリズムを記述するための形式言語と、機械証明のセミインタラクティブな開発環境を提供します。Coqは多くの場合、プログラム、プログラミング言語、数学の特性の認証に使われています。人間だけで検証が行われる大部分の数学的証明と異なり、Coqによる証明は実際にコンピュータによって検証されるため、人間が証明を読む時に犯す間違いを回避できます。

この形式検証は、証明の正しさを検証するCoq証明アシスタントによって行われ、米国カーネギーメロン大学コンピューターサイエンス学部のKarl Crary准教授によって完了されました。詳細はこちらをご参照ください。https:/hedera.com/platform#security

ヘデラのチーフ・サイエンティストであるLeemon Baird博士は述べています。「これはまだ序章にすぎません。コンピュータが数学的証明の正しさを検証するという、こうした形式手法は、セキュリティや信頼が必要不可欠なあらゆる領域において、ソフトウェアの未来のあり方です。」

今後も、ヘデラではCoqシステムによる証明をさらに作成して、さらなる効率の改善の正しさを証明し、最終的にはこのアルゴリズムを実装するソフトウェアの正しさも確認していきます。

非同期ビザンチンフォルトトラレント
30年以上にわたり、分散システムにおける業界標準のセキュリティはビザンチンフォルトトラレント（BFT）でした。ビザンチンフォルトトラレントとは、ネットワークの悪意のあるメンバー（ビザンチンノード）が合意形成を妨げたり、誠実なメンバーをだまして異なる結論に到達させようとする場合でも、誠実なメンバーは共通の合意形成に達することができるというものです。いずれ全てのノードが合意に達することができる場合、システムはビザンチンフォルトトラレントであり、全てのノードによって合意に達し、その合意が常に同じであることが認識されます。

ビザンチンフォルトトラレントは、さまざまな障害や攻撃を許容しながらも、合意形成に達することを意味しています。ビザンチンフォルトには、嘘、結託、選択的な不参加などが含まれます。こうしたエラーがある場合、ノードはただクラッシュするという、より単純なシナリオと比べて、一連のノードが有効な合意に達するのが困難になるのは明らかです。

最も強力なビザンチンフォルトトラレントは非同期です。非同期ビザンチンフォルトトラレントでは、誠実なメンバーの間でメッセージの受信がかなり遅れたり、相手にメッセージが全く届かないなどの可能性が許容されます。敵は部分的であってもネットワーク自体を制御するかもしれません。これが業界最高レベルの分散合意です。真にセキュアな分散型台帳技術（DLT）はこれを前提に合意形成を達成しなければなりません。

アルゴリズムのなかには、一定の時間を超えてメッセージの受信に遅れが生じることは決してなく、常にある一定の時間内にメッセージを届けられるとして、「部分的」に非同期ビザンチンフォルトトラレントであると主張するものがあるかもしれません。しかし、現実の世界では、ネットワークを破壊したり、取引の順番を変更するなど、多くのさまざまな攻撃者がまさにこの前提を標的とすることが可能です。ボットネット、DDoS（標的型攻撃）、悪意のあるファイアウォールの全てがメッセージの送受信を妨害できます。したがって、「部分的」な非同期ビザンチンフォルトトラレントは、長期的に高信頼な実世界のシステムに対応できません。ヘデラでは、インターネット全体にわたり、最終的に何兆ドルもの取引を処理可能な信頼レイヤを構築中であり、こうした攻撃に対処するため、最も強力なセキュリティ原則を適用する必要があります。

今回のCoqによる証明により、ヘデラは、真に非同期ビザンチンフォルトトラレントであるという数学的証明がコンピュータによって検証された、初の分散型台帳となります。ヘデラでは、合意形成は達成可能であり、合意に達し、その合意が常に同じであることが認識されることを保証します。これは、悪意のあるノードやネットワークのエラーについての現実的な前提のもとでも変わりません。

詳細はこちらをご参照ください。https:/hedera.com/platform#security

ヘデラについて
ヘデラ・ハッシュグラフ・プラットフォームは、グローバルな分散アプリケーションを誰でも簡単に開発できる、非常に多様なガバナンス構造を持つ公開分散型台帳を提供します。開発者は、ヘデラ・ハッシュグラフ・プラットフォーム上で、安全性が高く、公正かつ超高速の分散アプリケーションを構築できます。詳細については https://hedera.com/ をご覧いただくか、Twitter @hashgraph、Telegram（ https://t.me/hederahashgraph ）もしくはDiscord（ http://hedera.com/discord ）をフォローしてください。ホワイトペーパーは https://hashgraph.com/whitepaper をご参照ください。

報道機関からのお問い合わせ先
Zenobia Godschalk
E: pr@hashgraph.com
T: 1.833.794.7537 x 717

Source: Hedera Hashgraph, LLC
セクター: Crypto, Exchange, フィンテック, アントレプレナー