Linux binary symbolic execution not exploring multiple paths

[dguido]

Bug: Linux binary symbolic execution not exploring multiple paths

Summary

The examples/linux/basic example only generates 1 test case instead of the expected 2. The symbolic execution is not exploring both branches of a simple conditional statement.

Environment

• Manticore version: Latest master (commit 289e1e9)
• Python version: 3.11
• OS: Ubuntu Linux
• Installation method: uv pip install -e .

Steps to Reproduce

cd examples/linux
make  # Build the examples
manticore basic  # Or: python -m manticore basic

Expected Behavior

According to the comments in basic.c, Manticore should generate 2 test cases:

1. One where the input is <= 0x41
2. One where the input is > 0x41

The example documentation shows:

Expected output:
  $ manticore basic
  ...
  Generating testcase No. 1 for state No.3 - Program finished correctly
  Generating testcase No. 2 for state No.5 - Program finished correctly

Actual Behavior

Only 1 test case is generated:

$ python -m manticore basic
2025-08-23 03:56:50,529: [2202666] m.n.manticore:INFO: Loading program basic
...
2025-08-23 03:56:59,867: [2202666] m.c.manticore:INFO: Generated testcase No. 0 - test
2025-08-23 03:56:59,988: [2202666] m.c.manticore:INFO: Results in /root/manticore/examples/linux/mcore_kek0chbm

The generated test case has empty stdin and no constraints in the SMT file.

Root Cause Analysis

Issue 1: stdin not being attached to state

The investigation revealed that platform.input is not properly initialized with symbolic stdin. When checking the initial state:

m = Manticore.linux('./basic', stdin_size=256)
state = m._load(m._ready_states[0])
print(f"Has stdin: {hasattr(state.platform, 'stdin')}")  # Prints: False

The stdin should be attached via platform.input.write() in _make_linux() (manticore/native/manticore.py:503), but the platform doesn't have the expected stdin attribute.

Issue 2: Execution terminates early

The program terminates at the entry point (0x4017c0) without executing any instructions:

• No hooks are triggered
• No symbolic values are created
• No state forking occurs

Investigation Details

Test 1: Manual execution works correctly

$ printf "\x00\x00\x00\x00" | ./basic
Message: It is less than or equal to 0x41

$ printf "\x42\x00\x00\x00" | ./basic  
Message: It is greater than 0x41

Test 2: No symbolic values detected

Created debug scripts that hook various points in execution:

• Read syscall (0x41a020)
• After read (0x401717)
• Comparison instruction (0x40171d)
• Conditional jump (0x401722)

None of these hooks are ever triggered, indicating execution never reaches the main function.

Test 3: No state forking occurs

Monitoring for will_fork_state events shows zero forks throughout execution.

Test 4: Generated test case analysis

• test_00000000.stdin: Empty file (0 bytes)
• test_00000000.smt: Only declares STDIN variable, no constraints
• test_00000000.input: Shows all zeros for stdin

Code References

• Binary source: examples/linux/basic.c
• Manticore Linux loader: manticore/native/manticore.py:450-504
• Platform initialization: manticore/platforms/linux.py

Possible Regression

This appears to be a regression as the example documentation shows it previously worked. Recent commits that might be related:

• 1d3251f: Fix gzip state serialization Ubuntu 24.04 Python 3.12
• 882382c: Modernize package build configuration

Workaround

None found. The issue prevents basic symbolic execution functionality from working.

Reproducible Test Case

Created a minimal test that confirms the issue:

# Even this simple program only generates 1 state instead of 2
code = """
#include <unistd.h>
#include <stdio.h>

int main() {
    char c;
    if (read(0, &c, 1) \!= 1) return 1;
    if (c == 'A') {
        printf("Path A\\n");
    } else {
        printf("Path B\\n");  
    }
    return 0;
}
"""
# Compile with gcc -static, run with Manticore
# Expected: 2+ states
# Actual: 1 state

Impact

• Severity: Critical - Core functionality broken
• Affects all Linux binary symbolic execution
• Examples and tutorials don't work as documented
• New users cannot follow the quickstart guide
• Breaks fundamental symbolic execution capability

[dguido]

Investigation Complete - Root Causes Identified

After extensive investigation, I've identified the exact root causes of why the basic example only generates 1 test case instead of 2.

Summary of Findings

The symbolic data IS correctly attached to stdin (256 symbolic bytes present), but execution never reaches the read syscall due to three critical failures in statically-linked binaries:

1. __libc_start_main initialization fails
2. Stack canary protection crashes
3. Complex glibc wrappers interfere with symbolic execution

Root Cause 1: __libc_start_main Initialization Failure

• Location: Address 0x404301 in __libc_start_main
• What happens: Calls __libc_fatal with error "Unexpected relocation type in static binary" (string at 0x4881c8)
• Result: Program calls sys_exit_group(127) before ever reaching main()
• Why: The statically-linked glibc initialization code encounters relocation types it cannot handle in the symbolic execution environment

Execution trace:

1. _start (0x4017c0) - executes successfully
2. Calls __libc_start_main (0x4017df)
3. __libc_start_main performs initialization checks
4. At 0x4042f0: checks relocation type (cmpl $0x25, 0x8(%r15))
5. At 0x404301: calls __libc_fatal when check fails
6. __libc_fatal calls sys_exit_group(127)
7. Program terminates with "Program finished with exit status: 127"

Root Cause 2: Stack Canary Protection Failure

• Location: Address 0x4016ff in main (mov rsi, fs:0x28)
• What happens: Attempts to read stack canary from Thread Local Storage
• Result: Invalid memory access because FS segment base is 0 (TLS not initialized)
• Why: Manticore doesn't properly set up TLS for statically-linked binaries

If we bypass __libc_start_main and jump directly to main:

1. main entry (0x4016f0) - executes successfully
2. At 0x4016ff: mov rsi, fs:0x28 (read stack canary)
3. CRASH: Invalid memory access at address 0x28 (FS base is 0)

Root Cause 3: Symbolic Data IS Present But Never Used

• Finding: The symbolic stdin data is correctly initialized!
• Verification: platform.input has 256 symbolic bytes in the buffer
• Evidence: stdin.buffer contains ArrayVariable(STDIN) symbolic values
• Problem: Execution never reaches the read syscall due to the above failures

Complete Working Workaround

I've developed a complete workaround that makes the example work by addressing all three issues:

from manticore.native import Manticore
from manticore.core.state import TerminateState

m = Manticore.linux('./basic', stdin_size=4)

# 1. Bypass __libc_start_main initialization
@m.hook(0x404260)  # __libc_start_main
def model_libc_start_main(state):
    """Skip glibc init and call main directly."""
    main_addr = state.cpu.RDI  # First arg is main function pointer
    
    # Set up arguments for main(argc, argv, envp)
    state.cpu.RDI = 1  # argc
    state.cpu.RSI = state.cpu.RDX  # argv (was 3rd arg to __libc_start_main)
    state.cpu.RDX = 0  # envp = NULL
    
    # Push return address and jump to main
    state.cpu.push_int(0xdeadbeef)  # Fake return address
    state.cpu.PC = main_addr

# 2. Bypass stack canary checks
@m.hook(0x4016ff)  # mov rsi, fs:0x28
def bypass_canary_read(state):
    """Skip reading canary from TLS."""
    state.cpu.RSI = 0xdeadbeef  # Fake canary value
    state.cpu.PC = 0x401708  # Skip the instruction

@m.hook(0x401735)  # sub rax, fs:0x28 (canary check)
def bypass_canary_check(state):
    """Make canary check pass."""
    state.cpu.RAX = 0  # Make check pass (canary matches)
    state.cpu.PC = 0x40173e  # Skip to next instruction

# 3. Model __libc_read
@m.hook(0x41a020)  # Address of __libc_read
def model_libc_read(state):
    """Directly perform read syscall."""
    fd = state.cpu.RDI
    buf = state.cpu.RSI
    count = state.cpu.RDX
    
    # Call platform's sys_read directly
    result = state.platform.sys_read(fd, buf, count)
    state.cpu.RAX = result
    
    # Return to caller
    ret_addr = state.cpu.pop_int()
    state.cpu.PC = ret_addr

# Handle program termination
@m.hook(0xdeadbeef)  # Our fake return address
def handle_main_return(state):
    raise TerminateState("Program finished", testcase=True)

m.run()

With these hooks, the example successfully:

• ✅ Reaches main
• ✅ Performs the read syscall
• ✅ Gets symbolic value from stdin
• ✅ Evaluates the comparison symbolically
• ✅ Forks at the conditional branch
• ✅ Generates 2 test cases (one ≤ 0x41, one > 0x41)

Alternative Solutions

Option 1: Compile without -static

gcc -o basic basic.c  # Dynamic linking avoids glibc init issues

Option 2: Disable stack protection

gcc -static -fno-stack-protector -o basic basic.c

Option 3: Start directly at main

from manticore.native.manticore import _make_linux
state = _make_linux('./basic', stdin_size=4, entry_symbol='main')
# Still needs stack canary handling

Why This Affects All Static Binaries

ANY statically-linked binary compiled with modern gcc will have these issues:

1. Glibc static initialization: The relocation processing in __libc_start_main is incompatible with symbolic execution
2. Stack protection by default: Modern gcc enables -fstack-protector by default
3. TLS dependency: Stack canaries require Thread Local Storage which Manticore doesn't initialize

Diagnosis Process

The issue was diagnosed through:

1. Initial Discovery: Confirmed only 1 test case generated instead of 2
2. Stdin Verification: Verified symbolic data IS correctly attached to stdin
3. Execution Tracing: Traced from _start to find termination at __libc_start_main
4. Hook Placement: Identified exact failure locations via strategic hooks
5. Memory Analysis: Discovered FS segment base is 0, causing stack canary failure
6. Binary Analysis: Used objdump to understand instruction sequences

Impact

This is a critical issue because:

• It's the FIRST example new users try
• The failure mode is confusing (generates 1 test instead of 2)
• Error messages don't indicate the real problem
• Users may think Manticore is broken or they're using it wrong
• Affects ALL Linux binary symbolic execution with static linking

Recommendations for Permanent Fix

1. Add glibc models: Include built-in models for __libc_start_main and other common glibc functions
2. Initialize TLS properly: Set up FS/GS segments for stack canary support
3. Detect and warn: When loading static binaries, warn users about potential issues
4. Update examples: Compile examples with flags that work out-of-the-box (-fno-stack-protector)
5. Documentation: Add troubleshooting guide for static binary issues

Test Environment

• Binary compiled with: gcc (Ubuntu 11.4.0-1ubuntu1~22.04) 11.4.0
• Confirmed on: Latest master (commit 289e1e9)
• Python: 3.11
• OS: Ubuntu Linux

This investigation shows the issue is a fundamental compatibility problem between Manticore's symbolic execution engine and modern toolchain defaults for static binaries, NOT a problem with symbolic input handling.