/ Advanced Formal Verification of Web3 Full Software Stack /
CertiK recently released an advanced formal verification report on the Cosmos SDK Bank module. To our knowledge, this 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 complies with specifications and behaves as expected under all possible inputs and conditions. In this article, we will introduce the specific steps of formal verification for the Cosmos SDK Bank module and some verification results.
What is Cosmos SDK?
The Cosmos Software Development Kit (SDK) is a framework that allows developers to build custom blockchain applications. With the Cosmos SDK, developers can easily launch their own Layer 1 blockchain without worrying 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.
- Why couldn’t Solana take off with liquidity staking despite over 70% of SOL being staked?
- Fair Value Comes New Cryptocurrency Accounting Standards in the United States Will Take Effect by the End of the Year.
- Unveiling the Unknown Types of MEV in Ethereum Transaction Bundles
Source: https://golden.com/wiki/Tendermint-4AP8KX8
Bank Module
The bank module in the Cosmos SDK is responsible for all token management functions, such as the transfer of native tokens. Sending tokens requires meeting various restrictions and conditions, such as having sufficient available tokens in the account, excluding tokens that are staked, locked, or being unbonded. With the support of modules like staking and auth, the bank module manages the entire process of token sending. Although the bank module depends on several other modules, they are not within the scope of this formal verification, so we have made some assumptions about their functionality to simplify the process.
The bank module of the SDK consists of several sub-modules, including keeper and types, which are the core components that define the module’s behavior and data types. We will focus on the keeper sub-module because it covers the main functions and features of the module.
The keeper sub-module 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 following diagram, with arrows indicating the direction from components to functions or Keepers.
Source: https://docs.cosmos.network/v0.46/building-modules/msg-services.html
Verification Method
As mentioned earlier, the scope of this verification is limited to the bank module. Prior to verification, we first formalize the specifications of the data types within the bank module. For example, there is a token data structure in the bank module, which includes a denomination of type string and an amount of type big.Int, defined in the source code as follows:
This structure is very simple and we define it as follows using Coq (our modeling and formal verification language):
Based on this definition, we first prove some properties about the basic operations of coins, laying the foundation for the integrity of the bank module, as it needs to frequently modify and operate the coin type. For example:
This lemma proves a basic invariance: subtracting two coins does not change their face value, nor does it result in a negative balance.
Similar to the previous examples, the underlying components of each state transition are modeled in Coq, including KV Store, GasMeter, Error Handling, and Context.
For detailed specifications and verification of data types, please see: https://github.com/CertiKProject/cosmos-sdk-fv/tree/master/coq_proofs/perennial/src/cosmos_sdk_proofs
Modeling the keeper
After completing the modeling of the basic components, we can model the core keeper of the bank module to describe its functionality. The bank keeper has two interfaces, one for read-only access to token data and another for token transfer and supply maintenance.
The View keeper is responsible for handling read-only access to account balances and contains four functions for calculating account balances:
1. `GetBalance`: Retrieves the balance of a specific denomination for an address. It takes into account two cases: empty byte sequence and non-empty byte sequence. Formal verification ensures that the `GetBalance` function produces correct results in both cases.
2. `LockedCoins`: Returns all non-spendable coins for an address. Due to time constraints, we make assumptions about the implementation from the auth module.
3. `GetAllBalances`: Returns all account balances for a specified address.
4. `GetAccountsBalances`: Returns all account balances from storage, using the fields `BAddress` and `BCoins` as records.
The Send manager is responsible for handling token transfers and supply. During the transfer process, it keeps track of the token supply, so no new tokens are minted.
1. `SetBalance`: Sets the token balance for an account by address. This function takes into account two cases: setting the balance to zero and setting the balance to a non-zero value. The correctness of SetBalance is proven in both cases.
2. `subUnlockedCoin`: Deducts a specified amount (token) from an address. The recursive function `subUnlockedCoins` performs the same operation on a set of coins. The relevant properties of these functions are treated as axiomatic assumptions.
3. `addCoin`: Adds a specified amount (token) to an address. The recursive function `addCoins` performs the same operation on a set of coins. The relevant properties of these functions are treated as axiomatic assumptions.
4. `SendCoins`: Sends an amount from one account address to another, updating the balances of both addresses. If the receiving address does not exist, a new account is created for it.
With the model built using the above core components, we can now proceed with the verification.
Verification Process
Our verification is done by formally describing the invariants of these functions and proving them in an auxiliary proof system. The main focus is on the core functionalities of “View Keeper” and “Send Keeper”.
For example, the specification and lemma `setBalance_ok` prove the correctness of the `setBalance` function in the `BaseSendKeeper` module. Specifically, it proves the following properties:
1. When `send.setBalance` returns the “Ok” state, there exists a `newMultiStore`, and 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 necessary properties of a token in the system).
3. The relationship of `setBalance_prop` is maintained, ensuring that the function updates the balance in `newMultiStore` in the expected way and generates the updated environment `uctx`.
4. After the balance is set, calling `view.GetBalance` on the updated environment `uctx` with the account address `addr` and denomination `balance.(Denom)` will return the same balance set by `send.setBalance`.
These properties are described in the Coq specification language as follows:
For Coq code regarding other properties, visit: https://skynet.certik.com/projects/cosmos.
Future Work
The foundation of this verification is built upon several assumptions and axioms, which can be further verified to expand the scope of verification. The focus of future work includes the following areas:
1. Verification of assumptions: The current verification relies on a series of assumptions as the basis of the proof. In the future, these assumptions can be verified to ensure that they accurately reflect the expected behavior and properties of the system.
2. Verification of the Auth module: This module is responsible for managing account data and the signature mechanism and is a core component of the Cosmos SDK. In the future, a comprehensive formal verification can be conducted to ensure the accurate implementation of the module and its interaction with other modules.
3. More theorems about delegation, minting, and burning: Expanding the scope of verification and introducing more theorems about delegation, minting, and burning will help to gain a more comprehensive understanding of the system’s operation mechanism. These theorems can be combined with the verification of the Auth module to ensure the overall consistency and correctness of the system.
4. Expanding the entire Cosmos SDK infrastructure: The current verification work mainly focuses on the bank module and its related components. In the future, the process of formal verification can be expanded 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 robust and reliable environment.
5. Integration with other modules: As the Cosmos SDK includes various interconnected modules, exploring their interactions and dependencies is beneficial. This requires verifying the correctness of the interaction between modules and ensuring that any changes to one module do not have adverse effects on other modules.
6. Modeling and Verification of Incentive Mechanisms: Cosmos SDK also integrates incentive mechanisms such as staking and rewards distribution. Future research will model and verify these mechanisms to ensure their correctness and alignment with expected economic incentives.
This article presents the first successful case of advanced formal verification of the Cosmos SDK bank module, which has made effective contributions to the security and reliability foundation of the blockchain ecosystem. Future work will expand on this achievement by verifying assumptions, verifying other modules, and covering the entire Cosmos SDK infrastructure, ultimately building a more solid and trustworthy platform for developers and users.
Like what you're reading? Subscribe to our top stories.
We will continue to update Gambling Chain; if you have any questions or suggestions, please contact us!
