Automated Verification Techniques for Solana Smart Contracts
Abstract
Solana has been a relatively new blockchain platform that has gained popularity due to its quick transaction times and low transaction fees. However, the focus is mainly seen in their “smart contracts” – an automatically-enforced agreement under an on-chain program between an individual with financial implications involved. Due to the nature of the platform being relatively new, there has been no foundation related to the security concerns of developing these programs, but such programs have been continually deployed daily without any security considerations. During the investigation of real-world smart contracts, we found that there were several common vulnerabilities – missing ownership checks, missing signer checks, the signed invocation of programs, and the underflow and overflow of arithmetic operations. The mentioned vulnerabilities became the baseline for us to develop verification techniques in identifying them in real-world smart contracts. Furthermore, it became a goal to develop a static analysis tool in Rust that combines all the algorithms into a single static analysis tool, leveraging the MIR functionality provided by Rust. The results conveyed that the tool was able to reliably find sensitive instructions it deemed to be insecure. Even though there were several insignificant results, the initial verification techniques are valid in this early stage of development. Developers who wish to develop Solana smart contracts should use these verification techniques in practice before on-chain deployment as an initial benchmark for security concerns.
Citation
Tavu, Tien N (2022). Automated Verification Techniques for Solana Smart Contracts. Undergraduate Research Scholars Program. Available electronically from https : / /hdl .handle .net /1969 .1 /196530.