01/02/2018

IELE:ブロックチェーンのための新しい仮想マシン

ランタイム・ベリフィケーション(RV) は、ブロックチェーン用の新しい仮想マシンであるIELEの最初のバージョンをリリースすることを誇りに思っています。

IELEとは?

IELEは、ブロックチェーンでスマートコントラクトを実行するために特化したLLVMの変種です。その設計、定義、実装は、スマートコントラクトを主要な目的として検証するセマンティクス・ファーストのアプローチに従って、最高の数学的基準で行われてきました。具体的には、Kフレームワークを使用したIELEの正式な構文とセマンティクスを定義しました。これは、プログラム検証ツールを含む一連のプログラム分析ツールに加えて実行可能な参照モデルを提供します。Kは私たちのチームによって過去15年間に作成されたもので、最新の言語設計、セマンティクス、および形式手法を取り入れています。IELEの設計は、Kで数十の言語を形式的に定義した経験に基づいていますが、特にKで2つの他の仮想マシンを正式に定義している間の経験と教訓を参考にしています。

  • KEVMEthereum仮想 マシン(EVM)の意味論。
  • LLVMの意味論であるKLLVM; LLVMセマンティクスの最新バージョンは完成され次第一般公開されます。初期バージョンはすでに利用可能です。

スタックベースのマシンであるEVMとは異なり、IELEはLLVMのようなレジスタベースのマシンです。無制限の数のレジスタを持ち、無制限の整数もサポートしています。IELEプログラムの挙動を知るために、参考となるものが2つあります(これらはまだ検証されておらず、変更されるかもしれません):

設計原理

IELEの設計が進んだのは以下のような理由からです。

  1. スマートコントラクトを高水準の言語から翻訳し実行するための、一律で低水準のプラットフォームとして目的に資すること。コントラクトはアプリケーション・バイナリー・インターフェイス(ABI)によって相互に作用します。ABIはIELEの中核となる要素であり、単なる最先端の規約ではありません。整数は無制限、レジスタ数も無制限であるため、高水準の言語からのコンパイルが、いっそう簡潔でエレガントに、そしてLLVMの成果を考えれば、長期的にはさらに効率的になるはずです。実のところ、LLVMの最適化手法の多くが引き継がれると考えられています。そのため、IELEは可能な限りLLVMの設計上の選択や表現にしたがいました。チームには(LLVMを開発した)イリノイ大学のLLVMの専門家も加わっています。

  2. すべての言語に及ぶ一律の手数料(ガス)モデルを提供すること。IELEのガス計算の一般的な設計哲学は「制約はないが、消費した分の代価を払うこと」です。たとえば、IELEプログラムが使用するレジスタ数が多くなればなるほど必要なガスも多くなります。あるいは、実行時間内に計算する数が大きくなればなるほどガスは多く必要となり、使用メモリが増えれば増えるほど(さまざまな場所に格納されたデータの位置とサイズ双方の観点から)ガスがいっそう増大する、といった具合です。

  3. 安全なスマートコントラクトをより簡潔に記述できるようにすること。これには、スマートコントラクトがしたがわなくてはならない要求事項を詳述すること、加えて、その詳細に関してスマートコントラクトの妥当性を立証する自動化技術をさらに開発しやすくすることも含みます。たとえば、どうにかして計算した数をスタックにプッシュし、それをアドレスとみなしてジャンプすると、現在のスマートコントラクトの枠組みでは立証は困難となり、それゆえに安全性は低下します。IELEには、LLVMと同じように名前のついたラベルがあり、ジャンプ文がそういったラベルへジャンプできるのです。またIELEは制限のあるスタックを使用しません。さらに、スタックや桁あふれを懸念する必要がないおかげでスマートコントラクトについて詳述し、立証するのははるかにたやすくなります。

    Kフレームワークを用いてすでに定義し、実証し、評価したEVMの形式的セマンティクスであるKEVMと同様に、IELEの設計もセマンティクスベースのスタイルでKを用いて行なわれました。まだ開発中のKの高速な(LLVMベースの)実行バックエンドとともに、IELEのセマンティクスから自動的に得られるインタープリタは効率が非常に良く、IELEのレファレンス実装として役に立つだろうと期待されています。

次は何をするか?

IELEの潜在能力を最大限に引き出すために、次の作業として計画しているのは以下の事柄です。

  • Kの効率的なバックエンド。これによってIELEをはじめとするKセマンティクスは、許容可能なパフォーマンスで実行できます。KEVM paperで述べているように、Kの現行バージョンがEVMセマンティクスを実行するパフォーマンスは、EVMのC++リファレンス実装のパフォーマンスよりも1桁小さい範囲内にとどまっています。Kの実行パフォーマンスを1桁分向上させることはできると確信しています。これが達成できれば、暫定的な方法でIELEを実装する必要はありません。IELEの実行可能なKセマンティクスがその実装にもなり、Correct-by-Construction手法によって、もはやVM自体の実装欠損が弱点として悪用されたりはしません。またIELE自体も保守しやすいでしょうし、先々のバージョン展開がやりやすくなるでしょう。

  • SolidityPlutusからIELEへのコンパイラ/トランスレータ。IELEに直接スマートコントラクトを記述するほうが、EVMに記述するよりも適しています。なぜならば、IELEは、人間に読み取れるように設計されたLLVM IRにしたがうからです。しかしそれでもIELEのコードは低水準であるため、エラーを起こしやすいのです。IELEを適正にテストし、全体設計や機能への信頼を獲得するために、SolidityからIELEへの、やはりKでのコンパイラ/トランスレータを実装することになるでしょう。スマートコントラクトのための実用本位なプログラム言語のなかでもPlutusはとりわけ人気となっていますし、またPlutusの形式的セマンティクスも定義しているので、SolidityからIELEへのコンパイラに続いてPlutusからのコンパイラもすぐに開発されるでしょう。

  • セマンティクスベースのコンパイル。Kのパフォーマンス向上に加えて、Kの最先端のツールを提供する計画です。このツールをセマンティクスベースのコンパイラと呼んでいます。詳細は以前のブログ投稿を参照してください。考え方としては次の通りです。プログラム言語のセマンティクスLとLのプログラムPを用いて、(シンボリック実行をしっかりと行ない)新しい言語セマンティクスL′を生成するのです。L′はP向けにLを特殊化したものです。少なくとも1桁分はパフォーマンスが向上すると予測しています。何より、これによってKセマンティクスに沿う任意のプログラム言語の任意のプログラムをIELEにトランスレートする一律な仕組みができ、こうしてIELE、およびKは任意の言語でスマートコントラクトを実行する普遍的プラットフォームになるでしょう。

  • CardanoブロックチェーンでのIELEの利用。

技術面の詳細とダウンロード

IELEはGithub上にあり、徹底的に議論されていますし、(MITライセンスと同様に寛容な)UIUCライセンスの元で自由に利用可能です。

上述した2つのIELEプログラム、つまりIELEのコードは人間にも読み取れることを示すerc20.ieleとforwardingWallet.ieleに加え、以下に示すgithubリポジトリへのリンクから、IELEとは何か、および、EVMやLLVMと何が違うのかがよく理解できるでしょう。

  • iele-syntax.md - IELE言語の形式的構文一式。
  • iele.md - IELE言語の形式的実行可能セマンティクス一式。
  • Design.md - IELEの設計原理、およびLLVMやEVMとの詳細な比較。
  • iele-gas.md - IELEの現状のガスモデル(IELEへのコンパイラ開発時には、いまだにこれにあわせて調整されます)

関連事項

オープンソース、コミュニティ主導による開発という精神の元、IELEに関する議論はすべて、以下に示す手段で継続するつもりです。

  • ライオット上では#IELE:matrix.org
  • ギッター上ではruntimeverification/iele-semantics

    関心をお持ちでしたらどんな方々でも、参加し、疑問点を出し、コードを寄せ、あるいは私たちのツールを経験してください。ドキュメント、初めて開発する人向けの効率的なインストール/クイックスタートプロセス、例やテストの充実に取り組める協力者をつねに求めてもいます。力を貸してくださる方を採用していますし、人材募集は今後も継続するつもりです! 開設したばかりのツイッターページ@rv inc

    に最新情報を投稿します。関心をお持ちの開発者の方はこれをフォローし、交流してください。

    さらに安全性の高いスマートコントラクトをご一緒に構築しましょう!

謝辞

IOHKに対し、IELEKEVMの双方に惜しみなく資金援助をしてくださったことに心より感謝します。特にIELEは、IOHKからの援助、継続的な研究会合、それにIOHKの研究チームと交わした刺激的な技術的議論があったからこそ実現できたのです。

また、Kチームにも感謝いたします。KEVMセマンティクスの定義を行ない(テクニカルサポートも参照のこと)、ERC20コンプライアンスのためのスマートコントラクトを立証してくださいました。Kチームの尽力とEVM水準での重要な証明のおかげで、スマートコントラクトの立証に向けたより有益な支援を得て、新たなVM探究が可能となりました。

Artwork, Mike Beeple

This blog article has been produced by IOHK and syndicated by Cardano Foundation for wider distribution.

LATEST FROM AUTHOR