Synereoのスマートコントラクト言語を使用してハッキングを防ぐ方法

攻撃や操作に適切に抵抗する分散表現のプロトコルを設計することは、簡単な作業ではありません。比較的単純なユースケースを解決したとしても、ビットコインは中央管理のない通貨を提供することに成功したことで賞賛に値します。金融契約やガバナンスなどのより複雑な問題に対処する場合は、ルールを確立する必要があります。

DAO 攻撃が契約の問題によるものなのか、それとも Ethereum のスマート コントラクト言語 Solidity 自体の欠陥によるものなのかはともかく、ミッション クリティカルな状況で展開される契約の分析を支援するためのより優れたツールの必要性を浮き彫りにしているのは間違いありません。このようなツールを備えるには、候補となるスマート コントラクト言語の仕様がより高度である必要があります。実際には、契約を信頼性の高い実稼働レベルのサービスとして分析するためのツールを備えた、数学的に高度な仕様 (形式意味論と呼ばれることが多い) が必要です。

形式セマンティクスがなければ、コードについて推論したり、コードの動作を指定したり、形式検証を使用して仕様に準拠していることを確認したりすることは不可能です。事実上、Solidity のセマンティクスの唯一の仕様は、Ethereum 仮想マシン (EVM) 用にコンパイルされるバイト コードです。このコンパイラは正式に検証されていません。さらに、この仮想マシンが実行するコードは検証されていないため、Solidity 契約が何を行うのかについてはほとんど何も言えません。

イーサリアムのアプローチの厳密さの欠如は、初日から懸念の原因となってきましたが、ほとんどの人は、中央機関や仲介者によって引き起こされる摩擦から完全に独立した契約システムという単なるアイデアにすでに夢中になっているため、簡単に却下されてきました。予想どおり、形式意味論の単純な実装フリーの実装では、ミッションクリティカルな契約を適切に分析するために必要なレベルの精度が得られない段階にあります。そして、より多くのスマート コントラクトが作成および展開されるにつれて、それらを分析できること、さらにはそれらがどのように連携するかを分析できることがますます重要になります。

Synereo は、スマート コントラクトに対する数学的に厳密なアプローチを推進することを目的として設立されたため、この種の分析に適したツールを提供できます。 Synereo の言語専門家 Jack Pettersson 氏と CTO Greg Meredith 氏が発表した論文では、Synereo の Rholang スマート コントラクト言語では再入脆弱性が許容されないことを示す例を通じて、当社のアプローチが説明されています。
これは、ハッカーが DAO 資金を略奪することを可能にしたセキュリティギャップが、同等の Synereo 実装では決して発生しないことを意味します。すべてが自動化され、書き込みプロセス中にチェックされます。

Rholang は、スマート コントラクト内のきめ細かい同時実行性をサポートするために Synereo によって開発された言語です。セマンティクスは、ロー計算と呼ばれるモバイル処理計算から派生しています。そのため、Rholang コンパイラはモデル チェッカーと定理証明器を使用でき、これは同時分散イベント処理を使用して契約を検証および検証する場合に特に役立ちます。 Jack と Greg が言うように、Java や Scala などの最新のプログラミング言語で見られるような控えめな型宣言は、コンパイラ パイプラインをラップする Rholang などのモデル チェッカーのチェックになり、結果としてコンパイラ自体が実行時に悪意のあるコントラクトが存在するのを防ぎます。

詳細を検討する前に、契約開発を他の分野と比較すると役立ちます。電気技師の仕事について考えてみましょう。家庭に電気を供給することは、間違いなく極めて重要な仕事です。間違った配線を接続すると家が燃えてしまう可能性があります。電気技師が職人のように手作業で配線作業に取り組んでいた時代がありましたが、その作業の多くは極めて危険でした。現在、標準化された部品とベスト プラクティスにより、電気技師はよく理解された部品を使用してサービスに電力を分配できるだけでなく、チームで作業して大規模な建物に配線することもできます。

Rholang が採用したアプローチは、これに非常に似ています。契約、および契約内のさらに小さなロジック単位では、型を使用して、物事をまとめることが安全かどうかを示します。 Java、C#、またはその他の一般的な言語に精通しているプログラマーは、安全に使用できる命令を伴うプログラム命令をパーツか​​ら組み立てるこの方法に精通しているでしょう。唯一の新しい点は、Rholang のタイプでは、安全な使用を構成する要素についてより多くの情報を取得できることです。

どのように機能しますか?

Rholang では、開発者は契約の動作タイプを定義することで、作成するアプリケーションに受け入れられる契約を指定します。

行動タイプとは何ですか?これはプログラミングにおける新しい開発であり、コード自体だけでなく、コードの動作と構造に関するより多くの情報がより高いレベルでキャプチャされます。型定義は、コードが従わなければならない特定のルールと制約です。たとえば、契約を再度要求する前に、契約状態の更新を実行する必要があります。

これは事実上、攻撃者が The DAO で悪用した根本的な欠陥です。つまり、引き出しリクエストを処理するコントラクトは、更新を完了する前に繰り返しリクエストされていました。 Rholang などの並列環境では、コントラクトの更新と再入が競合し、コンパイラは型をチェックしてこの競合が安全かどうかを確認します。 Jack と Greg の記事では、コントラクト型は競合が安全ではないことを明示的に述べており、当然のことながら、コンパイラはコントラクト型に従わないコードを拒否します。 DAO の Solidity コントラクトでは、コントラクトに再入力するコード パスが単に競合するだけでなく、常に更新の完了をサポートするため、問題はさらに深刻です。

並列および分散コンピュータ操作についての推論は難しいことを私たちは心から認識しています。 Synereo が採用しているアプローチは、開発者の生活に支障をきたすことなく、開発者の生活を楽にしてくれるようです。コンパイル時の形式検証ツールを統合し、動作型を利用することで、次の 3 つの目標を達成できます。1. 開発者は、コード レベルと型レベルの 2 つのプログラム ビューを取得できます。 2. コンパイラ自体は、定義された型を通じて明示され、実際のコードではキャプチャされない意図を開発者に通知します。 3. 検証は開発プロセスの一部です。開発者は、コンパイラがコードの型チェックを行うことに非常に慣れています。

形式検証を最初から最後まで開発プロセスの一部として総合的に捉えると、他の利点もあります。たとえば、型を使用して設計するためのルールを生成し、DAO の脆弱性における本質的な問題に重点を置きます。この記事で見てきたように、型は契約の詳細の多くを抽象化し、同時実行性と非決定性が許可される場所と許可されない場所に焦点を当てます。 Synereo のアプローチのこれらの利点やその他の利点により、完全に分散化されたアプリケーションとプロトコルをシンプルかつ簡単に作成できます。

要約する

適切なツールが正しく使用された場合にのみ、分散型経済が実現し、暗号通貨運動以外の人々にとって意味のあるものになり始めることが期待できます。

経済やその他の分野におけるミッションクリティカルな分散型アプリケーションでは、形式検証が一般的な慣行になる必要があります。さらに、Synereo の評判メカニズムは、人々が引き続き参加していることを保証し、最もよく書かれた、最も洗練された契約でさえ予測できないエッジケースの健全性チェックを提供します。

イーサリアムとの対話は、エコシステム全体にとって非常に生産的であり続けると信じています。私たち全員が、各同僚が持ち寄るさまざまな専門知識から恩恵を受けることができます。 Synereo は、安全でスケーラブルな分散型契約とアプリケーションを作成するための優れたプラットフォームであると信じており、これらのツールをできるだけ早く開発者コミュニティに提供することに尽力しています。

（注：この記事の著者はSynereoのCEO、Dor Konforty氏です）