Manual reverse engineering writeup reference:

https://leoq7.com/2023/02/PBCTF-Move-VM/

Port of https://github.com/umutoztunc/whitesymex/ to MoveVM

cursor wrote the following:

Move Bytecode Symbolic Execution Engine

A Python-based symbolic execution engine for analyzing Move bytecode, designed for security research and vulnerability discovery in Move smart contracts.

Overview

This tool performs symbolic execution on Move bytecode disassembly, allowing researchers to explore different execution paths and find inputs that reach specific program states. It's particularly useful for:

• Finding inputs that trigger specific code paths in Move smart contracts
• Vulnerability research in blockchain applications
• Understanding complex control flow in Move programs
• Automated test case generation

Features

• Symbolic Execution: Uses Z3 theorem prover for constraint solving
• Path Exploration: Systematically explores different execution paths
• Move Bytecode Support: Handles various Move VM instructions including:
  • Arithmetic operations (Add, Sub, BitOr, BitAnd, Xor, Shl, Shr)
  • Comparison operations (Lt, Neq, Eq)
  • Control flow (Branch, BrFalse)
  • Local variable operations (StLoc, CopyLoc, MoveLoc)
  • Vector operations (VecLen, VecImmBorrow, VecPack, etc.)
  • Type casting (CastU8, CastU64, CastU128)
• Constraint Solving: Automatic generation and solving of path constraints
• State Management: Tracks program state including stack, locals, and instruction pointer

Architecture

Core Components

• State: Represents the execution state with stack, locals, and constraint solver
• PathGroup: Manages multiple execution paths (active, found, avoided, deadended, errored)
• Solver: Z3-based constraint solver for symbolic values
• Strategy: Implements path exploration algorithms
• Instruction: Represents parsed Move bytecode instructions

File Structure

├── main.py          # Entry point and bytecode parser
├── state.py         # Core execution state management
├── path_group.py    # Path exploration management
├── solver.py        # Z3 constraint solver wrapper
├── strategy.py      # Exploration strategy implementation
├── insn.py          # Instruction representation
├── ops.py           # Move bytecode operation definitions
├── errors.py        # Custom exception classes
└── disasm.txt       # Move bytecode disassembly input

Installation

Prerequisites

• Python 3.8+
• Z3 Theorem Prover

Setup

1. Install Z3:

pip install z3-solver

2. Clone or download this repository

3. Ensure your Move bytecode disassembly is in disasm.txt format

Usage

Basic Usage

python main.py

The default configuration will:

1. Parse the bytecode from disasm.txt
2. Create an initial symbolic state
3. Explore paths until reaching instruction pointer 539
4. Print the results and concrete input values

Custom Analysis

from main import parse_file
from state import State
from path_group import PathGroup

# Parse bytecode
instructions = parse_file("your_disasm.txt")

# Create initial state with symbolic input
entry_state = State.create_entry_state(instructions)

# Set up path exploration
path_group = PathGroup(entry_state)
path_group.explore(
    find=lambda state: state.ip == target_instruction,
    avoid=lambda state: state.ip in avoided_instructions,
)

# Get results
if path_group.found:
    concrete_input = path_group.found[0].concretize()
    print(f"Found input: {concrete_input}")

Input Format

The engine expects Move bytecode disassembly in the following format:

B0:
    0: ImmBorrowLoc[0](Arg0: vector<u8>)
    1: StLoc[41](loc40: &vector<u8>)
    2: CopyLoc[41](loc40: &vector<u8>)
    3: VecLen(3)
    ...

Symbolic Execution Process

1. Parsing: Bytecode is parsed into Instruction objects
2. State Initialization: Creates initial state with symbolic input variables
3. Path Exploration: Systematically explores execution paths using symbolic execution
4. Constraint Generation: Builds Z3 constraints for each path condition
5. Solution Finding: Uses Z3 to find concrete inputs that satisfy path constraints

Supported Operations

Arithmetic

• Add, Sub: Integer arithmetic
• BitOr, BitAnd, Xor: Bitwise operations
• Shl, Shr: Bit shifting

Comparison

• Lt: Less than comparison
• Neq, Eq: Equality comparisons

Control Flow

• Branch: Unconditional jump
• BrFalse: Conditional branch on false

Memory Operations

• StLoc, CopyLoc, MoveLoc: Local variable operations
• MutBorrowLoc, ImmBorrowLoc: Reference operations
• ReadRef: Dereference operation

Vector Operations

• VecLen: Get vector length
• VecImmBorrow: Immutable vector element access
• VecPack: Create vector from elements

Examples

Finding Specific Execution Paths

# Find paths that reach a specific instruction
path_group.explore(
    find=lambda state: state.ip == 539,
    avoid=lambda state: state.ip in [100, 200],  # Avoid error states
)

CTF Challenge Solving

The engine is particularly useful for solving blockchain CTF challenges:

# Example: Finding flag input for a Move contract
instructions = parse_file("challenge_disasm.txt")
entry_state = State.create_entry_state(instructions)
path_group = PathGroup(entry_state)

# Look for successful execution path
path_group.explore(
    find=lambda state: state.ip == success_instruction,
    avoid=lambda state: state.ip in error_instructions,
)

if path_group.found:
    flag_bytes = path_group.found[0].concretize()
    flag = ''.join(chr(b) for b in flag_bytes)
    print(f"Flag: {flag}")

Background: pbctf 2023 "MoveVM" Challenge

This symbolic execution engine was originally developed as a solution to the pbctf 2023 "MoveVM" challenge. The challenge involved analyzing Move bytecode to find the correct input that would satisfy certain conditions in the smart contract logic.

Limitations

• Currently supports a subset of Move VM instructions
• Memory model is simplified
• No support for complex data structures beyond vectors
• Limited error handling for malformed bytecode

Contributing

Contributions are welcome! Areas for improvement:

• Additional Move VM instruction support
• Enhanced memory model
• Performance optimizations
• Better error handling and debugging features

License

This project is provided as-is for educational and research purposes.