Solana is rapidly gaining traction among smart contract developers and users. However, its growing adoption has been accompanied by a series of major security incidents, which have spurred research into automated analysis techniques for Solana smart contracts. Unfortunately, existing approaches do not address the unique and complex account model of Solana. In this paper, we propose SseRex, the first symbolic execution vulnerability detection approach for finding Solana-specific bugs such as missing owner checks, missing signer checks, and missing key checks, as well as arbitrary cross-program invocations. Our evaluation of 8,714 bytecode-only contracts shows that our approach outperforms existing approaches and identifies potential bugs in 467 different contracts. Additionally, we analyzed 120 open-source Solana projects and conducted in-depth case studies on four of them. Our findings reveal that subtle, easily overlooked issues often serve as the root cause of severe exploits, further highlighting the need for specialized analysis tools like SseRex.

翻译：Solana 正在智能合约开发者和用户中迅速获得关注。然而，其日益增长的采用伴随着一系列重大的安全事件，这促使了对 Solana 智能合约自动化分析技术的研究。遗憾的是，现有方法未能解决 Solana 独特且复杂的账户模型。在本文中，我们提出了 SseRex，这是首个用于发现 Solana 特定漏洞的符号执行漏洞检测方法，这些漏洞包括缺失所有者检查、缺失签名者检查、缺失密钥检查以及任意的跨程序调用。我们对 8,714 个仅含字节码的合约的评估表明，我们的方法优于现有方法，并在 467 个不同的合约中识别出潜在漏洞。此外，我们分析了 120 个开源的 Solana 项目，并对其中四个项目进行了深入的案例研究。我们的发现表明，微妙且容易被忽视的问题往往是严重漏洞的根本原因，这进一步凸显了对 SseRex 这类专门分析工具的需求。