[💠 Platinum 3] 신기루 뒤의 선형 연립방정식 — DreamHack Mirage 풀이

mov    edi, 6
call   getauxval          ; AT_PAGESZ (=4096)
sub    rax, 1
and    rax, [pagesz]      ; 4096 & 4095 == 0  → 항상 참
test   rax, rax
sete   al                 ; al = 1

# recon.py — 바이너리 기본 정보 + 보호기법
from pwn import ELF, context
context.log_level = 'error'
e = ELF('extracted/chall', checksec=False)
print(f"arch     : {e.arch} {e.bits}-bit")
print(f"PIE      : {e.pie}")
print(f"RELRO    : {e.relro}")
print(f"NX       : {e.nx}")
print(f"Canary   : {e.canary}")
print(f"stripped : {not bool(e.symbols.get('main'))}  (main 심볼 없음)")

strings extracted/chall | grep -E 'Input|Correct|Wrong|Flag is|read error'

; fcn_1644 — 입력 size 검사 후 ...
call   std::__cxx11::...::size()
cmp    rax, 0x32          ; size == 50 ?
setne  al
...                       ; (청크를 변환하며 뭔가 하지만)
mov    eax, 1             ; size만 50이면 끝까지 eax = 1
ret

objdump -d --start-address=0x1685 --stop-address=0x1815 extracted/chall | sed -nE -f mirage.sed

# mirage.sed — fcn_1644 에서 반환값(eax)을 정하는 줄만 골라 주석
/cmp    \$0x32,%rax/{s/$/       <-- size == 50 ?/;p}
/mov    \$0x0,%eax/{s/$/       <-- size 가 50 아니면 0 반환/;p}
/mov    \$0x1,%eax/{s/$/       <-- 그 외에는 무조건 1 (= 통과, 신기루)/;p}
/	ret *$/p

lea    rdx, [exp2_table]   ; 상수 ③
lea    rcx, [transformed]  ; 변환된 입력 (신기루가 채워둔 배열)
lea    rax, [exp1_table]   ; 상수 ②
call   fcn_1ac7            ; → 여기가 진짜 Correct/Wrong 을 가른다

objdump -d --start-address=0x2054 --stop-address=0x2074 extracted/chall | sed -E -f dispatch.sed

objdump -d --start-address=0x65b4 --stop-address=0x662b extracted/chall | sed -E -f b128.sed

# b128.sed — 디스어셈블 실제 출력에 설명 주석만 얹는다(합성 아님)
s/(imul .*%eax)/\1            <-- 자릿수 x 곱수/
s/(and    \$0x7f,%eax)/\1         <-- base-128: 하위 7비트만 남긴다(limb)/
s/(mov    %bl,\(%rax\))/\1          <-- limb 저장/
s/(shr    \$0x7,%eax)/\1          <-- 올림수 = 값 >> 7/
s/(call   12f0 <getauxval@plt>)/\1   <-- anti-analysis 잡음/

# combine_probe.py 핵심 — combine 직후 dest 를 읽어 base-128 곱셈인지 확인
X0  = val(vec($rdi))          # 변환된 chunk0
e00 = val(vec($rsi))          # exp1[0][0]
# ... combine(fcn_69a8) 직후로 continue ...
dest = val(vec($rbp - 0x30))
print(f"X0 * exp1[0][0] = {X0*e00:#x}")
print(f"combine dest    = {dest:#x}")
print(f"combine == base-128 곱셈 ? {X0*e00==dest}")

gdb -q -nx -batch -ex 'source combine_probe.py' -ex 'starti < probe_in.txt' -ex 'py setup()' -ex 'continue' -ex 'cp' extracted/chall

# transform_probe.py — 변환된 입력 배열을 읽어 "5자 = BE 정수"임을 확인
import gdb
CHECK_OFF = 0x1ac7
def rd(a,n): return bytes(gdb.selected_inferior().read_memory(a,n))
def vec(p):
    raw=rd(p,24); p0=int.from_bytes(raw[0:8],'little'); p1=int.from_bytes(raw[8:16],'little')
    return list(rd(p0,p1-p0)) if p0 and 0<=p1-p0<64 else []
def base():
    return int(gdb.execute("info proc mappings",to_string=True).splitlines()[4].split()[0],16)
class T(gdb.Command):
    def __init__(self): super().__init__("tp", gdb.COMMAND_USER)
    def invoke(self,a,ft):
        rdi=int(gdb.parse_and_eval("$rdi"))        # 변환된 입력 배열(10 x vector)
        for i in range(3):
            limbs=vec(rdi+i*24)
            v=sum(d*(128**k) for k,d in enumerate(limbs))
            print(f"chunk[{i}] transform(limbs base128)={bytes(limbs).hex()}  -> int={v:#014x}  bytes={v.to_bytes(5,'big')}")
        gdb.execute("kill")
T()
def setup(): gdb.execute("break *"+hex(base()+CHECK_OFF))

gdb -q -nx -batch -ex 'source transform_probe.py' -ex 'starti < probe_in.txt' -ex 'py setup()' -ex 'continue' -ex 'tp' extracted/chall

for j = 0 .. 9:
    X_0*exp1[j][0] + X_1*exp1[j][1] + ... + X_9*exp1[j][9] == exp2[j]

# solve.py — 핵심부: base-128 복원 + 유리수 가우스 소거
from fractions import Fraction
 
def val(limbs):                       # base-128 bignum(LSB first) -> integer
    v = 0
    for k, d in enumerate(limbs):
        v += d * (128 ** k)
    return v
 
def solve(M, b):
    n = len(M)
    A = [M[j][:] + [b[j]] for j in range(n)]   # 증강행렬
    for c in range(n):
        piv = next(r for r in range(c, n) if A[r][c] != 0)
        A[c], A[piv] = A[piv], A[c]
        pv = A[c][c]
        A[c] = [x / pv for x in A[c]]
        for r in range(n):
            if r != c and A[r][c] != 0:
                f = A[r][c]
                A[r] = [A[r][k] - f * A[c][k] for k in range(n + 1)]
    return [A[i][n] for i in range(n)]

python3 solve.py

# dump_consts.py — gdb로 검증 루틴의 상수(exp1 10x10, exp2 10)를 /tmp/mirage_mat.json 에 덤프
import gdb, json
CHECK_OFF = 0x1ac7
def rd(a, n): return bytes(gdb.selected_inferior().read_memory(a, n))
def vec(p):                                  # std::vector<uint8_t> [begin,end,cap]
    raw = rd(p, 24)
    p0 = int.from_bytes(raw[0:8], 'little'); p1 = int.from_bytes(raw[8:16], 'little')
    return list(rd(p0, p1 - p0)) if p0 and 0 <= p1 - p0 < 256 else []
def pie_base():
    return int(gdb.execute("info proc mappings", to_string=True).splitlines()[4].split()[0], 16)
def setup():
    gdb.execute("break *" + hex(pie_base() + CHECK_OFF))
class DumpConsts(gdb.Command):
    def __init__(self): super().__init__("dc", gdb.COMMAND_USER)
    def invoke(self, arg, ft):
        e1 = int(gdb.parse_and_eval("$rsi"))   # exp1 : 10 x 10 (outer stride 240)
        e2 = int(gdb.parse_and_eval("$rdx"))   # exp2 : 10   (stride 24)
        M = [[vec(e1 + j*240 + i*24) for i in range(10)] for j in range(10)]
        B = [vec(e2 + j*24) for j in range(10)]
        json.dump({"M": M, "B": B}, open("/tmp/mirage_mat.json", "w"))
        gdb.write("dumped exp1(10x10) + exp2(10) -> /tmp/mirage_mat.json\n")
        gdb.execute("kill")
DumpConsts()

# solve.py — 전문: 상수 json을 읽어 선형계를 풀고 flag 출력
import json
from fractions import Fraction
 
def val(limbs):
    v = 0
    for k, d in enumerate(limbs):
        v += d * (128 ** k)
    return v
 
def solve(M, b):
    n = len(M)
    A = [M[j][:] + [b[j]] for j in range(n)]
    for c in range(n):
        piv = next(r for r in range(c, n) if A[r][c] != 0)
        A[c], A[piv] = A[piv], A[c]
        pv = A[c][c]
        A[c] = [x / pv for x in A[c]]
        for r in range(n):
            if r != c and A[r][c] != 0:
                f = A[r][c]
                A[r] = [A[r][k] - f * A[c][k] for k in range(n + 1)]
    return [A[i][n] for i in range(n)]
 
def main():
    d = json.load(open("/tmp/mirage_mat.json"))
    M = [[Fraction(val(d["M"][j][i])) for i in range(10)] for j in range(10)]
    b = [Fraction(val(d["B"][j])) for j in range(10)]
    X = solve(M, b)
    chunks = []
    for i, x in enumerate(X):
        assert x.denominator == 1, f"X[{i}] 가 정수가 아님: {x}"
        xi = int(x)
        bs = xi.to_bytes(5, "big")
        assert all(0x20 <= c < 0x7f for c in bs), f"청크 {i} 가 비출력문자: {bs!r}"
        chunks.append(bs)
    inner = b"".join(chunks).decode()
    print("chunks :", [c.decode() for c in chunks])
    print("input  :", inner)
    print("FLAG   : DH{" + inner + "}")
 
if __name__ == "__main__":
    main()

# reproduce.sh — 상수 덤프 → 선형계 풀이 → flag → 바이너리 검증
set -e
cd "$(dirname "$0")"
BIN=./extracted/chall
chmod +x "$BIN"
printf 'AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA\n' > /tmp/mi.txt
gdb -q -nx -batch -ex 'source dump_consts.py' -ex 'starti < /tmp/mi.txt' \
    -ex 'py setup()' -ex 'continue' -ex 'dc' "$BIN" 2>/dev/null | grep -E 'dumped'
FLAG=$(python3 solve.py | sed -n 's/^FLAG   : //p')
echo "solved: $FLAG"
INNER=$(printf '%s' "$FLAG" | sed -E 's/^DH\{(.*)\}$/\1/')
echo "$INNER" | "$BIN"

bash reproduce.sh