Certora today announced its engagement with Solana Foundation to review and formally verify the code underlying token extensions on Solana, the new program-level token features that natively extend token functionality. Certora will formally verify each of the extensions and then provide continuous security for any code changes or updates. We expect token extensions to be at the heart of any Solana application that needs to create and manage tokens. Therefore, providing ongoing security for token extensions is a matter of paramount importance for the whole Solana ecosystem. 

As we shared in previous posts, Certora has developed a new in-house formal verification tool, called the Solana Certora Prover (SCP), to secure Solana contracts. SCP takes Solana contracts written in Rust together with a specification of contract properties (aka rules and invariants) and automatically proves that these properties will always behave as expected. Since Solana contracts are executed using SBF (Solana Binary Format), a low-level bytecode derived from eBPF (extended Berkeley Packet Filtering), SCP analyzes SBF. This allows us to verify the code that actually runs on the Solana blockchain.

Token extensions instructions typically use a subset of extensions that can be enabled or disabled based on user-defined options and the account's state. A critical security property is that the use of multiple extensions should not leave an account in an inconsistent state due to unexpected contradictions among extensions. Providing this kind of assurance is beyond what testing or fuzzing can do due to the large number of possible account’s states due to the interleaving of all active extensions. 

Fortunately, this is when the power of SCP comes to the rescue. We will use SCP to prove mathematically that the semantics of the modifications performed by the extensions on the expected behavior of a Mint or Account are consistent across different SPL instructions. As an example, we will verify that regular and confidential transfer/deposit/withdraw use the same semantics for NonTransferable, ImmutableOwner, MemoTransfer, PermanentDelegate, and CpiGuard extensions.

About Certora

Certora is a blockchain security company that provides industry-leading formal verification tools and smart contract audits. Certora’s flagship security product, Prover, is helping protocols like Aave, Lido, and Maker integrate the power of formal verification into their development pipeline to catch even the most rare & hard-to-find bugs.