본문으로 건너뛰기

30. Z3로 CTF 암호 퍼즐 푸는 루틴

Z3가 암호를 대신 깨주는 것은 아니다. Z3는 사람이 읽은 문제를 제약식으로 정확히 번역했을 때, 가능한 값의 존재와 조건의 충돌을 증명하는 도구다. 여기서 다루는 코드는 CTF와 자기 소유의 퍼즐에만 사용하며, 실제 키나 서비스에 적용하지 않는다.

타입을 먼저 고정한다​

정수 산술과 고정 폭 비트 연산은 전혀 다르다. XOR·rotate·overflow가 있으면 BitVec, 범위가 있는 수학적 정수면 Int를 사용한다. Python의 ^와 Z3 식을 섞을 때는 양쪽이 같은 종류인지 확인한다.

from z3 import BitVec, Solver, sat

x = BitVec("x", 8)
s = Solver()
s.add(x ^ 0x2A == 0x68)
s.add(x >= 0x20, x <= 0x7E)

if s.check() == sat:
    value = s.model().eval(x).as_long()
    print(hex(value), chr(value))

BitVec(8)의 비교와 산술은 8비트 의미를 가진다. 더 넓은 정수로 변환해야 한다면 ZeroExt·SignExt를 명시한다. 모듈러 식은 Int에서 %를 사용하고, 음수의 나머지와 문제의 언어가 정의한 동작이 같은지 작은 예제로 확인한다.

제약식으로 옮기는 순서​

  1. 입력 길이·문자 집합·부분 키를 변수와 범위로 적는다.
  2. 암호 루틴의 각 단계를 작은 함수로 분리한다.
  3. 알려진 평문·암호문·해시 조건을 마지막에 추가한다.
  4. sat, unsat, unknown을 구분하고 모델을 독립 구현으로 검증한다.

예를 들어 여러 바이트의 XOR 퍼즐은 배열로 모델링할 수 있다.

from z3 import BitVec, BitVecVal, Solver, sat

cipher = [0x12, 0x1C, 0x00]  # 0x59 XOR b"KEY"
key = BitVec("key", 8)
s = Solver()
s.add(key >= 0x20, key <= 0x7E)
for c, expected in zip(cipher, b"KEY"):
    s.add((BitVecVal(c, 8) ^ key) == expected)

if s.check() == sat:
    print(s.model()[key].as_long())

실전에서는 중간 계산을 Python으로 미리 해버리면 제약이 사라질 수 있다. 반대로 모든 것을 symbolic으로 만들면 느려질 수 있으므로, 고정된 상수는 계산하고 미지수에 의존하는 부분만 Z3 식으로 남긴다.

해가 나온 뒤의 검증​

모델을 답으로 믿기 전에 원래 암호화·검증 함수에 다시 넣어 입력 전체를 재현한다. 해가 여러 개면 더 강한 제약이 필요하다는 뜻이고, unsat이면 오타·타입·인덱스·엔디언을 먼저 의심한다. 작은 범위의 brute force 결과와 Z3 모델을 교차 비교하면 번역 실수를 빠르게 찾는다.

성능 문제는 무작정 병렬화하기보다 대칭성 제거, 부분 키 고정, 독립 제약의 분리로 줄인다. push()와 pop()으로 가설을 비교하면 solver 상태를 보존할 수 있다. 출력에는 모델의 민감한 값보다 검증된 플래그나 최소한의 해시만 남긴다.

Z3를 잘 쓰는 루틴은 solver 호출보다 문제의 의미를 보존하는 데 있다. 식이 짧아도 타입과 검증 경로가 분명하면 재현 가능하고, 화려한 제약식보다 독립 검산이 신뢰를 만든다.