SAT Solvers for CTF - From Theory to Flags

SAT solvers provide intelligent constraint-solving that can systematically explore massive search spaces. Once you learn to translate CTF problems into Boolean formulas, they become one of the most powerful tools available for competition problem-solving, and this translates into real capability development for on-the-job skills.

Search spaces are infinite; correct answers are not.

Good CTFs Should Make You Think

If you've been doing CTFs for a while, you've probably encountered challenges where you've reverse-engineered the binary, understood the algorithm, and identified what the flag checker is doing, but the number of possible combinations makes brute forcing impractical. Or perhaps it's a crypto challenge where the cipher is mathematically weak but still computationally complex to break manually.

This is where SAT solvers become valuable.

What is SAT?

The Boolean Satisfiability Problem (SAT) is straightforward to state: given a Boolean formula, can you find values for the variables that make it true? Take (A OR B) AND (NOT A OR C). A SAT solver will determine that this is satisfiable and provide a solution such as A=true, B=true, C=true.

SAT is NP-complete, placing it among the most challenging classes of computational problems. However, modern SAT solvers are remarkably effective despite this theoretical complexity. Over decades of research into algorithms such as conflict-driven clause learning (CDCL), they can handle formulas with millions of variables. For CTF applications, this capacity is more than sufficient.

Basic Setup: Z3 for CTF

The most widely used SAT/SMT solver in CTF competitions is Z3 from Microsoft Research. SMT (Satisfiability Modulo Theories) extends basic SAT to handle not just Boolean logic but also integers, arrays, bit-vectors, and other data types. Install it with:

pip install z3-solver

Here's a common CTF use case. During reverse engineering, you encounter this flag checker:

bool check_flag(char *input) {
    return (input[0] ^ input[1]) == 0x42 &&
           (input[1] + input[2]) == 0xAE &&
           (input[2] * 2) == input[3] + 10 &&
           input[3] < 100;
}

Brute force? Painful. Z3? Easy.

from z3 import *

inp = [BitVec(f'input_{i}', 8) for i in range(4)]
s = Solver()

s.add(inp[0] ^ inp[1] == 0x42)
s.add(inp[1] + inp[2] == 0xAE)
s.add(inp[2] * 2 == inp[3] + 10)
s.add(inp[3] < 100)

# Add printable ASCII constraints
for i in range(4):
    s.add(inp[i] >= 0x20)
    s.add(inp[i] <= 0x7E)

if s.check() == sat:
    m = s.model()
    flag = ''.join(chr(m[inp[i]].as_long()) for i in range(4))
    print(f"Flag: {flag}")
else:
    print("No solution found!")

Z3 explores the constraint space and returns the solution. This pattern applies to any constraint-based flag checker, regardless of complexity.

Real CTF Example: Z3 for Complex Constraints

Consider a typical reversing challenge where the binary checks input character by character, with each check depending on previous characters. The constraints might look like this:

from z3 import *

flag = [BitVec(f'f{i}', 8) for i in range(20)]
s = Solver()

# Constraints from the binary
s.add(flag[0] == ord('f'))
s.add(flag[1] == ord('l'))
s.add(flag[2] == ord('a'))
s.add(flag[3] == ord('g'))
s.add(flag[4] == ord('{'))
s.add((flag[5] ^ 0x12) + flag[6] == 0x7F)

# For products that might exceed 8 bits, we need proper width handling
# Option 1: If the product should fit in 16 bits
prod = ZeroExt(8, flag[7]) * ZeroExt(8, flag[8])
s.add(prod == 0x1C20)

# For shift operations that exceed 8 bits
shifted = ZeroExt(8, flag[9]) << 2
s.add(shifted | ZeroExt(8, flag[10]) == 0x14A)

# Cryptographic mix
s.add((flag[11] ^ flag[12] ^ flag[13]) == 0x42)
s.add(flag[14] + flag[15] + flag[16] == 0x12C)

# Final constraint
s.add(flag[19] == ord('}'))

# Make it printable ASCII
for i in range(5, 19):
    s.add(flag[i] >= 0x20)
    s.add(flag[i] <= 0x7E)

if s.check() == sat:
    m = s.model()
    result = ''.join(chr(m[flag[i]].as_long()) for i in range(20))
    print(f"Flag: {result}")

This should not take more than 10 minutes to implement once you've completed the reverse engineering. The alternative would be writing a custom brute-forcing solution or using angr, which actually employs Z3 for symbolic execution internally.

Crypto Challenges: Analysing Weak Ciphers

SAT solvers are particularly effective for crypto challenges involving weak or reduced-round ciphers. Consider this common beginner-level CTF scenario where you need to recover the key to a plaintext-ciphertext pair:

from z3 import *

# Known plaintext-ciphertext pair
plaintext = [0x41, 0x42, 0x43, 0x44]  # "ABCD"
ciphertext = [0xA0, 0x30, 0xC7, 0x11]  # Valid ciphertext for demonstration

# Unknown key (4 bytes)
key = [BitVec(f'k{i}', 8) for i in range(4)]
s = Solver()

# Model the cipher
def encrypt(p, k):
    result = []
    for i in range(4):
        # XOR with key
        temp = p[i] ^ k[i]
        # Rotate left by 3
        temp = RotateLeft(temp, 3)
        # XOR with next key byte
        temp = temp ^ k[(i + 1) % 4]
        result.append(temp)
    return result

encrypted = encrypt(plaintext, key)

# Add constraints: encrypted must equal ciphertext
for i in range(4):
    s.add(encrypted[i] == ciphertext[i])

if s.check() == sat:
    m = s.model()
    recovered_key = [m[key[i]].as_long() for i in range(4)]
    print(f"Key: {recovered_key}")

This approach generalises to any cipher that can be modelled programmatically. Weaker ciphers allow faster solving by Z3. This technique has proven effective for CTF challenges involving custom stream ciphers, weak block ciphers, and poorly implemented RSA variants.

Logic Puzzles and Sudoku Variants

Some CTF challenges include logic puzzles that conceal flags. While SAT solvers may be excessive for standard Sudoku, CTF competitions often feature complex variants. Here's a basic Sudoku solver implementation in Z3:

from z3 import *

# Create 9x9 grid of integer variables
X = [[Int(f'x_{i}_{j}') for j in range(9)] for i in range(9)]
s = Solver()

# Each cell is 1-9
for i in range(9):
    for j in range(9):
        s.add(And(X[i][j] >= 1, X[i][j] <= 9))

# Each row has distinct values
for i in range(9):
    s.add(Distinct(X[i]))

# Each column has distinct values
for j in range(9):
    s.add(Distinct([X[i][j] for i in range(9)]))

# Each 3x3 box has distinct values
for box_i in range(3):
    for box_j in range(3):
        cells = []
        for i in range(3):
            for j in range(3):
                cells.append(X[box_i*3 + i][box_j*3 + j])
        s.add(Distinct(cells))

# Add known values (puzzle input)
# This would come from the challenge
s.add(X[0][0] == 5)
s.add(X[0][1] == 3)
# ... more constraints

if s.check() == sat:
    m = s.model()
    for i in range(9):
        for j in range(9):
            print(m[X[i][j]], end=' ')
        print()

CTF challenges often add complexity: the solved grid might encode coordinates or spell out the flag. The puzzle might follow custom constraint rules rather than standard Sudoku. Regardless of the variant, the approach remains consistent: model the constraints and allow Z3 to solve them.

Advanced: Circuit Analysis and Hash Collisions

This is where SAT solvers demonstrate particular strength. Some CTF challenges provide a logic circuit or hash function implemented as Boolean logic, requiring you to find an input that produces a specific output. This type of problem is well-suited to SAT solving.

Consider a simplified hash function presented as a circuit:

from z3 import *

def simple_hash(inp):
    # Input is 32 bits - extract high and low 16-bit parts
    a = Extract(15, 0, inp)   # Lower 16 bits
    b = Extract(31, 16, inp)  # Upper 16 bits
    
    # Mix operations
    a = a ^ b
    b = b + a
    a = RotateLeft(a, 5)
    b = b ^ 0xDEAD
    
    # Concatenate back to 32 bits
    return Concat(a, b)

# Find input that hashes to target
inp = BitVec('input', 32)
target = 0x13371337

s = Solver()
s.add(simple_hash(inp) == target)

if s.check() == sat:
    m = s.model()
    collision = m[inp].as_long()
    print(f"Input: {hex(collision)}")

This technique scales effectively. CTF challenges featuring hash functions with hundreds of lines of bit operations can still be solved using this approach. Z3 systematically explores the solution space regardless of complexity.

Maze and Path Finding

CTF challenges sometimes conceal flags behind maze-solving problems with complex constraints. The maze might enforce rules such as only allowing left turns after two straight moves, or changing state based on your movement history. SAT solvers can handle these constraint-based pathfinding problems.

from z3 import *

# Simple maze: find path from (0,0) to (5,5)
# 0 = passable, 1 = wall
maze = [
    [0, 1, 1, 1, 1, 1],
    [0, 1, 0, 0, 0, 1],
    [0, 0, 0, 1, 0, 1],
    [0, 1, 1, 1, 0, 1],
    [1, 1, 0, 0, 0, 0],
    [1, 1, 1, 1, 1, 0],
]

# Path length
N = 15

# Position at each step: (x, y)
path_x = [Int(f'x_{i}') for i in range(N)]
path_y = [Int(f'y_{i}') for i in range(N)]

s = Solver()

# Start at (0,0)
s.add(path_x[0] == 0)
s.add(path_y[0] == 0)

# End at (5,5)
s.add(path_x[N-1] == 5)
s.add(path_y[N-1] == 5)

for i in range(N):
    # Stay in bounds
    s.add(And(path_x[i] >= 0, path_x[i] < 6))
    s.add(And(path_y[i] >= 0, path_y[i] < 6))
    
    # Don't walk through walls
    for x in range(6):
        for y in range(6):
            if maze[x][y] == 1:
                s.add(Or(path_x[i] != x, path_y[i] != y))

# Each step moves by 1 in cardinal directions
for i in range(N-1):
    dx = path_x[i+1] - path_x[i]
    dy = path_y[i+1] - path_y[i]
    s.add(Or(
        And(dx == 1, dy == 0),   # right
        And(dx == -1, dy == 0),  # left
        And(dx == 0, dy == 1),   # down
        And(dx == 0, dy == -1),  # up
    ))

if s.check() == sat:
    m = s.model()
    # Extract the path
    path = []
    for i in range(N):
        x = m[path_x[i]].as_long()
        y = m[path_y[i]].as_long()
        path.append((x, y))
        print(f"Step {i}: ({x}, {y})")
    
    print("\nMaze with path (. = path, # = wall, O = empty):")
    for x in range(6):
        for y in range(6):
            if (x, y) in path:
                print('.', end=' ')
            elif maze[x][y] == 1:
                print('#', end=' ')
            else:
                print('O', end=' ')
        print()

Quick note, this model finds a path but doesn't prevent revisiting cells or loops. To enforce a simple path, add constraints ensuring each position is unique. For shortest paths, minimise N or add optimisation objectives.

Additional CTF-specific constraints (e.g., key collection, trap avoidance, timing requirements) increase model complexity, but Z3 handles these extensions effectively.

When to Use SAT Solvers

SAT solvers are most effective for CTF challenges when:

1. Clear constraints exist, but the combination space is too large for practical brute forcing
2. The challenge involves bit-level operations that are difficult to reverse analytically
3. The problem is fundamentally about logic puzzles or constraint satisfaction
4. Symbolic execution with angr is too slow or overly complex for the use case
5. You need to find inputs to a known function (inverse problems)

SAT solvers are less appropriate when:

1. Simple scripting or mathematical analysis provides a faster solution
2. The problem primarily concerns code execution rather than constraints
3. The challenge is network-based or forensics-focused
4. You haven't yet fully understood the underlying constraints

Practical Tips for CTF

Incremental development: Begin with a single constraint, verify Z3 solves it correctly, then progressively add additional constraints. Avoid attempting to model the entire binary at once.

Use appropriate data types: Employ BitVec('x', 8) for bytes and BitVec('x', 32) for integers. This matches the binary's actual data representation.

Watch bit-vector widths: When operations might exceed the bit-vector width (e.g., multiplying two 8-bit values), use ZeroExt() to extend them first. Otherwise, constants larger than the bit-width get silently truncated mod 2^n, which rarely matches your intent.

Add constraint boundaries: If you know the flag consists of printable ASCII, add those constraints. This significantly reduces the search space.

Verify satisfiability regularly: If s.check() returns unsat, one of your constraints is incorrect. Comment out constraints individually to identify the problematic one.

Set timeouts: Configure a timeout to avoid indefinite waits on unsolvable constraints:

s.set('timeout', 10000)  # 10 seconds

Document your solutions: When you successfully solve a challenge with Z3, save the script. You will reuse these patterns frequently across different challenges.

Beyond Basic Z3

Z3 supports capabilities beyond basic SAT solving:

• Floating point: For challenges involving floating-point operations
• Arrays: For buffer and memory constraint problems
• Strings: For string manipulation challenges
• Quantifiers: For expressing universal ("for all") or existential ("exists") properties

Most CTF challenges don't require these advanced features, but they are available when needed.

Z3 also integrates effectively with other CTF tools. Angr uses Z3 for symbolic execution. Pwntools scripts can invoke Z3 to solve constraints. Binary Ninja can export constraints for Z3 analysis. Rather than choosing between tools, you can strategically combine them.

The Bottom Line

SAT solvers are not universal solutions, but they represent powerful tools for specific problem classes. They enable you to solve problems that appear intractable by translating them into satisfiability queries. Once you develop the skill of thinking in constraints, you'll recognise SAT-solvable problems throughout CTF competitions.

The initial learning curve is substantial. Early attempts may involve incorrectly modelled constraints, unexpected unsat results when anticipating sat, or excessive solving times due to poor problem formulation. This is expected. After solving a few challenges with Z3, the approach becomes more intuitive.

While others develop custom brute forcing solutions or manually trace through assembly to reverse the mathematics, you can leverage Z3's automated solving capabilities. This efficiency advantage can make the difference in time-sensitive competition environments, making proficiency with SAT solvers a worthwhile investment for serious CTF competitors.