Recently, we published a report on customized formal verification of the Cosmos SDK bank module, which we believe is the first such successful effort for the Cosmos SDK. Formal verification is a technique that uses mathematical logic to ensure that a system conforms to a specification and behaves as expected under all possible inputs and conditions. Here, we will guide you through the steps taken to formally verify the bank module of the Cosmos SDK, as well as some results of the verification process.

This is the third in a series on formal verification of the whole Web3 stack. Previous articles include a review of the formal verification of TON master chain contracts and the formal verification of Ant Group's HyperEnclave.

What is the Cosmos SDK?

The Cosmos Software Development Kit (SDK) is a framework that enables developers to build custom blockchain applications. With the Cosmos SDK, developers can easily bootstrap their own Layer 1 blockchain without having to worry about designing and implementing everything from the consensus layer to the app layer. Cosmos SDK provides core modules that any chain can directly import and utilize, such as staking, auth, gov, and mint modules.

Source: Tendermint

The Bank Module

The bank module in the Cosmos SDK handles all functionality related to token management, such as native coin transfers. There are many constraints and conditions that need to be satisfied for one to be able to send coins, like having enough available coins, excluding staked, locked, or unbonding coins. The bank module, with assistance from other modules such as staking and auth, manages the entire process for sending coins. While the bank module relies on some other modules, they are out of the scope of this formal verification, so we postulate some assumptions about their functionality to avoid overly complicating the process.

The SDK bank module consists of several submodules, including keeper and types, which are the core components that define the behaviors and the data types of the module respectively. Between the two modules, we’re going to focus on the keeper submodule, which contains most of the module’s functionality and features.

The keeper submodule has two key components: view and send. The view keeper manages account and balance, and the send keeper manages modifying account balances, like transferring and staking locked/unlocked coins. A flowchart for the bank module is shown below, with arrows directed from component to functionality/keeper.

Source: Cosmos Documentation

Methodology As previously mentioned, the scope is limited to the bank module. The verification process begins by formally specifying the data types within the bank module. For instance, the bank module has a coin struct containing a string denomination and big.Int amount. In the original source code, it is defined as follows:

type Coin struct {
	Denom  string 
	Amount Int    
}

Given the simplicity of the structure, the Coq (our modeling and formal verification language) record is defined as follows:

Record Coin := { Denom : string; 
                 Amount : Z }.

From this definition, we first prove properties about the basic coin operations to establish a foundation for the bank module's functionalities, which frequently modify and manipulate the coin type. For example,

Lemma sub_coin_ok coin1 coin2 coin3 :
sub_coin coin1 coin2 = coin3 -> 
error.is_ok error.error Coin coin3 = true ->
(coin1.(Denom) = coin2.(Denom))%string /\
not (is_negative 
     {| Denom := coin1.(Denom); 
        Amount := coin1.(Amount) - coin2.(Amount) |}).

The above lemma proves a basic invariant that subtracting two coins will never change the denomination or result in a negative balance.

Similar to the example above, the underlying components contributing to each state transition are modeled in Coq. The components include the KV Store, GasMeter, Error Handling, and Context. Detailed specification and verification of the data types can be found in the published repository on GitHub.

Modeling Keepers

After migrating the base components, we can model the core keepers of the bank module to outline the module functionality. The bank keeper has two interfaces, one for read-only access to token data and one for transferring and maintaining token supply.

View Keeper manages read-only access to account balances. It has four functions used for account balance calculation:

1. GetBalance: Retrieves the balance of a specific denomination for an account by address. It considers two scenarios: empty and non-empty byte sequences. Formal verification ensures that the GetBalance function produces the correct result in both cases.
2. LockedCoins: Returns all unspendable coins for an account by address. Due to time constraints, some implementations from the auth module are assumed but not implemented.
3. GetAllBalances: Returns all account balances for a given account address.
4. GetAccountsBalances: Returns all account balances from the store as a record with fields BAddress and BCoins.

Send Keeper manages the transfer of coins and token supply. It maintains the token supply during transfer so no new token is minted.

1. SetBalance: Sets the coin balance for an account by address. The function considers two cases: setting a zero balance and setting a non-zero balance. The correctness of SetBalance is proven in both cases.
2. subUnlockedCoin: Deducts an amount (coin) from an address. A recursive function, subUnlockedCoins, performs the same operation for a set of coins. Properties related to these functions are assumed as axioms.
3. addCoin: Adds an amount(coin) to an address. A recursive function, addCoins, performs the same operat ion for a set of coins. Properties related to these functions are assumed as axioms.
4. SendCoins: Sends an amount from one account address to another, resulting in an updated context with the amount updated for both addresses. It also supports cases where the receiver does not exist, in which case a new account is created.

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

Formal Verification

Verification is accomplished by formalizing a function's invariants and proving them in a proof assistant. The primary focus is on the core functionalities of the View Keeper and Send Keeper.

For instance, the specification and lemma setBalance_ok demonstrate the correctness of the setBalance function for the BaseSendKeeper module. It specifically proves the following properties:

1. When send.setBalance returns an "Ok" state, there exists a newMultiStore such that the updated context uctx is derived from the original context ctx by updating the newMultiStore.
2. The balance being set is a valid coin (i.e., it satisfies the properties required for a coin in the system).
3. The setBalance_prop relation holds, which ensures that the function behaves as expected in terms of updating the balance in the newMultiStore and producing the updated context uctx.
4. After the balance is set, calling view.GetBalance on the updated context uctx, with the account address addr and denomination balance.(Denom), will return the same balance that was set by send.setBalance.

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

Inductive setBalance_prop : send.BaseSendKeeper -> context ->  address.AccAddress -> Coin -> MultiStore -> context -> Prop :=
...

Lemma setBalance_ok bk addr balance ctx uctx:
send.setBalance bk ctx addr balance = error.Ok error.error context uctx ->
exists newMultiStore, 
uctx = update_ms_context ctx newMultiStore /\
validate_coin balance /\
setBalance_prop bk ctx addr balance newMultiStore uctx /\
view.GetBalance bk.(send.svkeeper) uctx addr balance.(Denom) = 
error.Ok error.error Coin balance.

The Coq code for the other properties can be found in the report.

Future Work

The verification's baseline consists of several assumptions and axioms, which can be further validated to expand the scope of the work. Some possible areas of future focus include:

1. Validating Assumptions: The current verification relies on a set of assumptions serving as the baseline for proofs. Further work can validate these assumptions, ensuring they accurately represent the intended behavior and properties of the system.
2. Auth Module Verification: The auth module, responsible for managing account data and the signing mechanism, is a critical component of the Cosmos SDK. Future work could involve a more comprehensive formal verification of this module, ensuring the correctness of its implementation and its interaction with other modules.
3. Additional Theorems for Delegation, Minting, and Burning Coins: Expanding the scope of the verification effort to include more theorems related to delegation, minting, and burning coins would provide a more complete understanding of the system's behavior. These theorems could be connected to the auth module verification to ensure the consistency and correctness of the entire system.
4. Extending to the Entire Cosmos SDK Infrastructure: The current verification efforts focus on the bank module and related components. Future work could involve extending the formal verification process to encompass the entire Cosmos SDK infrastructure, providing a higher level of confidence in the overall correctness, security, and reliability of the platform, making it more robust and trustworthy for developers and users alike.
5. Integration with Other Modules: As the Cosmos SDK consists of various interconnected modules, it would be beneficial to explore the interactions and dependencies between them. This would involve verifying the correctness of module interactions and ensuring that any changes in one module do not adversely affect others.
6. Modeling and Verification of Incentive Mechanisms: The Cosmos SDK also includes incentive mechanisms such as staking and rewards distribution. Future work could involve modeling and verifying these mechanisms to ensure their correctness and alignment with the intended economic incentives.

This article demonstrates the successful formal verification of the Cosmos SDK bank module, providing a foundation for improved security and reliability in the blockchain ecosystem. The application of formal verification to such modules is a powerful form of Web3 security analysis. Future work can expand on this achievement by validating assumptions, verifying other modules, and encompassing the entire Cosmos SDK infrastructure, ultimately contributing to a more robust and verifiably trustworthy platform for developers and users.