In the previous post, we showed how to prove the correctness of Mint operation which is part of the basic functionality of both the SPL Token and SPL Token 2022. In this post, we show how the Solana Certora Prover (SCP) can be used to find bugs in the confidentiality extension of SPL Token 2022.

The main idea behind the confidentiality extension is to allow making claims about the balance of an account without actually revealing its actual value. Although this might seem magical, zero-knowledge (ZK) proofs allow exactly that. We provide a link at the end of this post in case you want to learn more about ZK proofs and how they are efficiently implemented in Solana.

In this post, we focus on a bug found by an SPL auditor on process_withdraw. Its source code is available here. This function allows withdrawing tokens from an account. Since the actual balance is encrypted, the function relies on a ZK proof to verify that the account has enough funds. One critical correctness property is that the public key associated with the ZK proof must be the same used by the token account from which the funds will be taken. This property did not hold in an older version of SPL Token 2022 and was categorized as a critical bug because an arbitrary amount of tokens could be taken from an account. The bug fix can be found here.

Let’s see how we could have found the bug using SCP. If you have read our previous post, you already know that the first thing we need to do is to write a verification harness. In the previous post, we explained what a verification harness is and wrote one for the Mint operation. Figure 1 shows our verification harness for process_withdraw.

Figure 1: verification harness for process_withdraw

Again, note that the harness is written in Rust and needs to be compiled together with SPL Token 2022. See our previous post for details. At line 64, the function under verification, process_withdraw, is called. In lines 57–62, we create a fresh Solana environment for the function.

This fresh environment consists of the following pieces. The second parameter in the call to process_withdraw, acc_infos contains four accounts. From those four accounts, the first account is called the token account and it is the one from where the funds are deducted. The third parameter of process_withdraw is the amount to be taken. The fifth parameter new_decryptable_available_balance contains the available balance in an encrypted form, and finally, the sixth parameter proof_instruction_offset describes which instruction in the same transaction contains the ZK proof. We omit the details of the first and fourth parameters because they are not relevant in this discussion.

Note that all these parameters are initialized non-deterministically by calling the function cvt::nondet which is defined in this library. Recall from the previous post that defining a non-deterministic value for a variable allows SCP to create a symbolic value of a particular type for that variable rather than reasoning about concrete values. Finally, unlike the harness for the Mint operation, this harness does not add any extra pre-condition to the fresh environment.

After the call, we would like to prove that:

If process_withdraw returns successfully then the encryption public key of the token account is the same as the public key used to generate the ZK proof.

The first thing to notice is that we call the unwrap method on the returned value generated by process_withdraw. This means that if process_withdraw produces an error then the call will panic and therefore, the assertion at line 69 (Figure 1) will never be executed. Note that this is fine since we want to check for our property only if the function returns successfully. The assertion CVT_assert uses two helper functions that allows us to get access to: (1) the encryption key from the extension in the token accountaccount get_encryption_key_from_confidential_extension, and (2) the ZK proof get_proof_withdraw_account. While there is nothing special about the former, the latter constitutes what we call a verification mock and it requires more explanation.

In order to understand what a verification mock is and why we need one here, let us first describe the relevant code of process_withdraw shown in Figure 2.

Figure 2: Using the ZK proof to check that the account has enough funds in process_withdraw

Lines 444–450 obtain the ZK proof that claims that the token account has enough funds. Lines 461–465 perform the actual withdrawal on the encrypted balance and lines 469–471 check that the new available balance is consistent with ZK proof, otherwise an error will be returned. Crucially, the check at lines 456–458 was originally missed and causes our property to be violated.

Unfortunately, the code that extracts a ZK proof (lines 444–450) is too complex for our verifier and any static analyzer. In Solana, transactions consists of instructions. For instance, a specific call to process_withdraw constitutes an instruction. Interestingly, the ZK proof is not passed as another parameter to process_withdraw but is instead provided as another instruction that is part of the same transaction. The parameter proof_instruction_offset from Figure 1, tell us in which instruction (of the same transaction) the ZK proof is stored. Therefore, note that in order to execute one instruction we need to fetch another instruction from the same transaction. This is implemented in Solana by the mechanism of instruction introspection. Moreover, automatic reasoning of the correctness of a ZK proof is very difficult because of the complexity of the math involved. Fortunately, we are not interested in how the program extracts the proof or whether the proof is an actual ZK proof. Instead, we only care about its public key and how it is used. With this in mind, we create a verification mock through a function called get_proof_withdraw_account which has been written specifically for SCP. Similar to testing, a verification mock is a fake implementation of a function. The goal is to omit as many details as possible and only model those aspects relevant for verification. In our case, get_proof_withdraw_account returns a symbolic ZK proof such that the first time it is initialized with non-deterministic values but subsequent calls always return the same proof.

For the curious reader, we show the full code of our mock get_proof_withdraw_account in Figure 3. Before we explain the code, we would like to emphasize that we do not expect Solana devs writing mocks like that. Instead, we plan to extend the Certora Verification Language to allow writing specifications in Rust-like notation. This will allow Solana devs writing mocks, among other things, in a much easier and intuitive way. Coming back to the mock code, we use two implementation “tricks” to simulate the intended behavior of the mock:

1. We define an external function CVT_nondet_pointer_withdraw_account_data that returns a raw pointer to WithdrawData, the type that defines the ZK proof used by process_withdraw. Since we do not provide its implementation, SCP must assume that the returned pointer is initialized non-deterministically. Note that the assumption at line 47 restricts the pointer to be non-null¹.
2. We define a global variable CVT_PROOF_WITHDRAW_ACCOUNT that represents the ZK proof. The first time get_proof_withdraw_account is called the global variable is initialized.

Figure 3: code of get_proof_withdraw_account

Note: The mock does not describe any detail about the ZK proof. This is intentional because our property of interest has nothing to do with the contents of the ZK proof.

The next figure shows the change to use our mock. The original code that extracts the proof has been replaced with the mock at line 444:

Figure 4: modified process_withdraw using a mock to obtain the ZK proof

In our harness written in Figure 1, it should now be easy to understand why we call the mock get_proof_withdraw_account in order to get the ZK proof and from there its public key.

Finally, we are ready to run SCP using our harness. In the previous post, we explained how to compile the harness together with SPL Token 2022 and generate the corresponding SBF code. Here, we show the command to run SCP on SPL Token 2022 before the bug fix:

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

Violated: proper_use_of_encryption_key_process_withdraw_account
proper_use_of_encryption_key_process_withdraw_account: A property is violated
Reports in file:///Users/jorge/Certora-solana-program-library/token/program-2022/src/certora_files/emv-1-release-spl_token_2022.so-04-Aug--14-28/Reports

Recall that the option -solanaEntrypoint tells SCP that the verification process should start from our harness.

SCP reports that the property has been violated. Moreover, it generates a report with more information about the violation (called a counterexample). Currently, the counterexample is shown on the Certora internal representation (IR), and therefore it is not meant for Solana devs. We are working on improving that by showing counterexamples using Rust names.

Next, we run SCP on SPL after the bug fix:

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

Verified: proper_use_of_encryption_key_process_withdraw_account
proper_use_of_encryption_key_process_withdraw_account: Properties successfully verified on all inputs

As you can see, SCP is able to prove that the fixed code satisfies our property of interest.

Challenges and Future Directions

In this series, we focused on functional properties of contracts. There are, of course other security-related properties that are very important. In Solana, an instruction is expected to check that all arguments are well-formed and properly connected. For instance, which account pays for the creation of other accounts, which account signed the transaction, etc. This is often non-trivial to check. Frameworks like Anchor simplify the process by allowing developers to specify account constraints in a declarative way. In principle, it is possible to use SCP to check that the generated code by Anchor satisfies these declarative specifications.

Another interesting property not covered in this series has to do with checking access permissions. For instance, whether a contract has access to modify certain account data. Although access permissions are ensured by the Solana Runtime, there is a clear benefit if they can be checked statically (before deployment) by SCP. Note that verifying access permissions in Solana is an easier task compared to other blockchains such as Ethereum. In Ethereum, a contract can manipulate the state of the whole blockchain. However, the Solana Runtime ensures that only the set of read/written accounts are passed to the contract. This makes the task of verifying access permissions more tractable, even when a contract transitively calls another contract (Cross Program Invocations).

There are two main kinds of Solana accounts: program and data accounts. The former stores the executable SBF bytecode while the later stores application data. For instance, a map of N key-value entries can be implemented by having N data accounts. One common mechanism to link data with a program is by using Program Derived Addresses (PDAs). Currently, SCP does not precisely model the connection between a program and its PDAs but it is something that we plan to support.

Another challenge is the precise modeling of serialization/deserialization of Solana accounts. Since Solana lacks a common format that can be used for communication between contracts, these contracts encode accounts simply as arrays of bytes. A very precise modeling of the serialization/deserialization code might not scale while an imprecise modeling (e.g., assume that deserialization returns non-deterministic accounts) might not be sufficient to prove the properties of interest. We are working on modeling serialization/deserialization at the right level of abstraction.

Conclusion

We have shown how to use SCP on the confidential extension of SPL Token 2022. This turned out to require the use of verification mocks to model hard-to-analyze Solana components. We have also highlighted current challenges and future directions.

We also want to emphasize the unique benefits of automatic verification compared to manual audits.

• First, SCP can formally guarantee that a property always holds or otherwise, provide a counterexample that can be used to either fix a bug or the specification.
• Second, specifications and mocks are reusable. The same problem described in process_withdraw was found by the same auditor in process_empty_account. We can reuse the specification and mock written for process_withdraw in order to check the same property on process_empty_account.
• Third, if the code is modified then SCP can re-check that the property holds on the new code without extra manual effort.

This is the end of our series of posts about formal verification of Solana contracts. We hope that you enjoyed it!

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.

Footnotes

¹ SCP also assumes that the external pointer is properly allocated.

References

All details about the confidentiality extension of SPL Token 2022: https://spl.solana.com/confidential-token/deep-dive/overview

Public key encryption scheme implemented in Solana: https://spl.solana.com/assets/files/twisted_elgamal-2115c6b1e6c62a2bb4516891b8ae9ee0.pdf