!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-5522147c3d-dd1a6f-6d2ef1)### / Web3 完全なソフトウェア スタックの高度な形式検証 /CertiK は最近、Cosmos SDK Bank モジュールに関する高度な正式検証レポートを公開しました。これは、私たちの知る限り、Cosmos SDK の正式検証に成功した最初の試みです。形式的検証は、数学的論理を使用してシステムが仕様に準拠し、考えられるすべての入力および条件下で期待どおりに動作することを確認する手法です。この記事では、Cosmos SDK Bankモジュールを正式に検証する具体的な手順と検証結果を紹介します。### Cosmos SDK とは何ですか?Cosmos Software Development Kit (略称 SDK) は、開発者がカスタム ブロックチェーン アプリケーションを構築できるようにするフレームワークです。 Cosmos SDK を使用すると、開発者はコンセンサス層からアプリケーション層までの設計や実装について心配することなく、独自のレイヤー 1 ブロックチェーンを簡単に起動できます。 Cosmos SDK は、ステーキング、認証、gov、mint モジュールなど、直接インポートして任意のチェーンで使用できる標準コア モジュールを提供します。!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-ffb0951d40-dd1a6f-6d2ef1)ソース：### バンクモジュールCosmos SDK の Bank モジュールは、ネイティブ トークンの転送など、トークン管理に関連するすべての機能を担当します。トークンを送信するには、ステーキングされているもの、ロックされているもの、または結合解除されているものを除く、アカウント内に十分な利用可能なトークンがあることなど、多くの制限や条件を満たす必要があります。ステーキングや認証などのモジュールのサポートにより、銀行モジュールはトークン送信のプロセス全体を管理します。銀行モジュールは他のいくつかのモジュールに依存していますが、それらはこの正式な検証の範囲外であるため、プロセスを簡素化するためにそれらの機能についていくつかの仮定を置きます。SDK のバンク モジュールは、モジュールの動作とデータ型を定義するコア コンポーネントであるキーパーとタイプを含むいくつかのサブモジュールで構成されます。モジュールの主な機能と特徴を説明するため、キーパー サブモジュールに焦点を当てます。keeper サブモジュールには、表示と送信という 2 つの主要なコンポーネントがあります。ビューキーパーはアカウントと残高の管理を担当し、送信キーパーはロックまたはロック解除されたトークンの転送やステーキングなど、アカウント残高の変更を担当します。バンクモジュールの流れを下図に示します。矢印はコンポーネントから関数または Keeper への方向を示しています。!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-5140a25ef1-dd1a6f-6d2ef1)ソース：＃＃＃ 認証方法前述したように、この検証の範囲はバンク モジュールに限定されます。検証を開始する前に、まずバンク モジュール内のデータ型の正式な仕様を策定します。たとえば、bank モジュールにはトークン データ構造があり、文字列型の単位と big.Int 型の量が含まれており、ソース コードでは次のように定義されています。!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-1c78ef9fa4-dd1a6f-6d2ef1)構造は単純で、Coq (モデリングおよび形式検証言語) で次のように定義します。!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-34f7c3dbba-dd1a6f-6d2ef1)この定義に基づいて、銀行モジュールの機能的完全性の基礎を築くために、まずコインの基本操作に関するいくつかの特性を証明します。これは、コイン タイプの頻繁な変更と操作が必要なためです。例えば：!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-26a5df4754-dd1a6f-6d2ef1)この補題は基本的な不変性を証明します。つまり、2 枚のコインを差し引いても、その額面は変更されず、残高がマイナスになることもありません。前の例と同様に、各状態遷移の基礎となるコンポーネントは Coq でモデル化されます。これらのコンポーネントには、KV ストア、ガスメーター、エラー処理、コンテキストが含まれます。データ型の詳細な仕様とその検証については、以下を参照してください。### キーパーのモデルを作成する基本コンポーネントのモデリングが完了したら、バンク モジュールのコア キーパーをモデル化して、モジュールの機能を記述することができます。バンクキーパーには 2 つのインターフェイスがあり、1 つはトークン データへの読み取り専用アクセス用で、もう 1 つはトークンの転送と供給メンテナンス用です。View keeper は、アカウント残高への読み取り専用アクセスを処理する責任があり、アカウント残高を計算するための 4 つの関数が含まれています。1. GetBalance: 住所ごとに特定の額面の口座残高を照会します。ここでは、ヌル バイトのシーケンスとヌル以外のバイトのシーケンスの 2 つのケースを考慮します。正式な検証により、GetBalance 関数がどちらの場合でも正しい結果を生成することが保証されます。2. LockedCoins: アドレスに対応するアカウント内のすべての非使用トークンを返します。時間の制約のため、認証モジュールからのいくつかの実装について仮定を立てました。3. GetAllBalances: 指定されたアドレスにあるすべての口座残高を返します。4. GetAccountsBalances: BAddress フィールドと BCoins フィールドをレコードとして、ストレージからすべてのアカウント残高を返します。!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-0600aa9388-dd1a6f-6d2ef1)送信マネージャーはトークンの転送と供給を処理します。転送プロセス中はトークンの供給が維持されるため、新しいトークンが鋳造されることはありません。1. SetBalance: アドレスを通じてアカウントのトークン残高を設定します。この関数は、残高をゼロに設定した場合と残高をゼロ以外に設定した場合の 2 つのケースを考慮します。どちらの場合も、SetBalance の正しさが証明されます。2. subUnlockedCoin: アドレスから指定された量 (トークン) を差し引きます。再帰関数 subUnlockedCoins は、トークンのセットに対して同じことを行います。これらの関数の関連するプロパティは、公理的な仮定として扱われます。3. addCoin: 指定された量 (トークン) をアドレスに追加します。再帰関数 addCoins は、コインのセットに対して同じ操作を実行します。これらの関数の関連する特性は、公理的な仮定とみなされます。4. SendCoins: あるアカウント アドレスから別のアカウント アドレスに送金すると、両方のアドレスのゴールドが更新されます。受信者が存在しない場合は、その受信者用に新しいアカウントが作成されます。上記のコア コンポーネントのモデルを使用して、検証を開始できます。### 検証プロセス私たちの検証は、主に「View Keeper」と「Send Keeper」のコア機能に焦点を当て、これらの関数の不変特性を形式的に記述し、補助的な証明システムで証明することによって行われます。たとえば、仕様と補題 setBalance\_ok は、BaseSendKeeper モジュールの setBalance 関数の正しさを証明し、特に次のプロパティを証明します。1. send.setBalance が "Ok" 状態に戻ると、newMultiStore が存在しますが、このとき、更新された環境 uctx は、newMultiStore を更新することによって、元の古い環境 ctx から派生します。2. 設定されている残高は有効なトークンです (システム内のトークンに必要なプロパティを備えています)。3. setBalance\_prop の関係は、関数が期待どおりに newMultiStore の残高を更新し、更新された環境 uctx を生成するように維持されます。4. 残高設定が完了したら、口座アドレス addr と額面残高 (Denom) を使用して、更新された環境 uctx 上で view.GetBalance を呼び出すと、send.setBalance で設定したのと同じ残高が返されます。これらのプロパティは、Coq 仕様言語で次のように説明されます。!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-fa94a64bc4-dd1a6f-6d2ef1)他のプロパティの Coq コードについては、以下を参照してください。### 将来のキャリアこの検証の基礎は、いくつかの仮定と公理に基づいて構築されており、検証の範囲を拡大するためにより深く検証できます。今後の作業の優先事項には次の分野が含まれます。1. 仮定の検証: 現在の検証は、証明の基礎として一連の仮定に依存しています。これらの仮定は、システムの意図された動作と特性を正確に反映していることを確認するために、将来テストすることができます。2. 認証モジュールの検証: このモジュールはアカウント データと署名メカニズムの管理を担当し、Cosmos SDK のコア コンポーネントです。将来的には、モジュールの実装と他のモジュールとの相互作用が正確であることを確認するために完全に正式に検証される可能性があります。3. コインの委任、鋳造、販売に関する定理の追加: 検証範囲を拡大し、コインの委任、鋳造、販売に関する定理をさらに導入することで、システムの動作メカニズムをより包括的に理解するのに役立ちます。これらの定理を認証モジュールの検証と組み合わせて、システム全体の一貫性と正確性を保証できます。4. Cosmos SDK インフラストラクチャ全体を拡張する: 現在の検証作業は、主に銀行モジュールとその関連コンポーネントに焦点を当てています。将来的には、正式な検証プロセスを Cosmos SDK インフラストラクチャ全体に拡張することで、プラットフォームの全体的な精度、セキュリティ、安定性が向上し、開発者とユーザーにより安定した信頼性の高い環境を提供できるようになります。5. 他のモジュールとの統合: Cosmos SDK には相互接続されたさまざまなモジュールが含まれているため、それらの間の相互作用や依存関係を調査することは非常に有益です。これには、モジュール間の相互作用が正しいことを検証し、1 つのモジュールへの変更が他のモジュールに悪影響を及ぼさないことを確認する必要があります。6. インセンティブ メカニズムのモデリングと検証: Cosmos SDK は、ステーキングや報酬分配などのインセンティブ メカニズムも統合します。今後の研究では、これらのメカニズムが正しく、期待される経済的インセンティブと一致していることを確認するために、モデル化および検証が行われる予定です。この記事では、Cosmos SDKbank モジュールの高度な正式検証の最初の成功例を示し、ブロックチェーン エコシステムのセキュリティと信頼性の基盤を構築するための効果的な作業を行います。今後の作業では、仮定の検証、他のモジュールの検証、Cosmos SDK インフラストラクチャ全体をカバーすることでこの成果を拡張し、最終的には開発者とユーザーにとってより強固で信頼できるプラットフォームを構築します。
Cosmos SDK標準モジュールの正式検証について詳しく解説
!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-5522147c3d-dd1a6f-6d2ef1)
/ Web3 完全なソフトウェア スタックの高度な形式検証 /
CertiK は最近、Cosmos SDK Bank モジュールに関する高度な正式検証レポートを公開しました。これは、私たちの知る限り、Cosmos SDK の正式検証に成功した最初の試みです。形式的検証は、数学的論理を使用してシステムが仕様に準拠し、考えられるすべての入力および条件下で期待どおりに動作することを確認する手法です。この記事では、Cosmos SDK Bankモジュールを正式に検証する具体的な手順と検証結果を紹介します。
Cosmos SDK とは何ですか?
Cosmos Software Development Kit (略称 SDK) は、開発者がカスタム ブロックチェーン アプリケーションを構築できるようにするフレームワークです。 Cosmos SDK を使用すると、開発者はコンセンサス層からアプリケーション層までの設計や実装について心配することなく、独自のレイヤー 1 ブロックチェーンを簡単に起動できます。 Cosmos SDK は、ステーキング、認証、gov、mint モジュールなど、直接インポートして任意のチェーンで使用できる標準コア モジュールを提供します。
!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-ffb0951d40-dd1a6f-6d2ef1)
ソース：
バンクモジュール
Cosmos SDK の Bank モジュールは、ネイティブ トークンの転送など、トークン管理に関連するすべての機能を担当します。トークンを送信するには、ステーキングされているもの、ロックされているもの、または結合解除されているものを除く、アカウント内に十分な利用可能なトークンがあることなど、多くの制限や条件を満たす必要があります。ステーキングや認証などのモジュールのサポートにより、銀行モジュールはトークン送信のプロセス全体を管理します。銀行モジュールは他のいくつかのモジュールに依存していますが、それらはこの正式な検証の範囲外であるため、プロセスを簡素化するためにそれらの機能についていくつかの仮定を置きます。
SDK のバンク モジュールは、モジュールの動作とデータ型を定義するコア コンポーネントであるキーパーとタイプを含むいくつかのサブモジュールで構成されます。モジュールの主な機能と特徴を説明するため、キーパー サブモジュールに焦点を当てます。
keeper サブモジュールには、表示と送信という 2 つの主要なコンポーネントがあります。ビューキーパーはアカウントと残高の管理を担当し、送信キーパーはロックまたはロック解除されたトークンの転送やステーキングなど、アカウント残高の変更を担当します。バンクモジュールの流れを下図に示します。矢印はコンポーネントから関数または Keeper への方向を示しています。
!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-5140a25ef1-dd1a6f-6d2ef1)
ソース：
＃＃＃ 認証方法
前述したように、この検証の範囲はバンク モジュールに限定されます。検証を開始する前に、まずバンク モジュール内のデータ型の正式な仕様を策定します。たとえば、bank モジュールにはトークン データ構造があり、文字列型の単位と big.Int 型の量が含まれており、ソース コードでは次のように定義されています。
!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-1c78ef9fa4-dd1a6f-6d2ef1)
構造は単純で、Coq (モデリングおよび形式検証言語) で次のように定義します。
!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-34f7c3dbba-dd1a6f-6d2ef1)
この定義に基づいて、銀行モジュールの機能的完全性の基礎を築くために、まずコインの基本操作に関するいくつかの特性を証明します。これは、コイン タイプの頻繁な変更と操作が必要なためです。例えば：
!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-26a5df4754-dd1a6f-6d2ef1)
この補題は基本的な不変性を証明します。つまり、2 枚のコインを差し引いても、その額面は変更されず、残高がマイナスになることもありません。
前の例と同様に、各状態遷移の基礎となるコンポーネントは Coq でモデル化されます。これらのコンポーネントには、KV ストア、ガスメーター、エラー処理、コンテキストが含まれます。
データ型の詳細な仕様とその検証については、以下を参照してください。
キーパーのモデルを作成する
基本コンポーネントのモデリングが完了したら、バンク モジュールのコア キーパーをモデル化して、モジュールの機能を記述することができます。バンクキーパーには 2 つのインターフェイスがあり、1 つはトークン データへの読み取り専用アクセス用で、もう 1 つはトークンの転送と供給メンテナンス用です。
View keeper は、アカウント残高への読み取り専用アクセスを処理する責任があり、アカウント残高を計算するための 4 つの関数が含まれています。
GetBalance: 住所ごとに特定の額面の口座残高を照会します。ここでは、ヌル バイトのシーケンスとヌル以外のバイトのシーケンスの 2 つのケースを考慮します。正式な検証により、GetBalance 関数がどちらの場合でも正しい結果を生成することが保証されます。
LockedCoins: アドレスに対応するアカウント内のすべての非使用トークンを返します。時間の制約のため、認証モジュールからのいくつかの実装について仮定を立てました。
GetAllBalances: 指定されたアドレスにあるすべての口座残高を返します。
GetAccountsBalances: BAddress フィールドと BCoins フィールドをレコードとして、ストレージからすべてのアカウント残高を返します。
!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-0600aa9388-dd1a6f-6d2ef1)
送信マネージャーはトークンの転送と供給を処理します。転送プロセス中はトークンの供給が維持されるため、新しいトークンが鋳造されることはありません。
SetBalance: アドレスを通じてアカウントのトークン残高を設定します。この関数は、残高をゼロに設定した場合と残高をゼロ以外に設定した場合の 2 つのケースを考慮します。どちらの場合も、SetBalance の正しさが証明されます。
subUnlockedCoin: アドレスから指定された量 (トークン) を差し引きます。再帰関数 subUnlockedCoins は、トークンのセットに対して同じことを行います。これらの関数の関連するプロパティは、公理的な仮定として扱われます。
addCoin: 指定された量 (トークン) をアドレスに追加します。再帰関数 addCoins は、コインのセットに対して同じ操作を実行します。これらの関数の関連する特性は、公理的な仮定とみなされます。
SendCoins: あるアカウント アドレスから別のアカウント アドレスに送金すると、両方のアドレスのゴールドが更新されます。受信者が存在しない場合は、その受信者用に新しいアカウントが作成されます。
上記のコア コンポーネントのモデルを使用して、検証を開始できます。
検証プロセス
私たちの検証は、主に「View Keeper」と「Send Keeper」のコア機能に焦点を当て、これらの関数の不変特性を形式的に記述し、補助的な証明システムで証明することによって行われます。
たとえば、仕様と補題 setBalance_ok は、BaseSendKeeper モジュールの setBalance 関数の正しさを証明し、特に次のプロパティを証明します。
send.setBalance が "Ok" 状態に戻ると、newMultiStore が存在しますが、このとき、更新された環境 uctx は、newMultiStore を更新することによって、元の古い環境 ctx から派生します。
設定されている残高は有効なトークンです (システム内のトークンに必要なプロパティを備えています)。
setBalance_prop の関係は、関数が期待どおりに newMultiStore の残高を更新し、更新された環境 uctx を生成するように維持されます。
残高設定が完了したら、口座アドレス addr と額面残高 (Denom) を使用して、更新された環境 uctx 上で view.GetBalance を呼び出すと、send.setBalance で設定したのと同じ残高が返されます。
これらのプロパティは、Coq 仕様言語で次のように説明されます。
!【Cosmos SDK標準モジュールの正式検証の詳細説明】(https://img-cdn.gateio.im/resize-social/moments-69a80767fe-fa94a64bc4-dd1a6f-6d2ef1)
他のプロパティの Coq コードについては、以下を参照してください。
将来のキャリア
この検証の基礎は、いくつかの仮定と公理に基づいて構築されており、検証の範囲を拡大するためにより深く検証できます。今後の作業の優先事項には次の分野が含まれます。
仮定の検証: 現在の検証は、証明の基礎として一連の仮定に依存しています。これらの仮定は、システムの意図された動作と特性を正確に反映していることを確認するために、将来テストすることができます。
認証モジュールの検証: このモジュールはアカウント データと署名メカニズムの管理を担当し、Cosmos SDK のコア コンポーネントです。将来的には、モジュールの実装と他のモジュールとの相互作用が正確であることを確認するために完全に正式に検証される可能性があります。
コインの委任、鋳造、販売に関する定理の追加: 検証範囲を拡大し、コインの委任、鋳造、販売に関する定理をさらに導入することで、システムの動作メカニズムをより包括的に理解するのに役立ちます。これらの定理を認証モジュールの検証と組み合わせて、システム全体の一貫性と正確性を保証できます。
Cosmos SDK インフラストラクチャ全体を拡張する: 現在の検証作業は、主に銀行モジュールとその関連コンポーネントに焦点を当てています。将来的には、正式な検証プロセスを Cosmos SDK インフラストラクチャ全体に拡張することで、プラットフォームの全体的な精度、セキュリティ、安定性が向上し、開発者とユーザーにより安定した信頼性の高い環境を提供できるようになります。
他のモジュールとの統合: Cosmos SDK には相互接続されたさまざまなモジュールが含まれているため、それらの間の相互作用や依存関係を調査することは非常に有益です。これには、モジュール間の相互作用が正しいことを検証し、1 つのモジュールへの変更が他のモジュールに悪影響を及ぼさないことを確認する必要があります。
インセンティブ メカニズムのモデリングと検証: Cosmos SDK は、ステーキングや報酬分配などのインセンティブ メカニズムも統合します。今後の研究では、これらのメカニズムが正しく、期待される経済的インセンティブと一致していることを確認するために、モデル化および検証が行われる予定です。
この記事では、Cosmos SDKbank モジュールの高度な正式検証の最初の成功例を示し、ブロックチェーン エコシステムのセキュリティと信頼性の基盤を構築するための効果的な作業を行います。今後の作業では、仮定の検証、他のモジュールの検証、Cosmos SDK インフラストラクチャ全体をカバーすることでこの成果を拡張し、最終的には開発者とユーザーにとってより強固で信頼できるプラットフォームを構築します。