Solana Formal Verification: A Case Study

Solana Formal Verification: A Case Study

We present a novel framework for formal verification of Solana Anchor programs – and a case study application to the Squads multisig.

Since the early days of computing, bugs have crept their way into programs and wreaked havoc on the intentions of the programmer. Logical fallacies, race conditions, or simple typos could manifest as crashes or lay undetected, silently breaking the functionality of the host program.

Rust, Realloc, and References

Rust, Realloc, and References

Rust is safe.. right? Not if your dependencies are unsafe.. A deep dive into a subtle Solana SDK bug, Rust internals, and how we found it all.

It all started with an audit of a program that used realloc on an account, without any bounds checks on the new size allowed. It seemed like the developers assumed that if the new size was too large, the realloc call (from solana_program) would error out appropriately.

The Move Prover: A Practical Guide

The Move Prover: A Practical Guide

A practical guide to the Move Prover - tutorial, case study, and specifications.

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.

Move: An Auditor's Introduction

Move: An Auditor's Introduction

What actually makes Move secure? A discussion of Move’s typing system and formal verification.

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?

Reverse Engineering Solana with Binary Ninja

Reverse Engineering Solana with Binary Ninja

An introduction to our open-source Binary Ninja plugin for blackbox Solana program analysis along with an executive reference to the Solana runtime.

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!

The Story of the Curious Rent Thief

The Story of the Curious Rent Thief

A tale of pickpockets preying on the Solana ecosystem. Read our investigation into the persistent theft of rent from uninitialized accounts. This is the story of the Solend rent thief.

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.

Becoming a Millionaire, 0.000150 BTC at a Time

Becoming a Millionaire, 0.000150 BTC at a Time

How we discovered a critical issue in Solana’s stable swap implementation. A story about arbitrage and rounding.

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.

Solana: An Auditor's Introduction

A security focused introduction to Solana, exploring the underlying runtime environment, security boundaries, and implications. An important resource for all developers who want to write more secure code.

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.

The $200m Bluff: Cheating Oracles on Solana

The $200m Bluff: Cheating Oracles on Solana

How we fooled oracles to beat the house. An exploration into liquidity tokens and oracle price manipulation.

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.

Pagination


© 2022. All rights reserved.

Powered by Hydejack v9.1.6