Ajibola Ojo

Work

Prism

A Rust-based symbolic execution pipeline for automatically reconstructing Solana program behaviour.

In progress

Rust / Program analysis / Solana / Z3

Why

Some of the most active programs on Solana, including proprietary AMMs, are deployed without source code. How they price a swap and which accounts they depend on has to be recovered from the deployed binary.

Doing that by hand is slow and has to be repeated every time a program is upgraded. Prism automates the pipeline from on-chain state to a description of the program's behaviour.

What I built

  • Account cloning: pulls a program and the accounts it touches from mainnet into a local environment.
  • Black-box simulation: replays transactions against the cloned state in LiteSVM.
  • Binary tracing: records SBPF execution traces for each simulated call.
  • Dependency reconstruction: recovers which accounts and fields a program reads and writes.
  • Symbolic analysis over the traces with Z3.

Architecture

mainnet state
     │
     ▼
account cloning ──► LiteSVM simulation ──► SBPF traces
                                              │
                                              ▼
                                   lifter ──► IR ──► analyzer (Z3)
                                                        │
                                                        ▼
                                          dependency reconstruction

Implementation

Core pipeline in Rust (tracer, lifter, analyzer and simulator), with Python for analysis and visualisation. Z3 handles constraint solving over lifted SBPF instructions.

Results

Measurements will be published here with the setup needed to reproduce them.

Links