100libs Young

Platform: spbctf | Category: Reversing | Type: Challenge | Difficulty: Easy | OS: Linux | Author: XESXOR | Date: 2026-07-02 | Status: Solved Techniques: bit_constraint_recovery, call_state_setup, constraint_solving, force_load_libs, symbolic_execution

Summary

Task: reverse a Linux x86-64 crackme whose check() ANDs the return values of 100 verifyN() functions, each living in its own stripped shared object and imposing bit-level constraints on the input. Solution: force-load all 100 .so files in angr, symbolically execute check() with a printable-ASCII symbolic buffer, constrain rax==1, and let the solver recover the flag string.

100libs Young — spbctf

Description

Task is easy: make the binary say YES

The challenge archive 100libs_young.tar.gz (from the rev-kids20 / forkbomb.ru infrastructure) contains a main ELF 100libs.elf and a libs/ directory holding 100 shared objects verify0.so .. verify99.so. The goal is to find the input string that makes the program print YES, which is exactly the flag.

Analysis

100libs.elf is a dynamically linked, not stripped x86-64 ELF.

• main reads a string via __isoc99_scanf("%s", buf) into a stack buffer at -0x110(%rbp), then calls check(buf). If check returns nonzero it prints YES, otherwise NO.

• check @ 0x4029ca initializes a local result to 1, then calls all 100 imported functions verify0..verify99 (each resolved via PLT from the corresponding verifyN.so) and AND-s every return value into the result: ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

   c read-only • copy allowed Copy
  int result = 1;
  result &= verify0(input);
  result &= verify1(input);
  ...
  result &= verify99(input);
  return result;

  So all 100 checks must return 1 (true) for the binary to say YES.

Each verifyN.so is a stripped shared object exporting a single verifyN(char*) function. Each function performs bit-manipulation constraint checks: it reads specific byte offsets of the input string, extracts individual bits (via sarb shifts + and masks), recombines them, and compares against embedded constants. For example, verify0 @ 0x57a reads offsets like +0xe and +0x2f, extracting bits with sarb $0x7, sarb $0x5, etc. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Collectively the 100 verify functions uniquely determine the correct input string. Manually reversing 100 libraries by hand is tedious and error-prone — automation via symbolic execution is the intended path.

Two key structural facts make angr ideal here:

1. The check function is straight-line — a flat AND-chain with no branching — so symbolic execution produces exactly one deadended state.
2. The correct input is fully determined by the accumulated constraints, so constraining the return value to 1 yields a unique satisfying model. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Solution

Load the main ELF together with all 100 .so files in angr, symbolically execute check with a symbolic input buffer, then constrain the return value to 1 and let the solver recover the input.

 python read-only • copy allowed Copy
#!/usr/bin/env python3
import angr, claripy, glob

# 1. Force-load every verify*.so so the PLT calls in check() resolve.
#    angr did NOT auto-resolve the 100 .so dependencies from the ELF's
#    needed list on this host, so force_load_libs + ld_path is required.
libs = sorted(glob.glob('./libs/verify*.so'))
p = angr.Project('100libs.elf',
                 ld_path=['./libs'],
                 use_system_libs=False,
                 force_load_libs=libs,
                 auto_load_libs=True)
‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

check = p.loader.find_symbol('check').rebased_addr

N = 100
BUF = 0x600000
buf = [claripy.BVS('b%d' % i, 8) for i in range(N)]

# 2. Use a call_state: it sets up a clean stack and a fake return address so
#    execution terminates cleanly at check()'s ret (deadended), instead of
#    running off into unconstrained territory.
st = p.factory.call_state(
    check, BUF, prototype='int check(char*)',
    add_options={angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                 angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS})
‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

# 3. Plant the symbolic buffer, constrain to printable ASCII, NUL-terminate.
for i in range(N):
    st.memory.store(BUF + i, buf[i])
    st.solver.add(buf[i] >= 0x20, buf[i] <= 0x7e)
st.memory.store(BUF + N, claripy.BVV(0, 8))

# 4. Run to completion; the AND-chain is straight-line so there is exactly
#    one deadended state.
sm = p.factory.simulation_manager(st)
sm.run()

for s in sm.deadended:
    s2 = s.copy()
    s2.solver.add(s2.regs.rax == 1)          # force check() to return true
    if s2.satisfiable():
        out = bytes(s2.solver.eval(buf[i]) for i in range(N))
        print(out)                            # flag + don't-care padding
        break

‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

angr returned a single deadended state; constraining rax == 1 was satisfiable and produced the flag string followed by don't-care padding bytes. The recovered buffer included trailing padding (@ and spaces) after the closing } — those bytes are unconstrained, and the actual flag is the prefix ending at }.

Pitfalls

• call_state vs blank_state. Using a blank_state with a hand-set rsp/rbp collided with the BUF data region and produced 0 deadended states / "unconstrained" errors. Switching to call_state (proper stack + fake return address) fixed it — execution then terminates cleanly at the ret.
• force_load_libs is mandatory. angr did NOT auto-resolve the 100 .so dependencies from the ELF's DT_NEEDED list on this host. Explicitly passing force_load_libs=libs together with ld_path=['./libs'] was required for the PLT calls to resolve to the real verifyN implementations.
• Trailing padding. The symbolic buffer beyond the closing } is unconstrained; the solver fills it with arbitrary printable bytes. Trim everything after } to get the flag. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Verification (Docker)

The solve host was macOS but the binary is linux/amd64, so the result was verified inside a Linux container:

 bash read-only • copy allowed Copy
printf 'spbctf{REDACTED}\n' | \
  docker run --rm -i --platform linux/amd64 -v "$PWD":/w -w /w ubuntu:20.04 \
  bash -c 'LD_LIBRARY_PATH=/w/libs ./100libs.elf'
# => YES

‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍