In a series of posts, we shall discuss our efforts to formally verify Solana smart contracts. We have developed a new in-house verification tool that takes Solana contracts written in Rust together with a specification and automatically proves that the specification holds. Otherwise, it produces a counterexample that witnesses the specification violation. In this post, we outline the main components of this new verification tool. In subsequent posts, we will demonstrate how to use it to formally verify Solana contracts.

Since Solana contracts are executed using SBF (Solana Binary Format), a low-level bytecode derived from eBPF (extended Berkeley Packet Filtering), our new verifier analyzes SBF. This allows us to verify the code that actually runs in the Solana blockchain. Although verifying SBF instead of Rust or even LLVM bitcode is more challenging, the benefits are twofold: 1. Vulnerabilities caused by compiler bugs can be caught (see e.g., [1]), and 2. Other source languages rather than Rust can be, in principle, supported as long as they are compiled to SBF (see recent projects such as [2]). To the best of our knowledge, our tool is the first automatic verifier (both academic and commercial) that can analyze SBF programs directly.

The new tool Solana Certora Prover (SCP) has been integrated with the Certora Prover (CP). The architecture of the SCP is depicted in Figure 1 below.

Figure 1: Architecture of the Solana Certora Prover (SCP)

Solana contracts are mostly written in Rust but other LLVM-based languages such as C or C++ are also supported. SCP compiles the Solana contract to SBF. The SBF virtual machine [4] mainly operates on four disjoint memory regions as shown in Figure 2: stack, heap, a special region that contains the Solana accounts available to the program, and the text region that contains the executable bytecode and read-only data. This virtual machine only has a set of 11 registers so register spilling occurs often in SBF programs (see [3] for SBF instruction set).

Figure 2: SBF Virtual Machine

The main job of the decompiler (top, right-most component in Figure 1) is to lift SBF code into the internal intermediate representation (IR) used by the Certora Prover. Since SBF programs access stack/heap/accounts regions as unstructured arrays of bytes, a naive translation from SBF to Certora Prover’s IR does not scale from a verification standpoint and therefore, it is not a viable solution. For this reason, our decompiler implements several novel abstract-interpretation based analyses (e.g., partially flow-sensitive pointer analysis, backward numerical analysis, etc) in order to produce easy-to-prove verification conditions. For instance, the decompiler scalarizes the stack (maps stack slots to local variables) and infers must non-alias facts between data from different accounts or heap locations. You can find more technical details in this presentation [5].

When decompilation is completed, the lifted IR program is translated to a set of verification conditions (i.e., logical formulas) that are solved by a portfolio of SMT solvers. If one of the solvers returns that the formula is unsatisfiable then the original Solana contract satisfies its specification. Otherwise, the solver produces a counterexample that is transformed to a human-friendly call trace that can be shown to Solana developers.

In Figure 1, the components enclosed in gray boxes are Solana specific while the rest have been reused from the Certora Prover. We would like to emphasize that the modular design of the Certora Prover has been crucial in allowing us to separate the Solana smart contract language specific aspects from the intermediate representation used by the solver. This separation of concerns allowed us to reuse the Verification Condition (VC) Generator, leveraging years of cutting-edge research and highly skilled engineering done by the Certora SMT team.

Conclusion

We have briefly described our new verification tool for Solana contracts. In the next posts, we shall demonstrate how the verifier can be used to prove the correctness of Solana contracts and discover bugs.

Please get in touch if you are interested in integrating Solana into your development process.

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

[1] Vyper re-entrancy bug. July 30th, 2023. https://cointelegraph.com/news/vyper-vulnerability-exposes-defi-ecosystem-stress-tests

[2] solang: a Solidity compiler for Solana. https://github.com/hyperledger/solang

[3] SBF instruction set: https://bpf.wtf/sol-0x03-isa/

[4] rbpf: Rust (user-space) virtual machine for eBPF. https://github.com/solana-labs/rbpf

[5] Presentation of the Solana Certora Prover in the “Challenges of Software Verification Symposium”, May 2023 in Venice (Italy). https://jorgenavas.github.io/slides/Solana-slides-CSV-05-26-23.pdf