イテレーション開発

仮想通貨は、ソフトウェアとして実装されたプロトコルです。プロトコルとは単に参加者間の知的な会話です。ソフトウェアは究極的にはいくつかの目標を与えられたデータの操作です。しかし、信頼性が非常に高いソフトウェア及び有用で安全なプロトコルと、その逆のものとの違いは完全に人間的です。

優れたソフトウェアは説明責任、明確なビジネス要件、繰り返し可能なプロセス、徹底したテストと飽くなき反復を必要とします。優れたソフトウェアには、問題を解決できるシステムを適切に設計するための専門知識と、才能のある開発者が求められます。

有用で安全なプロトコル、特に暗号と分散システムを含むプロトコルは、より学術的で規格駆動のプロセスから始まります。プロトコルが有用であることを保証するためには、査読、無限の議論、トレードオフの確固たる概念が必要です。しかし、これだけでは十分ではありません。プロトコルを実装し、実際に使用し、テストしなければなりません。

仮想通貨業界特有の課題は、全く異なる2つの哲学が適切な弁証法を行わずに絡み合っているということです。我々の命題は、若さ、欲求、情熱に支えられたスタートアップの心構えである「迅速に行動し、破壊する」ことです。これに対する反対命題は、十分な資金と威信を享受しながら、業界の革新をニッチのようなものに入れ込んで確実にしようとする願望によって動機付けされた、慎重かつ系統的で、学問的なアプローチです。

その結果、多くの仮想通貨は、ほとんど意味のないホワイトペーパーによって策定されたか、または急いで書かれたプログラムコードです。現在、時価総額トップ1018の仮想通貨のいずれも、査読されたプロトコルに基づいてもいなければ、正式な仕様19からの実装も行われていません。

しかし、これらには数十億ドルの価値が絡んでいます。一度導入されると、仮想通貨に変更を加えることは非常に困難です。ユーザーは、安全なシステムの使用と、マーケティングの主張の正当性をどのように知ることができるのでしょうか。提案されたプロトコルが達成できない場合には、どうなるのでしょうか。

この命題の欠如にも関わらずプロセスのみが尊重されていることが、IOHKがカルダノを構築したかった主な理由です。我々の望みは、より効果的で、誠実かつ正直な方法で取り組む事例として参考となるプロジェクトを開発することでした。

目標は、ソフトウェアとプロトコル開発する上でのまったく新しい手法を提案するのではなく、素晴らしいソフトウェアとプロトコルがすでに存在することを認識し、その創造につながった条件を踏襲することです。次に、これらの案件をできる限り一般に知られるようにオープンソース化し、業界全体の利益となるよう参照可能にすることです。

事実と意見

もう一つの懸念は、事実と意見の境界線が曖昧なことです。この世には、何百ものプログラミング言語、数多くの開発パラダイム、プロジェクト管理に関する幾多もの哲学があります。学界は、ビジネス上の懸念や実用性から遠ざかっていることから、独自の課題を抱えています。

カルダノはまず、工学の観点から普遍的に有用であると認められる明らかな欠点を捕らえようと試みました。たとえば、暗号化システムと分散システムの両方が非常に複雑なトピックであるため、安直な行為によって恐ろしい間違いを犯した事例は数多くあります。したがって、これらの分野からの識見を必要とするプロトコルは、定評のある専門家によって設計され、他の専門家が審査を行うために提出される必要があります。

ウロボロスはこの分野において最初のケーススタディです。これは、公的に検証可能な出版履歴を持つ暗号学者達の大規模かつ多様なチームによって設計され、標準的な暗号プロセス、セキュリティの仮定、敵対的なモデルおよびその証明などに基づいて構築されました。これらの証明は学会への提出20およびに、ケンブリッジ大学の研究チーム21開発の定理証明システムIsabelleによって独自に検証されました。

しかし、この作業だけではその有用性を保証できません。いくつかの仮定を踏まえたセキュリティモデルの厳密なチェックを行なっただけです。有用性を実証するためには、プロトコルを実装し、テストする必要があります。我々の開発者はHaskellRustの両方で検証を行いました。この作業により、同期モデルに焦点を当てる必要があることが明らかになりました。これはウロボロス・プラオスの策定にもつながります。

このようなイテレーション開発が素晴らしいプロトコルを生み出すのです。それぞれのステップが新しい教訓をもたらし、前のステップの正しさの再確認を要求するからです22。プロトコルが正しく設計されていることを確認するのは費用と時間がかかり、時には非常に面倒であっても、必要とされています。

プロトコル 、特に何十億もの人々によって使用されるものは短命でもなければ、急速的に進化するわけでもありません。むしろ、それは何十年も利用されることを目的としています。今後100年間は利用されるであろう新しい金融システムを世界に押し付ける前に、設計者に対して厳しい要求を行うのが合理的でしょう。

関数型の罪

より偏見を伴った話題に話を移しますと, ツール, ソフトウェア開発に使用される言語と方法論は、客観的実在というよりも宗教的な摂理による成果物です。ソースコードは散文のようなものです。誰もが何が良いのかということに対して意見を持っています。時には伝える内容よりも、その伝達方法の方が重要である場合もあります。

我々は、他人には間違っていると受け取られかねないものを選ばなければなりません。しかし、我々の選択の背景には、その判断を正当化するための基盤があります。

カルダノを実行しているプロトコルは、純粋関数型言語であるHaskellで実装されています。ユーザーインターフェイスは、ElectronのフォークであるDaedalusによってカプセル化されています。我々はできるだけWebアーキテクチャモデルを採用し、データベースでKey-Valueパラダイムを取り上げるためにRocksDBを使用しました。

コンポーネントレベルから見れば、この抽象化はメンテナンスがはるかに容易になり、より優れた技術が苦もなく導入され、また我々の技術スタックがGithubとFacebookの開発成果に部分的に結びついていることを意味します。

WebGUIを使用することで、Reactを活用し、フロントエンドの機能を何十万人ものJavaScript開発者が理解できるツールを使用して開発することができます。Webアーキテクチャを使用するということは、コンポーネントをサービスとして扱うことができ、セキュリティモデルが分かりやすくなることを意味します。

プロトコル開発のためにHaskellを採用することは、最も困難な選択でした。関数型言語の世界でも、選択肢は豊富にあります。より柔軟で不純な言語として、Clojure、Scala、F#のようなものがあります。これらの言語は、Javaと.NETエコシステムの膨大なライブラリの恩恵を受けるとともに、機能プログラミングの最良の側面を確保しています。

AgdaIdrisのような学問指向の言語は、正確性に関して強力な検証を可能にする技術と密接に関連しています。しかし、彼らには手ごろなライブラリや、卓越した開発経験がありません。

カルダノでは、OcamlとHaskellどちらかを選ぶことにしました。Ocamlは、素晴らしいコミュニティ、優れたツール、十分な開発経験、そしてCoqによる正式な検証に関する素晴らしい資産を持つ言語です23。では我々はなぜ Haskell を選んだのでしょうか。

なぜHaskellなのか

カルダノを構成するプロトコルは暗号学によって配布、バンドルされるため高度なフォールトトレランスを必要とします。最も好調な日でも、ビザンチンアクターが出現したり、不正な形式のメッセージが発信されたり、誤ったクライアントが意図せずにネットワーク上に何らかの騒ぎを起こしたりするかもしれません。

まず、Quickcheckなどや、Refinement Typesのような、より洗練された技術を容易に使用できる強力な型システムを採用でき、フォールトトレランスにある程度期待ができる言語を使いたいと考えました。HaskellとOcaml等が前者を満足させるのに対し、ErlangスタイルのOTPモデルは後者を満たします。

Cloud Haskellを導入したことで、Haskell独自の機能を維持しつつ、Erlangの利点の多くを獲得することができました。さらに、Haskellのモジュール性と合成性により、Time Warpというカルダノ専用の軽量ライブラリを使用することができました。

次に、Haskellのライブラリは、GaloisFP CompleteWell-Typedなどの商業用エンティティの広範な開発によって、ここ数年で大幅な進化を遂げました。結果として、Haskellを使用して本番レベルのアプリケーションを書くことができるようになりました24

さらに、PureScriptの急速な進化は、ClojurecriptがClojureに与えたように、HaskellとJavaScriptの間の必要不可欠な架け橋となっています。カルダノのブラウザ上での動作、またモバイルウォレットの開発には、PureScriptが特に重要になると考えています。

加えて、依存関係の解消に関して言えば、Haskellは、過去数年間、FP Completeから強力な援助を受けて作り出され、容易に利用できるStackageを通して、Michael Snoymanのような技術者が達成した重要な社会的、技術的成果から恩恵を受けています。

また、適切に依存性を解決した上で、我々はソフトウェアのビルドを再現可能にすることを目指しています。つまり、同じ構成値と依存バージョンであれば、まったく同じ成果物が作成されるということです。Stackageを通して、我々はNixOpsを利用し、その再現性を獲得することができました。

最後に、Haskellに特化した才能ある開発者の人口は、他の言語と比較してもかなり大きく、彼らは学術的にも、業界的にも十分に訓練されています。また熟練のHaskell開発者の中にコンピューターサイエンスに関する豊富な知識を持っていない者はほとんどいないため、Haskellは優秀な人材を確保するためのフィルターとしても機能します。

正式な仕様と検証

証明可能な正しいセキュリティモデルを使用してプロトコルを開発することの強みは、敵対的なパワーの限度に関する保証を提供することです。プロトコルが守られ、証明が正しければ、敵対者には、プロトコルのセキュリティ性に違反することができないという約定が与えられます。

より深く洞察すれば、前述の主張の重要性がより明らかになります。敵は予想外に知的かつ有能である場合もあります。数学的モデルだけで彼らの攻撃を防ぎきれるというのは言い過ぎです。それは全く真実ではありません。

現実は、純粋なセキュリティと正常な動作の妨げとなる要因と環境をもたらします。実装が間違っている可能性があります。ハードウェアは、これまで考慮されていなかったベクトルからの攻撃を呼び込む可能性があります。セキュリティモデルが不十分であり、実際の使用に準拠していない可能性があります。

従って仕様、厳重性及びチェックがどれほどプロトコルに要求されているかについての判断が必要となります。例えば、SeL4 Microkernelプロジェクトのような試みは、曖昧さに対する徹底的な攻撃であって、10,000行未満のC言語のコードを検証するために、ほぼ200,000行のIsabelleコードを必要とする主要な例です。しかし、オペレーティングシステムのカーネルは、適切に実装されていないとセキュリティ上の深刻な脆弱性となりうる重要なインフラストラクチャです。

すべての暗号化ソフトウェアは同様の難題に取り組まなければならないのでしょうか。あるいは、同等の成果を生み出すことのできる、それほど厳重ではない手段を選ぶことはできないのでしょうか。また、それが実行されている環境に脆弱性があると悪名高いWindowsXPなどであるならば、プロトコルを完全に実装しようとするのは無意味ではないでしょうか。

カルダノは、以下の点に関して妥協を行いました。まず、暗号技術と分散コンピューティングの複雑な性質のために、検証は非常に繊細で、長く、複雑で、時には至って専門的になる傾向があります。これは、人間によって行われる検査が退屈でエラーを起こしやすくなることを意味します。したがって、コアインフラストラクチャを網羅するために作成されたホワイトペーパーに示されている重要な証明はすべてコンピューターでチェックする必要があると考えています。

次に、Haskellのコードが当社のホワイトペーパーに正確に対応しているかの検証には、LiquidHaskellを介したSMT証明者とのインターフェースとIsabelle/HOLのいずれかを選択することができます。

SMT(充足可能性モジュロ理論)ソルバーは、等式または不等式を満たす関数パラメータを見出す、あるいはそのようなパラメータが存在しないという課題に取り組みます。De MouraとBjørnerが議論したように、SMTの使い道は様々ですが、重要な点は、これらの手法が強力であり、バグやセマンティックエラーを劇的に減らすことができることです。

一方、Isabelle / HOLは、実装の特定と検証の両方に使用できる表現力豊かで多様なツールです。Isabelleは、高次論理構造を扱う包括的な定理ソルバーであり、検証に使用される集合やその他の数学的オブジェクトを表現することができます。そのような制約を伴う問題に取り組むためにIsabelleはZ3 SMT検証システムと統合しています。

どちらのアプローチも有益であるため、両者を段階的に採用することにしました。人間によって記述された検証は、Isabelleでコード化され、その正確性を確認し、それによって我々のシステム化された検査の要件を満たしたことになります。そして、2017年と2018年にかけてカルダノに実装されているすべての本番コードにLiquid Haskellを徐々に追加する予定です。

最後に、正式な検証は、検証している仕様と利用できるツールセットと同じくらい優れています。Haskellを選択する主な理由の1つは、それが実用性と理論の適切なバランスを保っているためです。ホワイトペーパーから得られた仕様は、Haskellのコードによく似ており、この2つを関連づけることは、命令的な言語で行うよりもはるかに容易です。

適切な仕様をキャプチャし、アップグレード、バグ修正などの変更が必要なときに仕様を更新することは未だに困難ですが、それによってHaskellの評価が落ちるようなことはありません。開発者が証明可能安全性の基盤を構築することに苦労しているなら、理論上提案されているものを実装しなければなりません。

透明性

仮想通貨の開発および工学について議論する際の最後の論点は、どのようにプロジェクトの透明性を確保するかということです。設計上の決定とは、開発者の夢に出てきて突然具現化するような、明解な論理値や、エーテルのような非現実的なものではありません。これらは過去の過ちから得た経験、討論、教訓などから生まれたものです。

課題は、完全に透明な開発プロセスが、議論に影響を及ぼし、証拠に基づくものよりも大げさになることです。エゴがコミュニティを勝ち取ろうと試みます。また愚かであるという恐れがあると、会話は無力化し、非生産的なものとなってしまいます。

さらに部外者が、自身に興味のあるトピックのみを取り上げるために会話をすり替えようとするかもしれません。各人が求めているものはそれぞれ異なるからです。

恐れることなく自由に表現しながらも、進捗を開発者に任せているような、委託されたコミュニティが開発プロセスの必要性に関する透明性のバランスを保つためにはどのようにすれば良いのでしょうか。

カルダノでは、指揮監督のもとで規格駆動のプロセスを行う方法を採用することにしました。コミュニティは理論とコードがよく考えられ、検証されており、それによって開発者が解決したと主張するような物事が、実際に解決されているかどうかを確認する必要があります。そのために査読は、科学的要素を完全に満たしていなければなりません。なぜなら、それはまさにこの目的のために設計され、そして現代の世の中を切り開いてきたからです。

コードについては意見が分かれます。カルダノでは、カルダノ財団をIOHKの成果物の最終審査員として選任しました。特に、彼らには以下の任務が委ねられています。

  1. カルダノGithubに含まれるソースコードに対して定期的にレビューを行い、その品質、テストカバレッジ、適切なコメントと完全性を確認する

  2. カルダノ全てのドキュメントに対してレビューを行い、その正確性、有用性を確認する

  3. 科学者によって作成されたプロトコルが実装されているという主張に対して検証を行う

この務めを果たすために、IOHKは定期的でタイムリーな報告書を財団およびその代理人に提出し、審査を行ってもらいます。財団は、少なくとも四半期ごとにカルダノのコミュニティへの開発監視報告書をリリースする予定です。

この最初の取り組みに関しては、分散型プロジェクトがどのように説明責任を果たすかについて、より幅広い会話が開始される予定です。信頼できる第三者からの開発監督は、開発者が確実に軌道に乗るようにするための強力なツールですが、プロジェクトが常に実現されることを完全に保証するには不十分です。

このため、財団はCSLに財務システムを統合後、IOHK と共同開発された正式仕様に基づいた代替クライアントを構築する開発チームの奨励を行います。開発の多様性は、単一のアイデアや開発者によってモノカルチャーが形成されるのを回避するために、イーサリウムプロジェクトで使用された素晴らしい技法でした。

仕様に関しては、WC3IETFに準拠した標準プロセスから得られる豊富な知識があります。最終的には、カルダノの各プロトコルを統合するには、学術的な作業やソースコードとは独立した仕様が必要となります。むしろ、それはRFCのような適切な形式である必要があります。

カルダノ財団の中核となる教義の1つは、カルダノプロトコル専用の標準化団体として機能し、カルダノに関連する規格の更新、追加、変更についての意見交換の場を設けることです。IETFを通じてインターネット(標準の製品)が、どのようなコアプロトコルを使用するかについてコンセンサスを得ることができるのであれば、専門の機関が同様の結果を導き出すと仮定することも理にかなっています。

最後に、これらの議論をブロックチェーン上でホストされている分散したエンティティとして検討することは興味深いものです。この概念は自律分散組織(DAO)と呼ばれ、この分野に関する予備作業が現在進行中です。IOHKはカルダノを利用するエンティティのために必要に応じて使用できる参照DAOモデルを開発し、カルダノ財団にはこれを自身が定めた基準に基づいて採用する決定権があります。


脚注

18: 時価総額による包括的なリストについては www.coinmarketcap.com を参照

19: イーサリアムには、Yellow Paperと呼ばれる半正式な仕様があります。 ただし、EVMのセマンティクスは完全には規定されておらず、プロトコルの完全なる実装には不十分です。

20: カリフォルニア州で開催されたIACRのAnnual Crypto Conferenceの論文番号71

21: ローレンス・ポールソン教授の監督下の Kawin Worrasangasilpa による

22: 少し話が逸れますが、これに関してはハルモス教授の数学の教科書の書き方についてのディスカッションを是非ご覧になってください

23:この点に加えて、IOHKは実際にはOcamlでQeditasと呼ばれるプロジェクトを変名Bill Whiteから継承し、実装しています

24: Bryan O’Sullivan氏は、ここでHaskellの産業利用について素敵な話をしてくれています。