ブロックチェーンという言葉は、最先端の技術コンセプトから市場のホットワード、過剰消費の象徴まで、近年何度か浮き沈みを経験してきました。ブロックチェーンは多くの業界の問題点を解決するツールであり、次世代の「スーパービジネスキャリア」誕生の起爆剤となる可能性を秘めていると多くの人が信じています。

しかし、伝説的な壮大な変化はまだ到来しておらず、注目が集まっています。興味のある人はそこから利益を得ますし、利益を求める人はやみくもにお金を払います。世論の渦に早すぎると、成長段階のテクノロジーに悪影響を与え、試されることになります。

現在、上陸申請は非常に少なく、テクノロジーと業界の結びつきには依然として距離があり、テクノロジーと業界を本当に気にかけている「バックボーンの声」が投機筋の喧騒に影を落としているのが現状です。 Odaily は、トップの新しいビジネス メディア 36Kr、トップのテクノロジー リーダー、学術エリートと協力して、規制を受け入れる方法、業界のカスを取り除いて本質を抽出する方法、トラフィックと声を真剣に取り組む人々に引き渡す方法について話し合います。そしてブロックチェーンを力強く着陸させましょう。

9月5日、Odailyが主催し、36Kr Group Strategyが共催したブロックチェーンPODカンファレンスで、CertiKのチーフサイエンティストであるVilhelm Sjöberg氏が「完全に信頼できるスマートコントラクトとブロックチェーンエコシステムの構築に向けて」と題した講演を行った。

副題

以下は、CertiK の主任研究員である Vilhelm Sjöberg 氏の講演の書き起こしです。

皆さん、こんにちは。私は CertiK の主任研究員で、ブロックチェーンに関する多くの研究活動を行ってきました。ブロックチェーンはデータベースであり、技術や信頼の観点から重要な研究テーマが数多くあります。プログラムは実行中にエラーを起こしやすいのですが、なぜ実行中にミスが繰り返されるのでしょうか?プログラムの信頼性を高めるにはどうすればよいでしょうか?もちろん、それは人々がプログラミングが苦手なわけではなく、スマート コントラクトがブロックチェーンの非常に特別で重要な部分であるためです。ブロックチェーン上では、スマートコントラクトは一度デプロイされると更新することができないため、デプロイされたスマートコントラクト自体に抜け穴がある場合、ハッカーがその抜け穴を見つけて悪用し、資産を盗む可能性があります。これらの問題は私たちが避けなければならないものです。

プログラムの安全性を確保するために、一部は手動でレビューされますが、時間的コストが比較的高く、他の問題を引き起こす可能性があります。もちろん、監査用の自動テストもありますが、すべての問題を見つけるのに役立つわけではありません。したがって、ブロックチェーンにとって、これらのソリューションはまだ十分ではありません。

CertiK は数学的手法を使用してプログラムを証明します。つまり、正式な検証を通じてスマート コントラクトとブロックチェーン アプリケーションにセキュリティ サービスを提供します。当社のコンカレント オペレーティング システム カーネルである CertiKOS は完全に正式に証明されており、その背後にある主要なテクノロジは「ディープスペック」です。

複雑なシステムの場合、CertiK は詳細な仕様技術を利用して安全認証を取得します。私たちは複雑なシステムを階層化し、各抽象層が何を書き、何を行い、どのような操作を実行するかを理解し、それが正しい仕様を満たしているかどうかを証明します。抽象化レイヤーを作成すれば、それをまとめて検証できます。抽象化レイヤーは相互にリンクできるため、プルーフを統合できます。これが私たちの主な作業です。階層化と統合を通じて完全な分散型スマート コントラクトの検証を実現することです。

オペレーティング プログラム CertiKOS のカーネルはいくつかの層に分割されており、一度に 1 つの複雑な関数を処理するため、大規模で複雑なプログラムを検証することが可能です。

この図は、Landshark マシンにオペレーティング システム CertiKOS を展開したことを示しています。

私たちは学界の多くの専門家とも協力しており、このようなプロジェクトの開発に協力していただいています。 2015年、Gu Ronghui教授とShao Zhong教授は「ディープスペック」という概念を提案し、検証しました。 2016 年に、私たちはすでにこのすぐに使える製品とサービスを企業向けに販売していました。 2017 年に、スマート コントラクトを検証するために CertiK を拡張しました。したがって、学術研究も行うことができ、ブロックチェーンの正式な検証も行うことができます。

次に、私たちが実施している進行中の研究プロジェクトである、スマートコントラクトを検証するためのプログラミング言語である DeepSEA について詳しく紹介します。

その前に、理解を助けるために正式な検証とは何かについて説明しましょう。正式な検証には、浅い検証や深い検証など、さまざまな検証手法が含まれます。

浅いレベルの検証とは、スマート コントラクトの非常に一般的な整数オーバーフロー問題など、いくつかの一般的な検証を指します。比較的浅い検証のために、当社は第 1 世代の高性能スマート コントラクト自動検出エンジン CertiK AutoScanEngine (CASE) を設計しました。これは、スマート コントラクトを自動的にスキャンして脆弱性を特定するのに役立ちます。分散検証は、コントラクトをさまざまなモジュールに細分化することで完了します。ユーザーはコントラクトを検証エンジンにアップロードして、特定のメソッドを呼び出すときにどれが正しいか、またはエラーが発生した場合の対処方法を確認できます。プロセス全体で、人手にほとんど依存せずに最大限の機械検証が実現されます。

次に、深層検証についてお話したいと思います。たとえば、価値のある属性を検証する必要があり、それを証明する方法を考えなければなりません。特定のアーキテクチャまたは特定のメソッドに適用されるローカル プロパティがいくつかあります。しかし、詳細な検証は、すべてのスマートコントラクトのエコシステム全体に適用できます。ホワイトペーパーで説明されているように、ブロックチェーン エコシステム全体にセキュリティを提供することを目的として、一部の決済システム、オンチェーン、オフチェーンなどを含むさまざまなチェーンを統合および組み合わせることができます。

場合によっては、完全に機械に依存するだけでなく、人間の介入に依存することもあります。たとえば、複雑なシステムの場合は、マニュアルに仕様を記述する必要があります。CertiK では、各システムを異なるレイヤーに分割できます。したがって、このようなプロジェクトは、詳細な検証と仕様のシステムを作成するのに役立ちます。この目的のために、私たちは独自の言語 DeepSEA を開発しました。契約書を書きたいだけであれば、パーソナライズされた言語で書くことができます。ただし、一部の高信頼契約では、他の側面でそれほど高い信頼が得られない場合があります。もちろん、EVM の言語で記述することもできますが、あまり信頼できるコードではありません。そこで私たちは、もともと CertiK を記述するために開発された CertiK の言語 DeepSEA を立ち上げましたが、今では Ethereum コントラクトにもマッピングできるようになりました。仕様を生成できることに加えて、実績のあるコンパイラーを使用することもできます。

ブロックチェーンには、私たちが行うすべてが正しいことを確認するための契約があります。したがって、これは私たちが深いレベルで検証を行っている手順のいくつかを示す非常に良いデモンストレーションでもあると思います。さらに深く掘り下げると、契約が正しく良好な状態にあることを確認するために実行する必要のある手順がいくつかあります。したがって、この概念を明文化することができ、このような一連の手順を経て、最終的に契約の正確性を確保することができます。

他にもオンラインでご覧いただけるプロジェクトがあります。拡張できる決済関連のプロジェクトがいくつかあります。スマート コントラクト、コンパイラー、EVM モデルに関連するプロジェクトもあります。下記の分野でお手伝いさせていただきます。ご興味がございましたら、パートナーとしてご参加いただき、引き続きご連絡ください。皆さん、ありがとうございました！