Detailed explanation of formal verification of Cosmos SDK standard modules

Detailed explanation of formal verification of Cosmos SDK standard modules

/ Web3 complete software stack advanced formal verification /

CertiK recently published an advanced formal verification report on the Cosmos SDK Bank module, which to our knowledge is the first successful attempt at formal verification of the Cosmos SDK. Formal verification is a technique that uses mathematical logic to ensure that a system conforms to specifications so that it behaves as expected under all possible inputs and conditions. In this article, we will introduce the specific steps to formally verify the Cosmos SDK Bank module, as well as some verification results.

What is Cosmos SDK?

The Cosmos Software Development Kit (SDK for short) is a framework that allows developers to build custom blockchain applications. Using the Cosmos SDK, developers can easily launch their own Layer 1 blockchain without having to worry about the design and implementation from the consensus layer to the application layer. The Cosmos SDK provides standard core modules that can be directly imported and used by any chain, such as staking, auth, gov and mint modules.

Detailed explanation of formal verification of Cosmos SDK standard modules

source:

Bank module

The bank module in the Cosmos SDK is responsible for all functions related to token management, such as the transfer of native tokens. Sending tokens needs to meet many restrictions and conditions. For example, the account must have sufficient available tokens, excluding those tokens that have been staked, locked, or in the process of being unbundled. With the support of modules such as staking and auth, the bank module manages the entire process of token sending. Although the bank module depends on several other modules, since they are not within the scope of this formal verification, we made some assumptions about its functionality to simplify the process.

The bank module of the SDK consists of several submodules, including keeper and types, which are core components that define module behavior and data types. We will focus on the keeper submodule as it covers the main functions and features of the module.

The keeper submodule has two key components: view and send. The view keeper is responsible for managing accounts and balances, while the send keeper is responsible for changing account balances, such as transferring and staking locked or unlocked tokens. The flow of the bank module is shown in the figure below. The arrows indicate the direction from components to functions or Keepers.

Detailed explanation of formal verification of Cosmos SDK standard modules

source:

Authentication method

As mentioned earlier, the scope of this verification is limited to the bank module. Before the verification begins, we first formulate a formal specification for the data types in the bank module. For example, there is a token data structure in the bank module, which contains the denomination of type string and the amount of type big.Int, which is defined in the source code as follows:

Detailed explanation of formal verification of Cosmos SDK standard modules

This structure is very simple. We use Coq (our modeling and formal verification language) to define it as follows:

Detailed explanation of formal verification of Cosmos SDK standard modules

Based on this definition, we first prove some properties about the basic operations of coin to lay the foundation for the functional integrity of the bank module, because it requires frequent modification and manipulation of the coin type. For example:

Detailed explanation of formal verification of Cosmos SDK standard modules

This lemma proves a fundamental invariance: subtracting two coins does not change their denominations, nor does it result in a negative balance.

Similar to the previous example, the underlying components of each state transition are modeled in Coq, including KV Store, GasMeter, Error Handling, and Context.

For detailed specifications of data types and their verification, please see:

Model the keeper

After completing the modeling of the basic components, we can model the core keeper of the bank module to describe the functions of the module. The bank keeper has two interfaces, one for read-only access to token data and the other for token transfer and supply maintenance.

View keeper is responsible for handling read-only access to account balances, and contains four functions for calculating account balances:

  1. GetBalance: Query the account balance of a specific denomination through the address. It considers two cases: a sequence of null bytes and a sequence of non-null bytes. Formal verification ensures that the GetBalance function produces correct results in both cases.

  2. LockedCoins: Returns all non-consumable tokens of the account corresponding to an address. Due to time constraints, we made assumptions about some implementations from the auth module.

  3. GetAllBalances: Returns all account balances under the specified address.

  4. GetAccountsBalances: Returns all account balances from storage, with fields BAddress and BCoins as records.

Detailed explanation of formal verification of Cosmos SDK standard modules

The Send manager handles token transfers and supply. During the transfer process, it maintains the supply of tokens so no new tokens are minted.

  1. SetBalance: Set the token balance for the account through the address. This function considers two cases: a balance set to zero and a balance set to non-zero. In both cases, the correctness of SetBalance is proven.

  2. subUnlockedCoin: Deduct the specified amount (token) from an address. The recursive function subUnlockedCoins does the same for a set of tokens. The relevant properties of these functions are treated as axiomatic assumptions.

  3. addCoin: Add the specified amount (tokens) to an address. The recursive function addCoins performs the same operation on a set of coins. The relevant properties of these functions are considered axiomatic assumptions.

  4. SendCoins: Send the amount from one account address to another account address so that the funds of both addresses are updated. If the recipient does not exist, a new account will be created for it.

Using the above model of the core components, we can begin verification.

Verification process

Our verification is done by formally describing the invariant properties of these functions and proving them in an auxiliary proof system, focusing on the core functions of "View Keeper" and "Send Keeper".

For example, the specification and lemma setBalance_ok prove the correctness of the setBalance function of the BaseSendKeeper module, specifically proving the following properties:

  1. When send.setBalance returns to the "Ok" state, there is a newMultiStore. At this time, the updated environment uctx is derived from the original old environment ctx by updating newMultiStore.

  2. The balance being set is a valid token (it has the required properties of a token in the system).

  3. The relationship of setBalance_prop is maintained to ensure that the function updates the balance in newMultiStore in an expected manner and generates the updated environment uctx.

  4. After the balance setting is completed, use the account address addr and denomination balance.(Denom) to call view.GetBalance on the updated environment uctx, and it will return the same balance set by send.setBalance.

These properties are described in the Coq specification language as follows:

Detailed explanation of formal verification of Cosmos SDK standard modules

For Coq code of other nature, visit:

future career

The basis of this verification is based on several assumptions and axioms, which we can verify more deeply to expand the scope of the verification. Future work focuses on the following areas:

  1. Verification of assumptions: The current verification relies on a series of assumptions as the basis for proof. These assumptions can be tested in the future to ensure that they accurately reflect the expected behavior and properties of the system.

  2. Auth module verification: This module is responsible for managing account data and signature mechanism, and is the core component of Cosmos SDK. In the future, it can be fully formally verified to ensure that the module implementation and interaction with other modules are accurate.

  3. More theorems about delegation, minting and selling coins: Expanding the scope of verification and introducing more theorems about delegation, minting and selling coins will help to understand the operating mechanism of the system more comprehensively. These theorems can be combined with verification of the auth module to ensure the overall consistency and correctness of the system.

  4. Expand the entire Cosmos SDK infrastructure: the verification work at this stage is mainly focused on the bank module and its related components. In the future, the formal verification process can be extended to the entire Cosmos SDK infrastructure, thereby enhancing the overall accuracy, security, and stability of the platform and providing developers and users with a more stable and reliable environment.

  5. Integrate with other modules: Since the Cosmos SDK includes a variety of interconnected modules, it is very beneficial to explore the interactions and dependencies between them. This requires verifying the correctness of the interactions between modules and ensuring that any changes in one module do not adversely affect other modules.

  6. Modeling and verification of incentive mechanisms: Cosmos SDK also integrates incentive mechanisms such as staking and reward distribution. Future research will model and validate these mechanisms to ensure they are correct and consistent with expected economic incentives.

This paper presents the first successful case of an advanced formal verification of the Cosmos SDKbank module, making effective work for the security and reliability foundation of the blockchain ecosystem. Future work will expand on this achievement by validating assumptions, validating other modules, and covering the entire Cosmos SDK infrastructure, ultimately building a more solid and credible platform for developers and users.

View Original
This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
  • Reward
  • Comment
  • Share
Comment
0/400
No comments
Trade Crypto Anywhere Anytime
qrCode
Scan to download Gate app
Community
English
  • 简体中文
  • English
  • Tiếng Việt
  • 繁體中文
  • Español
  • Русский
  • Français (Afrique)
  • Português (Portugal)
  • Bahasa Indonesia
  • 日本語
  • بالعربية
  • Українська
  • Português (Brasil)