Formal verification – a powerful tool for proving the correctness of your programs. How does it actually work? This blog post will provide practical tips to help you use the Move Prover to its fullest potential, as well as explore a real-world example of how we used formal verification to secure a smart contract.
As part of our work, we seek to understand how to eliminate vulnerability classes. Designing safer languages enables developers to write code with confidence. How exactly does Move lend itself to safer programming practices? What can we learn from Move to generalize secure design principles for other execution environments?
We are excited to announce the release of our open-source Binary Ninja plugin for Solana! We have been hard at work developing this tool internally to aid our efforts in blackbox Solana program analysis. While it is still in development, it is now mature enough to be useful (and usable) and we have decided to release it to the larger security community. You can find it on Github here: https://github.com/otter-sec/bn-ebpf-solana. If you find bugs in our plugin or want to add improvements, please open an issue or submit a PR!
Recently, there’s been a rent thief. This bot steals money from uninitialized accounts across the Solana ecosystem, claiming and profiting from the rent. The Solend team noticed the bot when it attempted an attack on the new permissionless pools that are being developed (to be clear, funds stored in the main Solend protocol are completely unaffected). Let’s dig into how rent thieving works by doing a case study on an attack to one of the permissionless pools.
We discovered a critical rounding issue in the Solana Program Library’s implementation of stable swap, spl-token-swap. Similar to Neodyme’s spl-token-lending exploit, we were able to extract a single token per instruction. This exceeds the value of the 5000 lamport transaction fee on BTC stable swaps, allowing an attacker to profitably drain funds.
This blog post is meant as a security focused introduction to Solana written. We explore how exactly Solana’s runtime operates, what degree of control an attacker has, and any relevant security boundaries. That being said, we believe this is an important resource for all developers. With vulnerabilities putting millions in assets at risk, understanding what happens under the hood, even in passing, is crucial to writing safer code.
We discovered a vulnerability in Switchboard’s liquidity pool token price feeds which could hypothetically allow an attacker to manipulate the price of liquidity pool tokens and possibly steal lending protocol funds. This was reported to all affected lending protocols.