Layer7 리버싱 11차시 과제(VM) - prob4

문제 파일을 IDA로 열어 main함수부터 분석해보았다.

prob3와 같았다. 사용자로부터 32개의 문자를 입력받고, 그 입력값에 어떤 연산을 수행한 후, 후에 특정 조건과 비교해 만족한다면 Correct!, 다르면 Wrong...을 출력하고 있다.
init_cpu는

이전 문제처럼 v5에 입력값을 복사하는 역할이었고, run_cpu는 이전 문제와 모두 같고, 데이터만 달랐다.
그래서 조건 분기 부분을 처리하기 위해 prob3처럼 식을 추출하지 말고 그 자리에서 계산해줬고, 마지막에 플래그를 순서대로 출력해 출력조건을 맞춰주었다.

그럼 구현해보자.
일단, 프로그램의 로직대로 연산을 수행하기 위해 stub코드를 추출해줬고, run_cpu의 코드도 파이썬으로 새롭게 짜줬다.
그 후, 플래그의 순서대로 출력하면 플래그가 나온다.

from z3 import *

data=[
0x16, 0x01, 0x07, 0x80, 0x00, 0x00, 0x00, 0x16, 0x01, 0x08, 
0x00, 0x00, 0x00, 0x00, 0xE0, 0x02, 0x0A, 0x7C, 0xC6, 0x4C, 
0xD1, 0x53, 0x37, 0x77, 0x92, 0x5D, 0x02, 0x0A, 0x27, 0x48, 
0xE3, 0x30, 0x02, 0x15, 0xF8, 0xC8, 0x3B, 0x00, 0x00, 0x0A, 
0x78, 0x0A, 0x3B, 0x02, 0x0A, 0xBF, 0x98, 0x1F, 0xF4, 0x8C, 
0xAD, 0xB8, 0x9D, 0xE0, 0x02, 0x0A, 0x56, 0xFE, 0x9F, 0x72, 
0xFA, 0xB5, 0x33, 0xC7, 0x5D, 0x02, 0x0A, 0x0D, 0x5C, 0xBF, 
0xA4, 0x18, 0x15, 0x9E, 0xB5, 0x3B, 0x00, 0x01, 0x0A, 0x78, 
0x0A, 0x3B, 0x02, 0x0A, 0xB7, 0xB0, 0x5F, 0x5B, 0xCF, 0xFE, 
0x0C, 0x68, 0xE0, 0x02, 0x0A, 0xAD, 0xFE, 0x61, 0xE0, 0x1A, 
0x45, 0x62, 0x8F, 0x5D, 0x02, 0x0A, 0x2A, 0xBC, 0xFE, 0xAF, 
0xC6, 0x73, 0xCD, 0xC9, 0x3B, 0x00, 0x02, 0x0A, 0x78, 0x0A, 
0x3B, 0x02, 0x0A, 0xAE, 0x4D, 0x8B, 0xCB, 0x1B, 0x53, 0xB6, 
0xA8, 0xE0, 0x02, 0x0A, 0x1F, 0x33, 0xCC, 0x61, 0xE4, 0x19, 
0xE9, 0x8D, 0x5D, 0x02, 0x0A, 0xC7, 0xFF, 0x06, 0xB8, 0x9D, 
0xC3, 0xB8, 0xE4, 0x3B, 0x00, 0x03, 0x0A, 0x78, 0x0A, 0x3B, 
0x02, 0x0A, 0x69, 0x6B, 0x67, 0xC0, 0x49, 0x47, 0x31, 0x55, 
0x5D, 0x01, 0x08, 0x01, 0x00, 0x00, 0x00, 0xB3, 0x07, 0x08, 
0x21, 0x02, 0x0E, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 
0xCC
]

REG=[BitVec("FLAG(%d)"%i, 64) for i in range(4)]+[0]*14
TEMP=[x for x in REG[0:4]]

it=0
while True:
    res=data[it]
    if res==0xCC:
        break
    elif res==0x00:
        res=cur=data[it+1]
        if cur==1:
            REG[data[it+2]]&=int.from_bytes(data[it+3:it+7], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=7
        elif cur==2:
            REG[data[it+2]]&=int.from_bytes(data[it+3:it+11], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=11
        elif cur==0:
            REG[data[it+2]]&=REG[data[it+3]]
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=4
    elif res==0x16:
        res=cur=data[it+1]
        if cur==1:
            REG[data[it+2]]=int.from_bytes(data[it+3:it+7], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=7
        elif cur==2:
            REG[data[it+2]]=int.from_bytes(data[it+3:it+11], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=11
        elif cur==0:
            REG[data[it+2]]=REG[data[it+3]]
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=4
    elif res==0x5D:
        res=cur=data[it+1]
        if cur==1:
            REG[data[it+2]]+=int.from_bytes(data[it+3:it+7], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=7
        elif cur==2:
            REG[data[it+2]]+=int.from_bytes(data[it+3:it+11], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=11
        elif cur==0:
            REG[data[it+2]]+=REG[data[it+3]]
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=4
    elif res==0xE0:
        res=cur=data[it+1]
        if cur==1:
            REG[data[it+2]]-=int.from_bytes(data[it+3:it+7], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=7
        elif cur==2:
            REG[data[it+2]]-=int.from_bytes(data[it+3:it+11], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=11
        elif cur==0:
            REG[data[it+2]]-=REG[data[it+3]]
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=4
    elif res==0xB2:
        res=cur=data[it+1]
        if cur==1:
            REG[data[it+2]]|=int.from_bytes(data[it+3:it+7], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=7
        elif cur==2:
            REG[data[it+2]]|=int.from_bytes(data[it+3:it+11], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=11
        elif cur==0:
            REG[data[it+2]]|=REG[data[it+3]]
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=4
    elif res==0x78:
        REG[data[it+1]]=~REG[data[it+1]]
        it+=2
    elif res==0x3B:
        res=cur=data[it+1]
        if cur==1:
            REG[data[it+2]]^=int.from_bytes(data[it+3:it+7], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=7
        elif cur==2:
            REG[data[it+2]]^=int.from_bytes(data[it+3:it+11], "little")
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=11
        elif cur==0:
            REG[data[it+2]]^=REG[data[it+3]]
            REG[data[it+2]]&=0xFFFFFFFFFFFFFFFF
            it+=4
    elif res==0xB3:
        REG[16]=REG[data[it+1]]==REG[data[it+2]]
        REG[17]=data[it+1]>data[it+2]
        it+=3
    else:
        res=cur=data[it+1]
        if cur==0:
            it=data[it+2]
        elif cur==1:
            if REG[16]==1:
                it=data[it+2]
            else:
                it+=10
        elif cur==2:
            if REG[16]:
                it+=10
            else:
                it=data[it+2]
                
s=Solver()
s.add(REG[0]==0x7ECB527EEABB074C)
s.add(REG[1]==0xE635AE1A1123CE4F)
s.add(REG[2]==0x61467F6C95358D52)
s.add(REG[3]==0x1FA186EA0DBF462E)
print(s.check())
res=s.model()
print(res)
for i in TEMP:
    print(res[i].as_long().to_bytes(8, "little").decode(), end="")

이런 식으로 코드를 짜주면 다음과 같은 결과가 나온다.

flag : L7{TOO_LONG_INSTRUCTIONS...}