最近ではChatGPTが人気で、サービス開始からわずか2ヶ月でアクティブユーザー数が1億人を突破しました。これを使って記事を書いたり、コードを書いたり、恋をしたり、仕事を見つけたり、電子メールに返信したりすることは日常的な操作になっています。このソフトウェアを使ってインターネット上で「お金を稼ぐ」方法を教える方法はたくさんあります。ペンシルベニア大学ウォートン経営大学院は、「学生ChatGPTが経営管理試験に合格した」と主張した。

その結果、ある仕事が人工知能に置き換わったり、人間が人工知能に置き換わったりすることが話題になり、誰もが囚われの時代、誰もが少しずつ心臓を高鳴らせている。

それでは、人工知能、あるいは形式的検証などの「コンピューター製品」は人間に取って代わることができるのでしょうか？ Web3.0 の世界では、正式な検証が手動レビューに取って代わることができるでしょうか?

正式な検証

形式的検証は、コンピュータ プログラムが期待どおりに動作することを検証するための数学的証明方法です。プログラムの特性と期待される動作を数式として表現し、自動ツールを使用してこれらの数式が成り立つかどうかを確認します。このプロセスは、プログラムが期待に応えられるようにするのに役立ちます。

正式な検証の申請

形式的検証は、次のようなさまざまなシステムで広く使用できるツールです。

• コンピューターのハードウェア設計: 集積回路とデジタル システムが必要な仕様を満たし、正しく動作することを保証します。

• ソフトウェア エンジニアリング: 特に航空、医療機器、金融システムなどのミッション クリティカルなアプリケーション/ドメインにおけるソフトウェア システムの正確性と信頼性を検証します。

• ネットワーク セキュリティ: 暗号化アルゴリズムとプロトコルのセキュリティを評価し、セキュリティに敏感なシステムのセキュリティ ギャップを特定します。

• AI と機械学習: AI および ML モデルのプロパティと動作を検証して、期待どおりに動作し、正確な予測ができることを確認します。

• 自動定理証明: 数学、物理学、コンピューター サイエンスの分野で適用される、数学的定理の検証と数学的予想の証明。

• ブロックチェーンとスマート コントラクト: ブロックチェーン システムとスマート コントラクトの正確性、セキュリティ、信頼性を確保します。

スマートコントラクトの正式な検証

スマートコントラクトの正式な検証とは、スマートコントラクトのロジックや期待される動作を数式で表現し、自動ツールを使用してその数式が正しいかどうかを確認することです。

このプロセスには以下が含まれます。

• 契約の仕様とプロパティは形式言語で定義されます。

• 契約書のコードを翻訳する"」を数理論理学やモデルなどの形式的な表現に変換します。

• 自動化された定理証明器またはモデル チェッカーを使用して、コントラクトの仕様とプロパティが保持されていることを検証します。

• 検証プロセスを繰り返して、エラーや期待からの逸脱を見つけて修正します。

場合によっては、自動化された定理証明器やモデル チェッカーがプロパティを証明または反証できないことがあります。この場合、仕様と必要なプロパティを調整し、検証プロセスを繰り返すことが必要になる場合があります。

仕様を小さなコードに分割するか、より多くの仕様情報を提供することで、仕様とその期待されるプロパティを改良することができます。これにより、定理証明者やモデルチェッカーが仕様とプロパティが保持されていることを簡単に検証できるようになります。

正式検証は、1 つの契約に適用することも、複数の契約に同時に適用することもできます。 Web3.0 プロジェクトでは複数のコントラクトが使用されることが多く、これらのコントラクトが連携して機能し、目的のプロジェクト機能を正しく実装していることを確認することが重要です。

正式な検証では、この数学的手法を使用すると、スマート コントラクトのプロパティが数学的に正しいことが厳密に証明されているため、スマート コントラクトにバグ、バグ、その他の予期しない動作がないことを確認するのに役立ちます。

コードを形式化する

コードスニペットの例 1

次のコードは、簡略化されたトークン転送関数プログラムを示しています。 2 人のユーザーがおり、それぞれがいくつかのトークン (残高と残高 2) を持っています。 transferFromUser 1 関数は、User 1 から User 2 にトークンを転送します。このプログラムには、トークンの総供給量が常に残高の合計に等しいという不変条件があります。

コードスニペット 1: トークン転送プログラム

不変量を数式で表し、数式に番号を付けます。数式では、「=」は代入ではなく「等しい」を意味します。

コードスニペットの例 2

次のコードは、論理式を追加する方法を示しています (例を簡単かつ明確にするために、整数のオーバーフローは無視されています)。

コードスニペット 2: コードの意味を表す論理式関数

transferFromUser 1 がプログラム内で不変式を保持していることを確認したい場合は、式 7 (関数の最後) で不変式 (式 1) を確認できます。以下は、高校の代数学の方法を使用した証明です。

正式な検証と手動監査の連携

スマートコントラクトのセキュリティ確保という点では、正式な検証と手動監査は相互に補完し合うものと言えます。

正式な検証:

正式な検証は、契約のロジックと動作、およびその期待されるプロパティをチェックする体系的かつ自動化された方法を提供し、潜在的なバグや脆弱性の特定と修正を容易にします。手動検査では検出が難しい複雑な問題や微妙な問題を検出するのに非常に効果的です。

複雑な契約や複数の契約を扱う場合、人間がチェックする必要のあるすべての組み合わせや可能性について推論することは困難ですが、機械には「プレッシャーがありません」。

手動監査:

人間による監査により、契約コード、設計、展開を専門家がレビューできます。監査専門家は、経験と専門知識を活用して、潜在的なセキュリティ リスクを特定し、契約の全体的なセキュリティ状況を評価できます。

これに加えて、人間は正式な検証プロセスが正しく実行されたことを検証し、自動ツールでは検出できない問題をチェックすることもできます。したがって、正式な検証で使用される仕様と必須プロパティの正確性を確認するには、人間の専門家による監査の方がより役立ちます。

要約すると、正式な検証と手動監査の 2 つの方法を組み合わせることによってのみ、スマート コントラクトのセキュリティの包括的かつ徹底的な評価を実行でき、発見とバグ修正の可能性が高まります。これは人間と機械の長所を組み合わせたセキュリティへのアプローチでもあり、「多層防御」と呼ばれます。

セキュリティエキスパートオンラインAMA

正式な検証の力を過小評価することはできませんが、手動監査の重要性を無視することはできません。 ChatGPT の公式ウェブサイトでは、自身の欠点を認めており、人工知能は人間の思考や創造に取って代わることはできないというありきたりな議論もここで 10,000 語省略することができます...いいえ、Bard はミスを犯し、Google の株価は急落しました。

同様に、正式な検証は手動監査に代わることはできず、この 2 つは相互に補完してスマート コントラクトの完全な検査を実施します。

記事を読んだ後に質問がありますか? [日本 2 月 10 日(金)] の [CertiK Twitter AMA] にゲストとして参加し、専門家とオンラインで 1 対 1 の Q&A をしてみませんか。時差ぼけで参加できないお友達はバックグラウンドでメッセージを残していただければ、ゲストに代わってメッセージを伝え、AMAリプレイの内容を公開します！