2545 Tool Integration 72b88b4e

Symbolic Execution Tool Integration

Setup and usage guides for popular symbolic execution tools.

Table of Contents

1. KLEE (C/C++)
2. angr (Python/Binary)
3. Symbolic PathFinder (Java)
4. Z3 (Constraint Solver)
5. Crosshair (Python)

KLEE (C/C++)

Overview

KLEE is a symbolic execution engine for LLVM bitcode. It can automatically generate test cases that achieve high code coverage.

Installation

# Install dependencies
sudo apt-get install build-essential curl libcap-dev git cmake \
  libncurses5-dev python3-minimal python3-pip unzip libtcmalloc-minimal4 \
  libgoogle-perftools-dev libsqlite3-dev doxygen

# Install LLVM
sudo apt-get install llvm-13 llvm-13-dev llvm-13-tools

# Build KLEE
git clone https://github.com/klee/klee.git
cd klee
mkdir build
cd build
cmake ..
make
sudo make install

Basic Usage

1. Write code with symbolic inputs:

// example.c
#include <klee/klee.h>

int get_sign(int x) {
    if (x == 0)
        return 0;
    if (x < 0)
        return -1;
    else
        return 1;
}

int main() {
    int x;
    klee_make_symbolic(&x, sizeof(x), "x");
    return get_sign(x);
}

2. Compile to LLVM bitcode:

clang -I /path/to/klee/include -emit-llvm -c -g example.c -o example.bc

3. Run KLEE:

klee example.bc

4. View results:

# KLEE generates test cases in klee-out-N/
ls klee-last/

# View test inputs
ktest-tool klee-last/test000001.ktest

# Statistics
klee-stats klee-last/

Advanced Options

# Set time limit
klee --max-time=60s example.bc

# Set memory limit
klee --max-memory=1024 example.bc

# Generate only failing tests
klee --emit-all-errors example.bc

# Use optimization
klee --optimize example.bc

# Limit solver time
klee --max-solver-time=5s example.bc

Example: Finding Buffer Overflow

#include <klee/klee.h>
#include <assert.h>

void process_array(int arr[], int size, int index) {
    // Potential buffer overflow
    int value = arr[index];
    assert(value >= 0);
}

int main() {
    int arr[10] = {1, 2, 3, 4, 5, 6, 7, 8, 9, 10};
    int index;

    klee_make_symbolic(&index, sizeof(index), "index");

    // Add assumption: index should be in valid range (but may not be)
    klee_assume(index >= -5);
    klee_assume(index <= 15);

    process_array(arr, 10, index);
    return 0;
}

Run:

clang -I /path/to/klee/include -emit-llvm -c -g overflow.c -o overflow.bc
klee overflow.bc

KLEE will find:

• Test cases where index < 0 (negative index)
• Test cases where index >= 10 (buffer overflow)

angr (Python/Binary)

Overview

angr is a Python framework for analyzing binaries. It supports symbolic execution, control flow analysis, and vulnerability finding.

Installation

pip install angr

Basic Usage

1. Load binary:

import angr

# Load binary
project = angr.Project('./binary')

# Create initial state
state = project.factory.entry_state()

# Create simulation manager
simgr = project.factory.simulation_manager(state)

2. Explore paths:

# Explore until finding target address
target_addr = 0x400600
simgr.explore(find=target_addr)

# Check if target was found
if simgr.found:
    found_state = simgr.found[0]
    print(f"Found target! Input: {found_state.posix.dumps(0)}")

3. Symbolic execution:

import angr
import claripy

# Create project
project = angr.Project('./binary', auto_load_libs=False)

# Create symbolic input
flag = claripy.BVS('flag', 8 * 32)  # 32 bytes

# Create initial state with symbolic stdin
state = project.factory.entry_state(stdin=flag)

# Add constraints (e.g., printable ASCII)
for byte in flag.chop(8):
    state.solver.add(byte >= 0x20)
    state.solver.add(byte <= 0x7e)

# Create simulation manager
simgr = project.factory.simulation_manager(state)

# Explore
simgr.explore(find=lambda s: b"SUCCESS" in s.posix.dumps(1))

if simgr.found:
    solution = simgr.found[0].solver.eval(flag, cast_to=bytes)
    print(f"Solution: {solution}")

Example: Finding Correct Password

import angr
import claripy

def find_password(binary_path):
    # Load binary
    project = angr.Project(binary_path, auto_load_libs=False)

    # Create symbolic password (max 20 bytes)
    password = claripy.BVS('password', 8 * 20)

    # Initial state with symbolic stdin
    state = project.factory.entry_state(stdin=password)

    # Constrain to printable ASCII
    for byte in password.chop(8):
        state.solver.add(claripy.And(byte >= 0x20, byte <= 0x7e))

    # Simulation manager
    simgr = project.factory.simulation_manager(state)

    # Explore until "Correct!" message
    simgr.explore(find=lambda s: b"Correct!" in s.posix.dumps(1),
                  avoid=lambda s: b"Wrong!" in s.posix.dumps(1))

    if simgr.found:
        found = simgr.found[0]
        password_solution = found.solver.eval(password, cast_to=bytes)
        print(f"Password: {password_solution.decode().strip()}")
    else:
        print("No solution found")

find_password('./password_checker')

Hook Functions

import angr

project = angr.Project('./binary')

# Hook a function to replace its implementation
@project.hook(0x400500)
def custom_malloc(state):
    # Custom malloc implementation
    size = state.solver.eval(state.regs.rdi)
    addr = state.heap.allocate(size)
    state.regs.rax = addr

# Or use angr's built-in hooks
project.hook_symbol('printf', angr.SIM_PROCEDURES['libc']['printf']())

Symbolic PathFinder (Java)

Overview

Symbolic PathFinder (SPF) extends Java PathFinder with symbolic execution capabilities for Java programs.

Installation

1. Install JPF core:

git clone https://github.com/javapathfinder/jpf-core.git
cd jpf-core
./gradlew build

2. Install SPF:

git clone https://github.com/SymbolicPathFinder/jpf-symbc.git
cd jpf-symbc
./gradlew build

3. Configure site.properties:

# ~/.jpf/site.properties
jpf-core = /path/to/jpf-core
jpf-symbc = /path/to/jpf-symbc

Basic Usage

1. Write Java code:

public class Example {
    public static int compute(int x, int y) {
        int result;
        if (x > y) {
            result = x + y;
        } else {
            result = x - y;
        }
        return result;
    }

    public static void main(String[] args) {
        int x = Debug.makeSymbolicInteger("x");
        int y = Debug.makeSymbolicInteger("y");
        int result = compute(x, y);
    }
}

2. Create JPF configuration (.jpf file):

# example.jpf
target = Example
classpath = ${jpf-symbc}/build/examples
sourcepath = ${jpf-symbc}/src/examples

symbolic.method = Example.compute(sym#sym)
symbolic.min_int = -100
symbolic.max_int = 100

listener = gov.nasa.jpf.symbc.SymbolicListener

3. Run SPF:

jpf example.jpf

Example: Finding Null Pointer Exception

public class NullCheck {
    public static int getLength(String str) {
        if (str != null) {
            return str.length();
        }
        return 0;
    }

    public static void main(String[] args) {
        String str = Debug.makeSymbolicString("str");
        int length = getLength(str);
        Debug.printSymbolicConstraints();
    }
}

Configuration:

target = NullCheck
symbolic.method = NullCheck.getLength(sym)
symbolic.string_dp = choco

listener = gov.nasa.jpf.symbc.SymbolicListener

Z3 (Constraint Solver)

See constraint_solving.md for comprehensive Z3 usage.

Quick Reference

from z3 import *

# Create solver
solver = Solver()

# Add constraints
x = Int('x')
solver.add(x > 0)
solver.add(x < 10)

# Solve
if solver.check() == sat:
    print(solver.model())

Crosshair (Python)

Overview

Crosshair uses symbolic execution to test Python functions.

Installation

pip install crosshair-tool

Basic Usage

1. Add assertions to code:

def divide(a: int, b: int) -> float:
    """
    Divide two numbers.

    pre: b != 0
    post: _ * b == a
    """
    return a / b

2. Run Crosshair:

crosshair check mymodule.py

3. Watch mode (continuous checking):

crosshair watch mymodule.py

Example: Finding Bugs

def process_list(items: list) -> int:
    """
    Process a list and return the first positive item.

    pre: len(items) > 0
    post: _ > 0
    """
    for item in items:
        if item > 0:
            return item
    return 0  # BUG: violates postcondition if no positive items

Crosshair will find:

AssertionError: postcondition failed
Counterexample: items = [0]

Preconditions and Postconditions

def search(arr: list[int], target: int) -> int:
    """
    Binary search.

    pre: all(arr[i] <= arr[i+1] for i in range(len(arr)-1))  # Sorted
    post: _ == -1 or arr[_] == target
    """
    # Implementation
    ...

Tool Comparison

General Tips

1. Start with simple tools: Z3 for manual analysis, Crosshair for Python
2. Use KLEE for C: Best coverage and bug-finding for C programs
3. angr for binaries: When source code unavailable
4. SPF for Java: Integrates well with Java testing frameworks
5. Combine tools: Use Z3 for constraint solving alongside other tools
6. Set limits: Time and memory limits prevent infinite exploration
7. Focus exploration: Target specific functions or code sections
8. Validate results: Always verify tool-generated test cases