In a series of posts, we will 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 verify Solana contracts formally.

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 often occurs in SBF programs (see [3] for the SBF instruction set).

Figure 2: SBF Virtual Machine

The decompiler (top, right-most component in Figure 1) 's main job 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.) to produce easy-to-prove verification conditions. For instance, the decompiler scalarizes the stack (maps stack slots to local variables) and infers 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 into 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 contact us if you want to integrate Solana into your development process.

Acknowledgments: thanks to Prof. Arie Gurfinkel (University of Waterloo) for his invaluable help in this project, as well as the Certora team, especially 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