9月5日、Odailyが主催し、36Kr Group Strategyが共催したPOD Conference Security Forumで、Cheetah Blockchain Research Centerのセキュリティ専門家Yang Wenyu氏が「スマートコントラクト自動監査技術」と題した講演を行った。

Yang Wenyu氏はスマートコントラクト開発の現状を紹介した。ブロックチェーンは現在寒い冬の時期にあると多くの人が考えていますが、チーターブロックチェーン研究センターの統計によると、先月の新しいスマートコントラクトの数は1日あたり1317でした。研究センターに含まれるプロジェクトのうち、ブロックチェーン インフラストラクチャが 9.38%、ゲームと VR が 4.44%、商業と小売が 3.6%、ソーシャル メディアと通信が 3.4% を占めています。

その数は着実に増加していますが、スマートコントラクトはセキュリティの問題にも直面しています。 2017年から2018年6月にかけて、スマートコントラクトの脆弱性が頻繁に発生し、多額の経済的損失を引き起こしたほか、ブロックチェーンやスマートコントラクトの一部の開発者やユーザーにスマートコントラクトの安全性に疑問を抱かせ、イーサリアムに続くイーサリアムの開発も妨げられました。の開発。

また、Fomo3Dが台頭していた頃は、2日目だけで偽造契約書が大量に出現しました。模倣した Fomo3D ゲーム開発者が積極的な配布のロジックを変更したため、投資資金のほとんどが模倣契約開発者に流れ、これも DApps の開発を妨げています。

この文脈において、大規模なスマートコントラクトのセキュリティを効果的に保証するにはどうすればよいでしょうか? Yang Wenyu 氏は、手動監査の複雑さを軽減し、スマート コントラクトを使用して監査を自動化することが最善の方法であると考えています。

具体的には、自動監査方法は次の 3 つの主要なカテゴリに分類されます。

• 1つ目は機能コードマッチングです。これは、悪意のあるコードを抽出および抽象化し、検出対象のソースコードを検出するためのマッチングモジュールを形成します。利点は速度が速く、新しい脆弱性への迅速な対応ですが、欠点は使用範囲が限られていることと偽陰性率が高いことです。
  

• 2 つ目は、正式な検証に基づく自動監査方法です。これは 2016 年に平井氏によって初めて提供され、グリシチェンコ氏とヒルデンブラント氏の後に改良され、F* フレームワークと K フレームワークを使用して EVM を形式モデルに変換しました。 Formal は航空宇宙分野で一般的な形式検証フレームワークであり、K フレームワークは意味変換フレームワークです。
  

• 後者は、現在最も一般的に使用されている方法で、監査を自動化するためのシンボリック実行とシンボリック抽象化に基づいています。スマートコントラクトを分析する場合、ソースコードをコンパイルしてEVM OPCODEを形成し、自動分析エンジンに入力してCFGに変換し、これら2つの方法を使用して分析できます。代表的なものとしては、偽陽性率や偽陰性率を低減できる Oyente や Securify システムがありますが、分析方法が煩雑で時間がかかります。
  

しかし、Yang Wenyu氏は、現在の自動監査手法は非常に未熟な段階にあり、主に3つの大きな問題に直面していると指摘した。それは、高い誤報率、自動化の程度が低い、手動による二次監査への依存、監査時間が比較的長いというものだ。

以下は楊文宇氏のスピーチの全文です。お楽しみください。

皆さん、ありがとうございます。今日はこのカンファレンスに参加できて大変光栄です。今日の私の講演のテーマは、現在のスマートコントラクトの自動化セキュリティ検出技術を分析することです。今日の私の講演は 2 つの部分に分かれています。最初に、前編ではイーサリアムにおけるスマートコントラクト開発の現状を見てみましょう、後編ではこの現状を踏まえた上で、スマートコントラクトの自動化に関わるいくつかの手法について詳しく説明します。

まず、スマートコントラクト開発の現状を見てみましょう。当社のプラットフォームによると、過去 1 か月間、スマートコントラクトの数が 1 日あたり平均 1317 の増加率で着実に増加していることがわかります。これは私たちの理解と一致しているかもしれません。ブロックチェーンは現在寒い冬の時期にあるため、成長率は比較的安定しています。第二に、NLT 手法を使用してスマート コントラクトの分野を分割しており、一部の機密分野を除いて、スマート コントラクトは現在、インフラストラクチャ、商業小売、ゲーム、ソーシャル メディア、通信で広く使用されています。これがスマート コントラクトの現状です。現在、スマート コントラクトのセキュリティ状況はどうなっていますか。おそらくゲスト 2 人がすでに詳細に説明していると思います。2017 年から 2018 年 6 月まで、この種のスマート コントラクトの脆弱性が頻繁に発生しました。そのたびに、これは多額の経済的損失をもたらすだけでなく、一部の開発者やブロックチェーン、さらにはスマートコントラクトのユーザーにスマートコントラクトのセキュリティについて強い疑念を抱かせ、これもイーサリアムの開発を妨げます。

さらに、先ほどゲストが Fomo3D について言及したこともわかりますが、基本的なスマート コントラクトのセキュリティに加えて、現在ではセキュリティが非常に注目されています。この種のゲームでは、開発者が実際にアクティブ割り当てのロジックを変更したため、ハニカム ゲームをプレイする過程で、投資資金のほとんどがコピーキャット契約の開発者に流れ、それがゲームの開発にも貢献しました。 DApp.に支障をきたします。

現在、私たちは大規模なスマート コントラクトのセキュリティを効果的に確保する方法という問題に直面しています。これは今日議論する問題でもあります。第 2 部では、現在のスマート コントラクト自動化監査テクノロジーの開発について共有したいと思います。

振り返ってみると、昨日正午現在、イーサリアムには合計193万件のスマートコントラクトが存在し、日々の増加率は順調に増加しており、監査方法には手動監査と自動監査が含まれています。大規模なスマート コントラクトの中で、私たちの最善の方法は、手動監査の複雑さを軽減して、自動監査を通じてより多くのことを実行できるようにすることです。自動監査は 3 つの部分に分かれています。まず、最初のタイプは機能コード照合、2 番目のタイプは状況検証に基づくサブデューティ監査方法、最後のタイプはシンボリック実行とシンボリック抽象化に基づく自動監査です。

まず特徴コードマッチングについて見てみましょう 名前からも明らかですが、悪意のあるコードを抽出・抽象化するものです 静的なオリジナルコードと一致するセマンティックマッチです 監査方式の利点は明らかです、例えば、非常に高速ですソース コードで文字列の一致を実行すると、2 人目はすぐに新しい脆弱性を見つけることができるため、高速です。監査で新しい脆弱性が発生した場合、新しい一致パターンをいくつかすぐに提出できます。 「その欠点は何ですか? もう一度見てみましょう。現在のブロックチェーンはオープンで透明であるべきだと理解していますが、実際の状況はそうではありません。おそらく統計をとったのです。現在のコードオープン率は 48.62% に過ぎません。」つまり、イーサリアムでは、コントラクトの半分以上が実際にはオープンソースではなく、コードのみが公開されています。先ほどゲストは、コードを確立するのにも多大な労力を費やしたと言いました。この制限が使用範囲につながります。この方法は限定的ですが、アプリ検出などの従来の静的監査方法では、ライブラリ内のいくつかの固有の関数を呼び出して監査しますが、スマート コントラクトの一部の関数や機能はより可変であるため、脆弱性の割合が比較的高くなります。

2 番目の方法, 形式的検証に基づく一般的な自動監査について説明します. 形式的検証監査スマート コントラクト セキュリティは 2016 年に平井によって初めて提供されました. 論理対話型証明者, イザベルデ レム言語 -> 形式モデル, 形式モデル検証を通じて,コードロジックに問題があるかどうかを判断し、この作業の最後の 2 つは形式面をさらに改革し、比較的非効率な変換方法である Lem 言語を放棄しました。F* フレームワークと K フレームワークを使用して EVM をFormal モデル、Formal は航空宇宙分野で形式的な検証を行うことが多いフレームワーク、K フレームワークはセマンティック変換フレームワークです。これら 2 つの代表的な技術研究について、より深く理解したい場合は、以下の論文。

3 番目のポイントは、今日は皆さんとのコミュニケーションに焦点を当てたいと思いますが、最も一般的に使用される手法には、シンボリック実行とシンボリック抽象化に基づく自動監査があります。この自動監査について見てみましょう。スマート コントラクトを分析するとき、まずオブジェクトが何であるかを明確に分析する必要があります。機能一致コードについて説明したように、EVM 上のスマート コントラクト コードのほとんどが公開されていないことがわかっています。次に、オブジェクトを分析して、それが EVM OPCODE であることを確認します。いくつかのソース コードを渡した後、コンパイルして EVM OPCODE を形成し、自動分析エンジンに入力します。このシンボリック実行とシンボリック抽象化による自動監査フレームワークにはいくつかの共通点があり、OPCODEはエンジンに入力されると一つずつ制御フローチャートであるCFGに変換され、このCFGを通じて簡単に理解することができます。この CFG とはどういう意味ですか? CFG は、コントラクト コード内のロジックを高速なものにパッケージ化することです。内部のロジックがフォークされると、左側のコントラクトは非常に大きく完全な CFD を形成するため、プログラマーはよりよく理解して実行できます。いくつかのロジック。

CFG の生成後、現在 2 つの分析手法があります。1 つはシンボリック実行に基づく検証です。このタイプがより代表的です。誰もがよく知っている Mythril、Oyente、Maian です。公開されているシンボリック抽象分析手法は Securify です今日は、Oyente と Securify という 2 つのシステムの具体的なアーキテクチャと実装方法について主に説明します。まず、Oyente を見てみましょう。Oyente のロジックは左から見ることができます。CFG では、アプリケーションの後、最初はエクスプローラーです, コード内の各処理を検証して形式的検証を行います。このように、X があるかどうかを検証します。これにより、X が C1、C2、C3 の条件を満たすだけでなく、この時点で判定できます。状態が no であるか、yes であるかを確認して、ロジック全体の流れを確認します。 2 番目のコア分析は、実際には Oyente の最もコアな部分です。出力されたばかりのエクスプローラー パスを変換し、一部の脆弱性検証のみを実行します。現時点では、TOD、タイムスタンプ依存関係、および誤った例外の処理、これら 3 つの検証のみを提供します。最終的に、これはシステムは、偽陽性と偽陰性の率を保証できます。マイクロソフトのオープンソース検証ツールを使用して、アーキテクチャ全体をカプセル化します。先ほど説明したプロセスでは、CFG からエクスプローラー検証への検証が必要な場合があることも理解する必要があります。毎回検証となるため、この分析方法は特に時間がかかり、成功しない可能性があります。ここがオイエンテが現在大きな問題を抱えているところだ。

この問題に基づいて、Securify と同様に、彼らは別の方法を提供しています. 彼らは、現在のコントラクト コードが実際には特に分離しやすいと信じています. 従来のコードとは異なり、いくつかの比較的固定された形式のコントラクト コードなど、結合は特に高いです。コントラクト ロジック全体の検査を行う必要はありません。コントラクトのデカップリングの各モジュールを分析して、自動化の程度を向上させます。左の図は検証プロセス全体を示しています。コントラクトのバイトコードはドメイン言語を介して渡されます。は、特に前述のパターン マッチングと同様、一部の脆弱性を検証言語のパターン マッチング フレームワークに変換し、セマンティクスがこれと互換性があるかどうかを検証する検証モジュールです。最後にレポートも提供され、この自動監査方法により、最終的にウォレットを出力できる管理者を変更することができます。

より具体的なポイントは、セマンティック分析をどのように行うかです。実際、このエクスプローラー コードの分析は 2 つの次元から行われます。1 つ目はロジック、2 つ目はデータです。論理メソッドは 2 種類のロジックを定義します。1 つ目は MayFollow と呼ばれます、2 番目は MustFollow と呼ばれ、MayFollow は L2 に L1 に続くパスが必要であることを意味し、MustFollow は L2 のすべてのパスが L1 に従う必要があることを意味します。これら 2 つの違いは、ロジック フレームワーク全体を定義します。

2 つ目はデータです。契約でのデータ変更の定義には 3 つのタイプがあります。最初の MayDepOn は 2 つの要素で、1 つは Y と呼ばれ、もう 1 つは T と呼ばれます。T が変更されると、Y は変更される場合と変更されない場合があります。 2 番目は Eq、つまり Y は T によって決定されます。 3 つ目は DetBy です。Y と T は 1 対 1 に対応しており、T が Y に変化する限り、必ず変化します。ここでより鮮明に想像できます。実際、Maydepon は T 変数のようなものです。時間、ある期間内、Y は値、T は変化する、Y は変化しない可能性があります。3 番目は 1 対 1 の関係です。ハッシュを計算するのと同じように、T を変更する限り、Y は変化する必要があります。ロジックとデータの 2 つの次元を通じて、検証を実施しました。最終検証モジュールでは、現在、約 6 ～ 7 のスマート コントラクト脆弱性検証言語が提供されています。これらはすべてプラグインで記述されており、他のセキュリティ開発者は引き続き検証を強化できます。脆弱性の言語。

最終的に、自動監査を評価するときは、自動化の程度、誤検知率、誤検知率からこの問題を提供する必要があります。データをバインドできることがわかり、検出されたデータがシンボリック実行とシンボリック抽象化の 2 つの自動監査方法により、この作業は非常に煩雑ですが、この方法により誤検知率を減らすことができます。

最後に復習すると、現在、機能コード照合、形式検証、シンボリック実行、シンボリック抽象化の 3 種類の自動監査方法があります。分析プロセス全体を振り返ると、現在の自動監査手法は非常に未熟な段階にあり、主に 3 つの大きな問題に直面していることが明確にわかります。 . . 2 つ目は自動化の程度が比較的低く、継続的に監査する必要があること、3 つ目は監査時間が比較的長いことです。

最後は分析全体の見直しです。まずはスマートコントラクトの開発状況を明らかにし、自動監査手法をテストしてみましょう。技術交流グループが左右にあります。興味のあるお子様はぜひご参加ください。より詳細なディスカッションを一緒に行います。これが私が今日行っていることです。コンテンツを共有していただきありがとうございます。