Generating SMT Libv2 output - wmkhoo/taintgrind GitHub Wiki

Taintgrind can be made to generate SMT-Libv2 formulae to solve for alternative input values whenever tainted conditional branches and load/store addresses are encountered via the --smt2=yes option.

Using the sign32.c example, run with

valgrind --tool=taintgrind --smt2=yes ~/sign32

Save to a trace file with

valgrind --tool=taintgrind --smt2=yes --trace-file=/tmp/sign32.trace ~/sign32

Use z3 to solve for alternative input values with

python3 ./tools/tnt_solve_branches.py --z3 z3 /tmp/sign32.trace

Which should give

branch seq 27: sat
model 1:
  hex: 00000000
  c-escaped: \\x00\\x00\\x00\\x00
  [0] 0x00 addr=0x1ffefffa00 symbol=src_byte_0_1ffefffa00
  [1] 0x00 addr=0x1ffefffa01 symbol=src_byte_1_1ffefffa01
  [2] 0x00 addr=0x1ffefffa02 symbol=src_byte_2_1ffefffa02
  [3] 0x00 addr=0x1ffefffa03 symbol=src_byte_3_1ffefffa03
branch seq 38: sat
model 1:
  hex: 00000080
  c-escaped: \\x00\\x00\\x00\\x80
  [0] 0x00 addr=0x1ffefffa00 symbol=src_byte_0_1ffefffa00
  [1] 0x00 addr=0x1ffefffa01 symbol=src_byte_1_1ffefffa01
  [2] 0x00 addr=0x1ffefffa02 symbol=src_byte_2_1ffefffa02
  [3] 0x80 addr=0x1ffefffa03 symbol=src_byte_3_1ffefffa03
summary: sat=2 unsat=0 unknown=0 total=2

The two alternative values for myint are 0x00000000 and 0x80000000 (or -2147483648 as a signed 32-bit int).

Solving the Symbolic Maze

The symbolic maze in tests/symbolic_maze.c reads a 28-byte movement program from standard input. Each byte must be one of:

  • w — move up
  • s — move down
  • a — move left
  • d — move right

The target returns exit status 1 when the movement program reaches the # cell. The concolic search therefore uses 1 as its success code.

Run the concolic search

Use a 28-byte seed and restrict generated bytes to valid maze commands:

python3 tools/tnt_concolic_search.py \
  --seed ssssssssssssssssssssssssssss \
  --success-code 1 \
  --alphabet wsad \
  --max-runs 80 \
  tests/symbolic_maze

The seed must be exactly 28 bytes. A shorter seed causes the maze to return exit status 3 before its input is tainted, leaving no symbolic branches to explore.

During the search, each line shows the concrete run, target exit status, and candidate input. Exit statuses 10 and above indicate the movement index at which the candidate collided with a wall. The search prioritizes candidates that make more progress through the maze.

A successful run produces output similar to:

run 53: exit=1 input=b'ssssddddwwaawwddddssssddwwww'
solution hex: 73737373646464647777616177776464646473737373646477777777
solution ascii: b'ssssddddwwaawwddddssssddwwww'

The number and order of explored candidates may change as the search policy is updated.

Replay the solution

Replay the result natively and print its exit status:

printf '%s' 'ssssddddwwaawwddddssssddwwww' | tests/symbolic_maze
echo $?

The expected exit status is 1.

Replay it under Taintgrind and save an SMT2 trace:

printf '%s' 'ssssddddwwaawwddddssssddwwww' | \
  ../vg-in-place \
    --tool=taintgrind \
    --taint-stdin=yes \
    --smt2=yes \
    --trace-file=/tmp/symbolic_maze.trace \
    tests/symbolic_maze

Inspect the resulting JSONL trace with:

head /tmp/symbolic_maze.trace