The Certora team recently finished reviewing token extensions on Solana utilizing our in-depth formal verification tools. We wrote specifications (also known as rules) for certain key properties of the code and applied the Solana Certora Prover, a tool we built to automatically prove that the code behaves as expected. The Prover verifies the Solana Binary Format (SBF) code, which is the actual code running on the Solana blockchain. 

One of the benefits of writing formal verification specifications is that they can describe scenarios that are very unlikely to happen but can be critical for security. 

In this blogpost, we hope to give you an overview of some key findings from our token extensions security report. If you would like to understand what formal verification is, and how it applies to the Solana blockchain, we’ve created a series of introductory blog posts for you.

First, some context about token extensions

Token2022 is a program on the Solana blockchain operating alongside the 'legacy' SPL Token program. First deployed on mainnet in early 2024, it has become popular for deploying token extensions on Solana, with over 700,000 tokens deployed to date. 

Developed in collaboration with large institutions, token extensions address legacy token limitations, providing Solana developers with tools to add programmable features at an unprecedented level. This flexibility is particularly valuable for enterprise use-cases like KYC or payment reconciliation, offering built-in compliance for Solana projects.

While developers can still use legacy tokens, the new token extensions offer a simpler and more powerful alternative:

• Advanced features can be natively built into tokens, without relying on custom token programs developed in-house or by third parties.
• Rich, on-chain metadata that can be easily initialized, stored, and later modified via a simple update transaction to the token mint.
• Currently, Token2022 offers a total of 15 extensions that can be added to tokens to add capabilities such as confidential transfers, native stablecoin support, transfer fees, and the ability to create "soulbound" (non-transferable) tokens.
  

The result is plug-and-play, regulation-friendly, versatile token functionality that significantly decreases engineering time and resources.

It is important to note that the Token2022 program has already been manually audited by several well-known auditors. However, the work done by Certora has been the first one that automatically verified the SBF code. 

Summary of our main findings

Here are a few highlights from our review:

1. Our review process, which includes verification of low-level SBF code, identified an opportunity for optimization that sped the program’s performance by up to 20%.

2. We developed rules that validate recent updates implemented by the Solana team. These rules serve to reinforce existing safeguards and provide additional assurance against potential issues by covering a comprehensive range of behaviors.

3. We wrote reusable specifications which we used to verify multiple instructions. This approach uncovered that while a fix had been implemented for transfer instructions (Transfer and TransferChecked), it was absent from burn instructions (Burn and BurnChecked). This discrepancy had eluded detection by all previous auditors.

Let’s dive into these in more detail.

Identifying an opportunity for boosting performance

The Solana runtime provides a system call sol_memcmp that implements non-overlapping memory comparisons. The Rust compiler and LLVM provide a builtin intrinsic memcmp for the same operation. Mixing the two prevents many LLVM optimizations since LLVM treats sol_memcmp as an unknown external function. At the same time, all uses of memcmp are compiled to either multiple word-level compares, or a call to sol_memcmp. The exact choice is controlled by Rust Compilers and LLVM optimization switches. The lack of these optimizations can increase the complexity of the SBF file, and therefore, an increase of its computation units. 

In our report, we recommended not to use sol_memcmp, instead use platform independent comparison provided by Rust. This is the commit that followed our recommendation. As part of that commit, there are some tests that showed the reduction of computation units. For instance, for the TransferChecked instruction, the reduction was around 20%.

This optimization was discovered by manually inspecting the SBF code.

Validating program updates

Before this fix, the Solana Program Library (SPL) relied on the Mint account to keep track of non-transferable tokens. However, the SPL also allows unchecked (legacy) transfers, which are transfers without a Mint account.

We wrote a rule that checks that the legacy and the checked transfer instructions were equivalent, with the exception that the checked instruction requires a mint while the legacy instruction doesn’t. This is a simplified version of that rule:

#[rule]

/// If checked transfer fails then unchecked (legacy) transfer should fail
fn rule_transfer_unchecked_checked() {

    // Generate symbolic accounts
    let acc_infos = acc_infos!(); // Certora macro
    let source_info = &acc_infos[0]; 
    let mint_info = &acc_infos[1];
    let destination_info = &acc_infos[2];
    let authority = &acc_infos[3];

    // Generate non-deterministic instruction arguments
    let decimals:u8 = nondet(); // Certora function
    let amount:u64 = nondet(); 

    // Add some preconditions that constrained mint_info
    ...
    let res1 = process_transfer(&id(), &acc_infos, amount,  
                                Some(decimals), None).is_err();
    cvt_assume!(res1); // Certora macro   
    ...

    let res2 = process_transfer(&id(),&acc_infos, amount, 
                                None, None).is_err();
    cvt_assert!(res2); // Certora macro
}

Certora rules are special functions written in Rust. A rule is pretty similar to a testing harness. First, an environment for the function/s under verification is created. Similarly to testing, this environment might contain preconditions that constrain the environment. Second, the function or functions under verification are called. Third, some desired properties are checked. 

The key difference between formal verification and testing is that the environment for verification does not need to be concrete. The environment created by our rule generates a symbolic fixed set of AccountInfo by calling the Certora provided macro acc_infos!. This macro generates the blockchain state under which the calls to process_transfer will be executed. Unless extra preconditions are written, the accounts are fully unconstrained. For instance, the public key of the account is symbolic and, therefore, it can take any value. Similarly, the data of the account is just a non-deterministic array of bytes.  Basic types (for instance u8 and u64) implement a new Rust trait Nondet that generates symbolic values of the appropriate type. Preconditions or assumptions can be written by calling the macro cvt_assume!. Finally, properties are checked by calling the macro cvt_assert!.

Our rule creates a symbolic environment consisting of four accounts: source, mint, destination, and authority. The second account is of special interest because the harness needs to add some extra preconditions to exclude bad-formed Mint accounts. This is because our property only holds if the instruction does not revert due to errors related to the Mint account. For simplicity, we exclude those preconditions from the above rule description.  Moreover, the rule creates two more unconstrained symbolic values for the expected decimals by the Mint account and for the amount to be transferred.  Then, the harness states that if a call to process_transfer with a Mint account (this is known because the fourth parameter is not None) reverts then a call to process_transfer without a Mint account (the fourth parameter is None) must also revert. 

This rule found the issue fixed here and confirmed that the fix was correct. Importantly, note that this rule is actually pretty general, and it can detect other inconsistencies between unchecked and checked transfers. 

Writing reusable specs

The CpiGuard extension ensures that some actions cannot be taken during CPI (Cross-Program Invocations). For instance, fund decreasing instructions (Transfer, TransferChecked, TransferCheckedWithFee, and Burn) when protected by the extension CpiGuard should not be allowed if signed by the owner. The intention is that they are only allowed in cpi if signed by some other account delegate.  Specifically, if CpiGuard is enabled the following scenarios should not be allowed  (i.e., the instruction should revert):

1. An account is delegated to itself
2. The account is a permanent delegate of the mint
3. The account is owned by System Program or Incinerator (in this case, the signing authority is not checked and can be arbitrary) 
   

Before this commit, SPL allowed an account to delegate to itself and sign burn instructions (Burn and BurnChecked). The Certora team wrote this rule to check that the above commit indeed excluded self delegations:

#[rule]

fn rule_process_burn_cpi() {
   let acc_infos = acc_infos!(); // Certora macro
   let source_info = &acc_infos[0];
   let authority_info = &acc_infos[2];
   let source_base = 
       get_account_base!(source_info); // Certora macro
   let amount_arg: u64 = nondet(); // Certora function
   let expected_decimals_arg:u8 = nondet(); // Certora function  
   let source_data = source_info.data.borrow();
   let acc = StateWithExtensions::<Account>::unpack(&source_data)
             .unwrap();
   let ext = acc.get_extension::<CpiGuard>().unwrap();
   cvt_assume!(ext.lock_cpi.into()); // Certora macro
   cvt_assume!(in_cpi()); // Certora macro
   process_burn(&id(), &acc_infos, 
                amount_arg,expected_decimals_arg.into()).unwrap();             
   cvt_assert!
      (&source_base.owner != authority_info.key); // Certora macro

This rule has the same structure as the previous rule. We first generate a symbolic environment and instruction arguments by calling acc_infos! and nondet, respectively. The new part is that the rule only succeeds  if the source account has the extension CpiGuard (lines 8-9), lock_cpi is enabled and the current instruction is executed via CPI by another instruction (line 11). After that, if the instruction BurnChecked succeeds (identified by calling process_burn with a fourth argument different from None) at line 12, then the source’s owner cannot sign the instruction (assertion at line 13). 

We applied the same rule to transfer instructions (Transfer and TransferChecked) by only replacing the call to process_burn with process_transfer and found out that transfer still allowed self-delegations. This problem has been acknowledged by SPL developers and fixed in this commit.

Conclusion

Using the Certora Solana Prover, we were able to contribute to the security of the Token2022 program by formally verifying some critical logic, validating previous code updates and identifying performance optimizations.

As a Solana developer, you too can apply the benefits of formal verification to your own project and detect issues before they get deployed into production.

To learn more about our tools and how we can help secure your app, visit our website at certora.com and join the Certora Discord server through this invite link. We look forward to having you join our community!