Runtime VerificationとIELE - 相互運用性から普遍性へ
KEVMとIELEがCardanoにもたらす、比類なきレベルのセキュリティ、スケーラビリティ、プログラム可能性
2021年 5月 10日 5 分で読めます
新興のRuntime Verification(RV)社の会長兼CEO、Grigore Rosu教授が3月のCardano360マンスリーショーに出演し、そのアイデアと、RVとIOHKのコラボレーションについて語ってくれました。
Rosu教授およびRVと私たちとのプロフェッショナルな関係は2017年に遡ります。教授の経歴が(どの言語でも)それを物語っています。Rosu教授はNASA、DARPA、Microsoftに勤め、イリノイ大学アーバナ・シャンペーン校で教鞭をとってきました。
彼はまた、「単に失敗するわけにはいかないソフトウェア」と評されているKフレームワークを手掛けています。15年にわたり開発されているこのフレームワークの主要目的は、セキュリティの強化です。この詳細は後述するとして、まずは簡単に歴史を振り返ります。
スマートコントラクトに関して言えば、まずEthereum Virtual Machine(イーサリアムバーチャルマシン:EVM)が初期の多くの標準を定めました。例えば、Solidityを使用したお馴染みのERC-20スマートコントラクトの作成です。しかし、このシステムは完璧なものではありません。スマートコントラクトはコードの脆弱性で知られ、これが安全性の問題を引き起こしてきました。
IELE:比類のないセキュリティ、スケーラビリティ、プログラム可能性
2020年後半から、Cardano開発者は、KEVM(Kイーサリアムバーチャルマシン)を介してSolidity/イーサリアムコミュニティとつながりを持ってきました。KEVMはKフレームワークで指定したEVM実装で、開発者は、Kがコントラクトの正確性を確認するために作成したフォーマル検証を使用することができます。
IELEは物事を一歩先へ進めます。Rosu教授が3月のCardano360で説明したように、IELE(イエレ:ルーマニア神話に登場する妖精のような生き物にちなむ)はスマートコントラクトを実行し、ブロックチェーン開発者に人間が読める言語を提供する仮想マシンです。IELEは、イーサリアム用にSolidityで作成されたスマートコントラクトが抱えるセキュリティと正確性の問題に対処するために、形式手法を念頭に設計され、セキュリティ、スケーラビリティ、プログラム可能性をレベルアップする道を容易にします。
IELEは、LLVMコンパイラーの中間表現に似ています。これにより、LLVMコミュニティの豊富な知識が活用できます。具体的には、安全で効果的なコンパイラー最適化の作成に費やされた作業がLLVM IRに活かされます。LLVMコンパイラーにつぎ込まれた努力の多くを、IELEオプティマイザーにも移植することができます。
LLVMとは
IELEが実装されると(教授によると、6か月以内に最初のプルーフオブコンセプトのテストが可能になります)、開発の機会はさらに広がります。IELEは仮想マシンというよりパスポートのようなもので、新しいユニークな才能の宝庫への(水門といわぬまでも)扉を開きます。開発者の中には、かつて一から新しいプログラミング言語を学ぶことを考えて、ブロックチェーン分野に入ることをあきらめた人もいるでしょう。RVの革新的なアプローチによる直接的な結果として、スマートコントラクトに参入したい開発者は誰でも、Solidityを含む自分の良く知っている言語で作成することができるようになります。結果作成されたものは、ソース言語に関係なく、IELEを装備したブロックチェーンで正常に実行されます。
Cardanoにとって意味するもの
この成功により、開発者や企業には、イーサリアムから移行し、Cardanoブロックチェーンに参加するインセンティブが与えられます。オープン性、包括性、相互運用性はCardano構築の基盤です。その哲学は常に、あらゆるバックグラウンドを持つ開発者を歓迎し、Cardanoの着実な進化を確保することです。Rosu教授には大胆な計画があります。「IELEはこの十年の私たちの研究の目玉です」と、彼は述べます。「これは、普遍的なフレームワークとして望みうる最大のものです」と。
最後に
RVとの提携は、IOHKの革新への献身を、そしてCardanoをできるだけ広く開発者コミュニティへ開放する姿勢を示しています。KEVM/IELEの実装により、協調へ向けた新たな道が築かれ、Cardanoのリーチと相互運用性が拡張されます。そしてこれが、「構築による修正」環境のコンテキストにおける新たなアイデア、コンセプト、技術開発の探求へと導きます。
Alexによる他の記事はCardanoコミュニティサイト、Adapulseをご覧ください 。
最新の記事
Input | Output chief scientist receives prestigious Lovelace computing award 筆者: Fergie Miller
3 December 2024
Delivering change in Ethiopia: lessons and reflections 筆者: Staff Writer
28 November 2024
Applying formal methods at Input | Output: real-world examples 筆者: James Chapman
26 November 2024