19. angr로 심볼릭 실행 맛보기

심볼릭 실행은 정답을 “추측”하는 도구가 아니다. 입력 바이트를 기호로 두고 프로그램 경로가 요구하는 제약식을 수집한 뒤, 그 제약을 만족하는 구체 입력을 푸는 방법이다. 따라서 대상은 승인된 crackme, CTF, 자기 소유 바이너리로 한정하고, 결과가 실제 의미를 갖는지 디버거로 다시 확인한다.

작은 입력부터 모델링하기

import angr
import claripy

project = angr.Project("./target", auto_load_libs=False)
length = 16
symbolic = claripy.BVS("stdin", length * 8)
state = project.factory.full_init_state(stdin=angr.SimFileStream(
    name="stdin", content=symbolic, has_end=True
))
state.solver.add(symbolic.get_byte(length - 1) == 0x0a)
simgr = project.factory.simulation_manager(state)
simgr.explore(find=0x401234, avoid=[0x401250])
if simgr.found:
    solution = simgr.found[0].solver.eval(symbolic, cast_to=bytes)
    print(solution)

주소는 샘플마다 다르므로 0x401234를 사실처럼 복사하지 말고, 디버거·디스어셈블러에서 성공과 실패 지점을 확인해 바꾼다. PIE나 심볼 제거가 있으면 분석 기준 주소와 런타임 주소를 구분한다. stdin 길이, 줄바꿈, 널 바이트 같은 환경 조건을 모델에 포함하지 않으면 solver가 찾은 입력이 실제 실행에서 재현되지 않는다.

상태 폭발을 다루는 기준

avoid는 빠른 만능 필터가 아니라, 실패 경로라는 근거가 있을 때만 사용한다. 라이브러리를 자동 로드하면 현실성은 늘지만 상태가 커질 수 있으므로, 경계가 분명한 함수는 hook이나 SimProcedure로 추상화한다. 반복문에는 길이 제한과 유효한 초기 상태를 주고, 탐색이 멈췄다면 solver의 난이도보다 잘못된 주소·입력 모델·누락된 환경 의존성을 먼저 점검한다.

해가 나왔다는 사실은 취약점이나 정답의 증명이 아니다. 제약식이 의도한 성공 조건을 표현하는지, 실제 바이너리가 그 입력으로 같은 경로를 택하는지, 분석 중 가정한 외부 함수가 결과를 바꾸지 않는지를 검증해야 한다. 이 구분이 심볼릭 실행을 마술이 아니라 설명 가능한 분석으로 만든다.