In our previous post, we described our new verification tool for Solana contracts. In this post, we show the verifier in action on SPL Token 2022, a widely-used Solana application. In the next post, we will show how to find bugs in the confidential extension of SPL Token 2022.

Solana SPL Token is analogous to ERC-20 tokens on Ethereum. For instance, SPL Token allows you to mint tokens, transfer tokens, burn tokens, etc. SPL Token 2022 adds extra functionality to SPL Token such as confidential transfers, non-transferable tokens, immutable account ownership, etc. In this post, we demonstrate how to prove the correctness of basic operations such as the Mint operation. Mint is implemented by the function process_mint_to, and its code is available here.

A glimpse of the code

Note that it is out of the scope of this post to describe all details of the Mint operation. In fact, we argue that it should not be necessary to be an expert in SPL Token in order to verify its correctness. Instead, we only show some relevant parts of the code in Figure 1 and 2.

Figure 1: Preamble of process_mint_to

The relevant arguments are accounts and the amount of tokens to mint. The first thing the function does is to extract each of the accounts:

• The mint account mint_info (the one that keeps track of basic information about the new token such as supply)
• The destination account destination_account_info (a token account where the new tokens will be transferred)
• The owner account owner_info (another token account that owns tokens)

The function performs a series of checks (not shown here) to ensure the operation can take place. For instance, one of the checks ensures that the mint account is not frozen and thus, it can mint tokens. Another check validates the owner account as an actual owner of the tokens to be transferred.

Figure 2: transference of tokens and update of the token supply

Figure 2 shows the actual computation of process_mint_to: the amount of tokens is transferred to the destination account and the mint account is updated with the new supply.

Note:

The code checks for integer overflow. If the call to process_mint_to succeeds we know for sure that no integer overflow occurred.

Writing Specifications

In order to use the Solana Certora Prover (SCP), we first need to write a verification harness. A verification harness is similar to a testing harness in the sense that it is a special function that calls the function under verification. Unlike testing, where the function inputs must be actual values, in a verification harness the inputs can be symbolic. After the function returns successfully, the harness can have one or more assertions that describe the properties of interest. Figure 3 shows the full code of our verification harness for process_mint_to.

Figure 3: verification harness for process_mint_to

As you can see, the verification harness is simply another function written in Rust. In this case, we didn’t need to modify process_mint_to at all. A typical harness consists of three parts:

1. A non-deterministic Solana environment together with any necessary precondition that restricts the environment.
2. Call the function under verification.
3. The post-condition.

For writing non-deterministic environments, we have built a Rust library that extends both Rust basic types such as Boolean, integers, etc. and Solana-specific types such as AccountInfo or PubKey to create objects of those types that can be interpreted as fully symbolic by SCP (e.g. see nondet functions in Figure 3). For instance, acc_infos is an array of three non-deterministic accounts: the mint account, the destination account and the owner. In addition to creating fresh environments, note that Solana developers can also write preconditions that restrict the environment. For instance, CVT_assume(amount>0) tells the verifier that we only care about inputs where the amount is strictly greater than zero.

After this, the harness calls process_mint_to with the fresh environment and a symbolic non-zero positive amount. Very importantly, note that the harness calls unwrap on the value returned by process_mint_to. This means that if process_mint_to produces some kind of error (i.e. any of the checks failed) then, the call will panic (i.e., abort) and therefore, the rest of the harness will never be executed. In particular, if the execution of the harness panics, then the post-condition (the assertions after) will not be executed. Although this might be counter-intuitive, this is exactly the behavior that we want. If the call to process_mint_to fails, then the Solana transaction that makes the call will be reverted without having any effect on the blockchain state.

Last but not least, there are four assertions (see calls to CVT_assert) that establish the post-condition. The first assertion checks that the tokens of the destination account after the call to process_mint_to must be the number of tokens before the call plus the amount of tokens being minted. The second assertion checks that the number of tokens after must be strictly greater than the number of tokens before. Note that this is only true because we added the precondition that the amount must be greater than zero. Similarly, the third and forth assertions check for the same conditions but for the token supply.

Compile SPL Token 2022 and Usage of SCP

Since SPL Token 2022 is written in Rust, to compile the application with our verification harness, we first need to modify Cargo.toml in order to include the Certora library that contains all the functionality to create fresh environments as well as special functions to write the pre- and post-conditions used in Figure 3:

[dependencies.solana-cvt]
path = "../../solana-cvt"

and add the following line in the lib.rs:

mod certora_verification_harness;

where certora_verification_harness.rs contains the function integrity_of_process_mint_to shown in Figure 3.

Then, we are ready to generate SBF with the command:

cargo build-sbf --arch=sbfv2

And finally, run the Solana Certora Prover:

certoraRun.py target/sbf-solana-solana/release/spl_token_2022.so \
              --prover-args \
              "-solanaEntrypoint integrity_of_process_mint_to"

Verified: integrity_of_process_mint_to
integrity_of_process_mint_to: Properties successfully verified on all inputs

The option -solanaEntrypoint tells the prover that the verification process should start from our harness. In this case, SCP is able to prove the property in a few milliseconds.

Conclusions

We have shown how to use SCP to prove the correctness of the Mint operation. As a Solana developer, the main task is to write a verification harness that contains both the specification (pre- and post-conditions) and the expected Solana environment by the code under verification. Our next post will show how to find bugs in the confidential extension of SPL Token 2022 which will require the use of verification mocks.

Acknowledgements: thanks to Prof. Arie Gurfinkel (University of Waterloo) for his invaluable help in this project, and the Certora team, specially Alexander Bakst and John Toman.

References

To learn more about Solana programming model: https://solanacookbook.com/

The source code of SPL Token: https://github.com/solana-labs/solana-program-library/tree/master/token/program

The source code of SPL Token 2022: https://github.com/solana-labs/solana-program-library/tree/master/token/program-2022