layer7 리버싱 11차시 과제(VM) - prob3

일단 문제 파일을 내려받아 아이다로 열어보았다.

대충 사용자로부터 32개의 문자를 입력받고, 그 문자에 대한 연산을 수행한 후, 그 연산 결과가 아래 조건문과 일치하는지 보고 일치하면 Correct!, 다르면 Wrong...을 출력하는 코드이다.

그럼 사용자로부터 입력받은 후의 첫번째 함수인 init_cpu를 보자.

사용자로부터 입력받은 값을 v5라는 새로운 배열에 복사하는 코드였다.

그럼 다음 코드, run_cpu 부분을 확인해보자.

다른 VM 문제와 같은 형식이었다.
stub이라는 배열에 들어있는 값에 따라 연산을 수행해나가는 코드였다.

처음엔 그냥 "코드 그대로 가져다 써서 식 추출한 다음에 그대로 z3-solver 돌리면 되겠지"라고 생각했으나, 밑에 있는 조건문을 보고 생각이 달라졌다.

이렇게 미지수인 a1 배열의 값에 따라 분기하는 것 때문이었다.
이를 어떻게 해결해야할지 생각하다 선배님의 풀이를 듣게 되었는데, 바로 연산을 수행하면서 분기를 그때그때 수행해주면 된다는 것이었다.
즉, 코드를 그대로 가져다 쓰되, 식을 추출하지 말고 그냥 바로 연산을 해버리면 풀린다는 것이다.
이 풀이를 듣자마자 지금까지 직접 식 추출하면서 풀었던 문제들이 머릿속을 스쳐지나가며 "식을 추출할 필요가 없었구나"라는 생각을 가지게 되었다.

어쨌든 풀이를 알았으니, 한번 구현해보자.
64비트 비트벡터를 4개와 [0] 14개로 채운 리스트를 하나 생성해주고(입력받는 문자의 길이는 최대 32바이트이므로), 위 식을 그대로 코드로 짠다.
그 후, stub에 들어있는 값을 복사해 특정 값에 따라 연산이 처리될 수 있도록 해주면 문제가 풀릴 것이다.

이런 식으로 stub에 들어있는 값을 추출해오고,

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==0x1C:
        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==0x88:
        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==4:
        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==0xDA:
        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==0x4A:
        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==0x25:
        REG[data[it+1]]=~REG[data[it+1]]
        it+=2
    elif res==0x77:
        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==0xF4:
        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]

이렇게 조건문과 식까지 파이썬으로 옮겨주면 준비는 식 추출까진 끝났고,
Solver()를 할당해줘 미지수를 구한다.
그 후, 순서대로 출력하면 플래그가 나올 것이다.

s=Solver()
s.add(REG[0]==0x4635CE5D1658B74C)
s.add(REG[1]==0xE1EC52A29AF4B45F)
s.add(REG[2]==0xBDF35F48B8974554)
s.add(REG[3]==0xC42B5522A0596E41)
print(s.check())
res=s.model()
print(res)
for i in TEMP:
    print(res[i].as_long().to_bytes(8, "little").decode())

이런 식으로 식을 추가해주고, 미지수를 구한 후 리틀엔디언으로 8바이트씩 끊어서 출력하면 플래그가 나온다.

flag : L7{CAN_U_TRANSLATE_VM_BRANCH?}