prob-3
__int64 __fastcall run_cpu(unsigned __int64 *a1)
{
__int64 result; // rax
__int64 v2; // rsi
unsigned __int64 *v3; // rdx
unsigned __int64 *v4; // rdx
unsigned __int64 *v5; // rdx
unsigned __int64 *v6; // rdx
unsigned __int64 *v7; // rdx
unsigned __int64 *v8; // rdx
unsigned __int64 *v9; // rax
unsigned __int64 *v10; // rdx
unsigned __int64 *v11; // rdx
unsigned __int8 v12; // [rsp+9h] [rbp-Fh]
unsigned __int8 v13; // [rsp+9h] [rbp-Fh]
unsigned __int8 v14; // [rsp+9h] [rbp-Fh]
unsigned __int8 v15; // [rsp+9h] [rbp-Fh]
unsigned __int8 v16; // [rsp+9h] [rbp-Fh]
unsigned __int8 v17; // [rsp+9h] [rbp-Fh]
unsigned __int8 v18; // [rsp+9h] [rbp-Fh]
unsigned __int8 v19; // [rsp+Ah] [rbp-Eh]
unsigned __int8 v20; // [rsp+Bh] [rbp-Dh]
int v21; // [rsp+Ch] [rbp-Ch]
v21 = 0;
while ( 1 )
{
result = stub[v21];
if ( (_BYTE)result == 0xCC )
break;
switch ( stub[v21] )
{
case 0x88:
result = stub[v21 + 1];
v12 = stub[v21 + 1];
if ( v12 )
{
if ( v12 == 1 )
{
a1[stub[v21 + 2]] = *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v12 != 2 )
return result;
a1[stub[v21 + 2]] = *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
a1[stub[v21 + 2]] = a1[stub[v21 + 3]];
v21 += 4;
}
break;
case 4u:
result = stub[v21 + 1];
v13 = stub[v21 + 1];
if ( v13 )
{
if ( v13 == 1 )
{
a1[stub[v21 + 2]] += *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v13 != 2 )
return result;
a1[stub[v21 + 2]] += *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
a1[stub[v21 + 2]] += a1[stub[v21 + 3]];
v21 += 4;
}
break;
case 0xDA:
result = stub[v21 + 1];
v14 = stub[v21 + 1];
if ( v14 )
{
if ( v14 == 1 )
{
v3 = &a1[stub[v21 + 2]];
*v3 -= *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v14 != 2 )
return result;
v4 = &a1[stub[v21 + 2]];
*v4 -= *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
v2 = stub[v21 + 2];
a1[v2] -= a1[stub[v21 + 3]];
v21 += 4;
}
break;
case 0x1Cu:
result = stub[v21 + 1];
v15 = stub[v21 + 1];
if ( v15 )
{
if ( v15 == 1 )
{
v5 = &a1[stub[v21 + 2]];
*v5 &= *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v15 != 2 )
return result;
v6 = &a1[stub[v21 + 2]];
*v6 &= *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
a1[stub[v21 + 2]] &= a1[stub[v21 + 3]];
v21 += 4;
}
break;
case 0x4Au:
result = stub[v21 + 1];
v16 = stub[v21 + 1];
if ( v16 )
{
if ( v16 == 1 )
{
v7 = &a1[stub[v21 + 2]];
*v7 |= *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v16 != 2 )
return result;
v8 = &a1[stub[v21 + 2]];
*v8 |= *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
a1[stub[v21 + 2]] |= a1[stub[v21 + 3]];
v21 += 4;
}
break;
case 0x25u:
v9 = &a1[stub[v21 + 1]];
*v9 = ~*v9;
v21 += 2;
break;
case 0x77u:
result = stub[v21 + 1];
v17 = stub[v21 + 1];
if ( v17 )
{
if ( v17 == 1 )
{
v10 = &a1[stub[v21 + 2]];
*v10 ^= *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v17 != 2 )
return result;
v11 = &a1[stub[v21 + 2]];
*v11 ^= *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
a1[stub[v21 + 2]] ^= a1[stub[v21 + 3]];
v21 += 4;
}
break;
case 0xF4:
v19 = stub[v21 + 1];
v20 = stub[v21 + 2];
a1[16] = a1[v19] == a1[v20];
a1[17] = v19 > v20;
v21 += 3;
break;
default:
result = stub[v21];
if ( (_BYTE)result != 64 )
return result;
result = stub[v21 + 1];
v18 = stub[v21 + 1];
if ( v18 )
{
if ( v18 == 1 )
{
if ( a1[16] == 1 )
v21 = (unsigned __int8)*(_QWORD *)&stub[v21 + 2];
else
v21 += 10;
}
else
{
if ( v18 != 2 )
return result;
if ( a1[16] )
v21 += 10;
else
v21 = (unsigned __int8)*(_QWORD *)&stub[v21 + 2];
}
}
else
{
v21 = (unsigned __int8)*(_QWORD *)&stub[v21 + 2];
}
break;
}
}
return result;
}
구조 자체는 기존의 문제와 비슷하다. 한가지 차이점은 0xF4 opcode에서 특정 인덱스의 값을 세팅해주고 default에서 그 값에 따라서 분기를 하는 분기문이 구현되어 있다는 것이다. 어떻게 해야될까 고민을 조금 했는데 그냥 배열 하나 만들어두고 vm에서 하는 연산을 똑같이 하면 분기 결과를 알 수 있지 않을까? 라는 추측을 했고 실제로 했더니 정상적으로 연산식이 추출이 되었다. 여기서 더 나아가서 굳이 연산식을 추출하고 추출 결과에 z3를 돌리지 않고 그냥 추출하는 동시에 z3를 같이 돌려줘도 된다는 사실을 깨닫고 한번에 플래그를 얻어줬다.
from z3 import *
from pwn import *
vm = [0x88, 0x01, 0x07, 0x20, 0x00, 0x00, 0x00, 0x88, 0x01, 0x08, 0x00, 0x00, 0x00, 0x00, 0xDA, 0x02, 0x0A, 0x8A, 0xD6, 0xBA, 0x0C, 0xE0, 0xE7, 0x12, 0x4C, 0x77, 0x02, 0x0A, 0x07, 0x05, 0x29, 0x3C, 0x36, 0x57, 0x27, 0x44, 0x04, 0x02, 0x0A, 0xF2, 0x4D, 0xE8, 0x6B, 0x35, 0xA9, 0x51, 0xE6, 0x25, 0x0A, 0x77, 0x00, 0x00, 0x0A, 0xDA, 0x02, 0x0B, 0x78, 0x8F, 0x59, 0x48, 0xC3, 0x01, 0xEC, 0xA0, 0x77, 0x02, 0x0B, 0x98, 0xEE, 0xCF, 0xA8, 0x5B, 0xCA, 0x13, 0xC5, 0x04, 0x02, 0x0B, 0xF9, 0x65, 0xEB, 0x45, 0x9A, 0x63, 0xC5, 0xF4, 0x25, 0x0B, 0x04, 0x00, 0x00, 0x0B, 0xDA, 0x02, 0x0C, 0xEE, 0x28, 0xC6, 0x2B, 0xCB, 0xDB, 0x80, 0x1E, 0x77, 0x02, 0x0C, 0x69, 0x6A, 0x7F, 0xBE, 0x39, 0xA1, 0x96, 0x56, 0x04, 0x02, 0x0C, 0xC3, 0x88, 0xFB, 0x35, 0x6B, 0x7C, 0x5F, 0xA1, 0x25, 0x0C, 0xDA, 0x00, 0x00, 0x0B, 0xDA, 0x02, 0x0A, 0x9E, 0x4B, 0x3C, 0x30, 0x6A, 0xBE, 0xFE, 0x83, 0x77, 0x02, 0x0A, 0x63, 0x8A, 0x7D, 0x7E, 0x41, 0xFD, 0xB4, 0xA9, 0x04, 0x02, 0x0A, 0xB1, 0x9A, 0x8A, 0x58, 0x9D, 0xBE, 0xA9, 0x9D, 0x25, 0x0A, 0x77, 0x00, 0x01, 0x0A, 0xDA, 0x02, 0x0B, 0x9A, 0x00, 0xC1, 0x6C, 0x4B, 0xA0, 0x16, 0x9E, 0x77, 0x02, 0x0B, 0x4E, 0xAC, 0x03, 0x7A, 0xB7, 0x8C, 0x84, 0x3F, 0x04, 0x02, 0x0B, 0xB8, 0x7D, 0x9D, 0xE5, 0x98, 0x9B, 0xD6, 0xEC, 0x25, 0x0B, 0x04, 0x00, 0x01, 0x0B, 0xDA, 0x02, 0x0C, 0xF8, 0xD3, 0x70, 0xDB, 0x32, 0xAB, 0xD9, 0x1C, 0x77, 0x02, 0x0C, 0x6A, 0xC9, 0x00, 0x92, 0xE0, 0xEF, 0x11, 0x29, 0x04, 0x02, 0x0C, 0xF5, 0xF3, 0xA4, 0x67, 0x9D, 0xE9, 0x8D, 0x94, 0x25, 0x0C, 0xDA, 0x00, 0x01, 0x0B, 0xDA, 0x02, 0x0A, 0x24, 0x54, 0x77, 0xBA, 0x22, 0xD3, 0x19, 0x14, 0x77, 0x02, 0x0A, 0xC9, 0xF7, 0xE7, 0x89, 0x6B, 0x83, 0x21, 0x0F, 0x04, 0x02, 0x0A, 0x48, 0xD1, 0x69, 0x61, 0x89, 0x5C, 0x1D, 0x3A, 0x25, 0x0A, 0x77, 0x00, 0x02, 0x0A, 0xDA, 0x02, 0x0B, 0x76, 0xC4, 0x87, 0x5A, 0xA9, 0xA5, 0x95, 0xEA, 0x77, 0x02, 0x0B, 0x26, 0xCD, 0x73, 0xCD, 0xAA, 0xAD, 0x5C, 0xCF, 0x04, 0x02, 0x0B, 0xF3, 0x1A, 0x8D, 0x49, 0x66, 0x12, 0xE4, 0x7C, 0x25, 0x0B, 0x04, 0x00, 0x02, 0x0B, 0xDA, 0x02, 0x0C, 0x90, 0xD3, 0xCE, 0xA1, 0xBB, 0x4C, 0x68, 0x07, 0x77, 0x02, 0x0C, 0xE2, 0xF8, 0x9D, 0x0C, 0xB7, 0xAC, 0x53, 0xBF, 0x04, 0x02, 0x0C, 0xDB, 0x3E, 0x89, 0xB6, 0x16, 0xAA, 0x4E, 0x9E, 0x25, 0x0C, 0xDA, 0x00, 0x02, 0x0B, 0xDA, 0x02, 0x0A, 0xDF, 0xB7, 0xED, 0x2F, 0xA7, 0xBF, 0x90, 0x30, 0x77, 0x02, 0x0A, 0x75, 0x75, 0x81, 0x4D, 0x2B, 0x45, 0x7C, 0x2F, 0x04, 0x02, 0x0A, 0x9E, 0x99, 0x4B, 0x4B, 0xA0, 0x71, 0xEB, 0xEB, 0x25, 0x0A, 0x77, 0x00, 0x03, 0x0A, 0xDA, 0x02, 0x0B, 0x57, 0x66, 0xA9, 0x7B, 0xCC, 0x0A, 0x5E, 0xB5, 0x77, 0x02, 0x0B, 0x75, 0xE2, 0x8E, 0x77, 0x49, 0xB7, 0x5E, 0xE6, 0x04, 0x02, 0x0B, 0x9F, 0xF6, 0xB4, 0x71, 0xD2, 0xE5, 0x48, 0xD7, 0x25, 0x0B, 0x04, 0x00, 0x03, 0x0B, 0xDA, 0x02, 0x0C, 0x9F, 0x04, 0x59, 0xA3, 0xC8, 0xB8, 0xA3, 0x7F, 0x77, 0x02, 0x0C, 0x08, 0xDB, 0x05, 0x60, 0xEB, 0x3F, 0xCF, 0xEB, 0x04, 0x02, 0x0C, 0xE5, 0x2B, 0xE3, 0xC1, 0x94, 0xAA, 0x48, 0xB1, 0x25, 0x0C, 0xDA, 0x00, 0x03, 0x0B, 0x04, 0x01, 0x08, 0x01, 0x00, 0x00, 0x00, 0xF4, 0x07, 0x08, 0x40, 0x02, 0x0E, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xCC]
idx = 0
FLAG = [BitVec('a%i'%i, 64) for i in range(4)]
a1 = [x for x in FLAG]+[0]*14
s = Solver()
while True:
opcode = vm[idx]
if opcode == 0xCC:
break
elif opcode == 0x88:
v12 = vm[idx+1]
if v12:
if v12 == 1:
a1[vm[idx+2]] = int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] = 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v12 == 2:
a1[vm[idx+2]] = int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] = 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] = REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] = a1[vm[idx+3]]
idx += 4
elif opcode == 4:
v13 = vm[idx+1]
if v13:
if v13 == 1:
a1[vm[idx+2]] += int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] += 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v13 == 2:
a1[vm[idx+2]] += int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] += 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] += REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] += a1[vm[idx+3]]
idx += 4
elif opcode == 0xDA:
v14 = vm[idx+1]
if v14:
if v14 == 1:
a1[vm[idx+2]] -= int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] -= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v14 == 2:
a1[vm[idx+2]] -= int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] -= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] -= REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] -= a1[vm[idx+3]]
idx += 4
elif opcode == 0x1C:
v15 = vm[idx+1]
if v15:
if v15 == 1:
a1[vm[idx+2]] &= int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] &= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v15 == 2:
a1[vm[idx+2]] &= int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] &= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] &= REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] &= a1[vm[idx+3]]
idx += 4
elif opcode == 0x4A:
v16 = vm[idx+1]
if v16:
if v16 == 1:
a1[vm[idx+2]] |= int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] |= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v16 == 2:
a1[vm[idx+2]] |= int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] |= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] |= REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] |= a1[vm[idx+3]]
idx += 4
elif opcode == 0x25:
a1[vm[idx+1]] = ~a1[vm[idx+1]]
print("REG[%d] = ~REG[%d]" % (vm[idx+1], vm[idx+1]))
idx += 2
elif opcode == 0x77:
v17 = vm[idx+1]
if v17:
if v17 == 1:
a1[vm[idx+2]] ^= int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] ^= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v17 == 2:
a1[vm[idx+2]] ^= int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] ^= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] ^= REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] ^= a1[vm[idx+3]]
idx += 4
elif opcode == 0xF4:
v19 = vm[idx+1]
v20 = vm[idx+2]
a1[16] = a1[v19] == a1[v20]
a1[17] = v19 > v20
idx += 3
else:
res = vm[idx]
if res != 64:
break
v18 = vm[idx+1]
if v18:
if v18 == 1:
if a1[16] == 1:
idx = vm[idx+2]
else:
idx += 10
else:
if v18 != 2:
break
if a1[16]:
idx += 10
else:
idx = vm[idx+2]
else:
idx = vm[idx+2]
s.add(a1[0] == 0x4635CE5D1658B74C)
s.add(a1[1] == 0xE1EC52A29AF4B45F)
s.add(a1[2] == 0xBDF35F48B8974554)
s.add(a1[3] == 0xC42B5522A0596E41)
if s.check() == sat:
res = s.model()
for i in FLAG:
print(p64(int(str(res[i]))).decode(), end='')
이렇게 vm을 돌리는 동시에 z3를 같이 돌려주면 한번에 플래그가 나오게 된다.
prob-4
__int64 __fastcall run_cpu(unsigned __int64 *a1)
{
__int64 result; // rax
__int64 v2; // rsi
unsigned __int64 *v3; // rdx
unsigned __int64 *v4; // rdx
unsigned __int64 *v5; // rdx
unsigned __int64 *v6; // rdx
unsigned __int64 *v7; // rdx
unsigned __int64 *v8; // rdx
unsigned __int64 *v9; // rax
unsigned __int64 *v10; // rdx
unsigned __int64 *v11; // rdx
unsigned __int8 v12; // [rsp+9h] [rbp-Fh]
unsigned __int8 v13; // [rsp+9h] [rbp-Fh]
unsigned __int8 v14; // [rsp+9h] [rbp-Fh]
unsigned __int8 v15; // [rsp+9h] [rbp-Fh]
unsigned __int8 v16; // [rsp+9h] [rbp-Fh]
unsigned __int8 v17; // [rsp+9h] [rbp-Fh]
unsigned __int8 v18; // [rsp+9h] [rbp-Fh]
unsigned __int8 v19; // [rsp+Ah] [rbp-Eh]
unsigned __int8 v20; // [rsp+Bh] [rbp-Dh]
int v21; // [rsp+Ch] [rbp-Ch]
v21 = 0;
while ( 1 )
{
result = stub[v21];
if ( (_BYTE)result == 0xCC )
break;
switch ( stub[v21] )
{
case 0x16u:
result = stub[v21 + 1];
v12 = stub[v21 + 1];
if ( v12 )
{
if ( v12 == 1 )
{
a1[stub[v21 + 2]] = *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v12 != 2 )
return result;
a1[stub[v21 + 2]] = *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
a1[stub[v21 + 2]] = a1[stub[v21 + 3]];
v21 += 4;
}
break;
case 0x5Du:
result = stub[v21 + 1];
v13 = stub[v21 + 1];
if ( v13 )
{
if ( v13 == 1 )
{
a1[stub[v21 + 2]] += *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v13 != 2 )
return result;
a1[stub[v21 + 2]] += *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
a1[stub[v21 + 2]] += a1[stub[v21 + 3]];
v21 += 4;
}
break;
case 0xE0:
result = stub[v21 + 1];
v14 = stub[v21 + 1];
if ( v14 )
{
if ( v14 == 1 )
{
v3 = &a1[stub[v21 + 2]];
*v3 -= *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v14 != 2 )
return result;
v4 = &a1[stub[v21 + 2]];
*v4 -= *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
v2 = stub[v21 + 2];
a1[v2] -= a1[stub[v21 + 3]];
v21 += 4;
}
break;
default:
if ( stub[v21] )
{
switch ( stub[v21] )
{
case 0xB2:
result = stub[v21 + 1];
v16 = stub[v21 + 1];
if ( v16 )
{
if ( v16 == 1 )
{
v7 = &a1[stub[v21 + 2]];
*v7 |= *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v16 != 2 )
return result;
v8 = &a1[stub[v21 + 2]];
*v8 |= *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
a1[stub[v21 + 2]] |= a1[stub[v21 + 3]];
v21 += 4;
}
break;
case 0x78u:
v9 = &a1[stub[v21 + 1]];
*v9 = ~*v9;
v21 += 2;
break;
case 0x3Bu:
result = stub[v21 + 1];
v17 = stub[v21 + 1];
if ( v17 )
{
if ( v17 == 1 )
{
v10 = &a1[stub[v21 + 2]];
*v10 ^= *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v17 != 2 )
return result;
v11 = &a1[stub[v21 + 2]];
*v11 ^= *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
a1[stub[v21 + 2]] ^= a1[stub[v21 + 3]];
v21 += 4;
}
break;
case 0xB3:
v19 = stub[v21 + 1];
v20 = stub[v21 + 2];
a1[16] = a1[v19] == a1[v20];
a1[17] = v19 > v20;
v21 += 3;
break;
default:
result = stub[v21];
if ( (_BYTE)result != 33 )
return result;
result = stub[v21 + 1];
v18 = stub[v21 + 1];
if ( v18 )
{
if ( v18 == 1 )
{
if ( a1[16] == 1 )
v21 = (unsigned __int8)*(_QWORD *)&stub[v21 + 2];
else
v21 += 10;
}
else
{
if ( v18 != 2 )
return result;
if ( a1[16] )
v21 += 10;
else
v21 = (unsigned __int8)*(_QWORD *)&stub[v21 + 2];
}
}
else
{
v21 = (unsigned __int8)*(_QWORD *)&stub[v21 + 2];
}
break;
}
}
else
{
result = stub[v21 + 1];
v15 = stub[v21 + 1];
if ( v15 )
{
if ( v15 == 1 )
{
v5 = &a1[stub[v21 + 2]];
*v5 &= *(unsigned int *)&stub[v21 + 3];
v21 += 7;
}
else
{
if ( v15 != 2 )
return result;
v6 = &a1[stub[v21 + 2]];
*v6 &= *(_QWORD *)&stub[v21 + 3];
v21 += 11;
}
}
else
{
a1[stub[v21 + 2]] &= a1[stub[v21 + 3]];
v21 += 4;
}
}
break;
}
}
return result;
}
앞의 문제와 큰 틀은 비슷하다. 분기문이 구현된 형태도 유사한데 약간의 차이점이 있다면 이 문제는 default후에 다시 case문을 실행한다는 것이다. 이거 말고는 앞의 문제와 완전히 똑같은 방식으로 풀린다. 딱히 할 말이 없다.
from pwn import *
from z3 import *
vm = [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]
idx = 0
FLAG = [BitVec('a%i'%i, 64) for i in range(4)]
a1 = [x for x in FLAG]+[0]*14
s = Solver()
while True:
opcode = vm[idx]
if opcode == 0xCC:
break
elif opcode == 0x16:
v12 = vm[idx+1]
if v12:
if v12 == 1:
a1[vm[idx+2]] = int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] = 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v12 == 2:
a1[vm[idx+2]] = int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] = 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] = REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] = a1[vm[idx+3]]
idx += 4
elif opcode == 0x5D:
v13 = vm[idx+1]
if v13:
if v13 == 1:
a1[vm[idx+2]] += int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] += 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v13 == 2:
a1[vm[idx+2]] += int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] += 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] += REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] += a1[vm[idx+3]]
idx += 4
elif opcode == 0xE0:
v14 = vm[idx+1]
if v14:
if v14 == 1:
a1[vm[idx+2]] -= int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] -= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v14 == 2:
a1[vm[idx+2]] -= int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] -= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] -= REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] -= a1[vm[idx+3]]
idx += 4
else:
if vm[idx]:
if opcode == 0xB2:
v16 = vm[idx+1]
if v16:
if v16 == 1:
a1[vm[idx+2]] |= int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] |= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v16 == 2:
a1[vm[idx+2]] |= int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] |= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] |= REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] |= a1[vm[idx+3]]
idx += 4
elif opcode == 0x78:
a1[vm[idx+1]] = ~a1[vm[idx+1]]
print("REG[%d] = ~REG[%d]" % (vm[idx+1], vm[idx+1]))
idx += 2
elif opcode == 0x3B:
v17 = vm[idx+1]
if v17:
if v17 == 1:
a1[vm[idx+2]] ^= int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] ^= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v17 == 2:
a1[vm[idx+2]] ^= int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] ^= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] ^= REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] ^= a1[vm[idx+3]]
idx += 4
elif opcode == 0xB3:
v19 = vm[idx+1]
v20 = vm[idx+2]
a1[16] = a1[v19] == a1[v20]
a1[17] = v19 > v20
idx += 3
else:
res = vm[idx]
if res != 33:
break
v18 = vm[idx+1]
if v18:
if v18 == 1:
if a1[16] == 1:
idx = vm[idx+2]
else:
idx += 10
else:
if v18 != 2:
break
if a1[16]:
idx += 10
else:
idx = vm[idx+2]
else:
idx = vm[idx+2]
else:
v15 = vm[idx+1]
if v15:
if v15 == 1:
a1[vm[idx+2]] &= int.from_bytes(vm[idx+3:idx+3+4], "little")
print("REG[%d] &= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+4], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 7
elif v15 == 2:
a1[vm[idx+2]] &= int.from_bytes(vm[idx+3:idx+3+8], "little")
print("REG[%d] &= 0x%08X" % (vm[idx+2], int.from_bytes(vm[idx+3:idx+3+8], "little")))
print("REG[%d] &= 0xFFFFFFFFFFFFFFFF" % vm[idx+2])
a1[vm[idx+2]] &= 0xFFFFFFFFFFFFFFFF
idx += 11
else:
print("REG[%d] &= REG[%d]" % (vm[idx+2], vm[idx+3]))
a1[vm[idx+2]] &= a1[vm[idx+3]]
idx += 4
s.add(a1[0] == 0x7ECB527EEABB074C)
s.add(a1[1] == 0xE635AE1A1123CE4F)
s.add(a1[2] == 0x61467F6C95358D52)
s.add(a1[3] == 0x1FA186EA0DBF462E)
if s.check() == sat:
res = s.model()
for i in FLAG:
print(p64(int(str(res[i]))).decode(), end='')
이런식으로 풀 수 있다. 사실 두 문제 모두 반복문이 구현되어 있는 형태라 연산식이 매우 길게 나와서 이렇게 풀면 비효율적이고 mov, add, xor과 같은 어셈블리 instruction으로 직관화 한 후에 간소화 하는게 정석이라는데 일단 이 두문제는 이렇게 무지성으로 때려넣어도 풀릴만할것 같아서 그냥 무지성으로 풀었다.
'Layer7' 카테고리의 다른 글
| Layer7 - 포너블 1차시 과제 (0) | 2022.10.04 |
|---|---|
| Layer7 - 포너블 1차시 수업 (0) | 2022.10.04 |
| Layer7 - 리버싱 10차시 과제 (0) | 2022.10.04 |
| Layer7 - 리버싱 9차시 과제 (0) | 2022.10.04 |
| Layer7 - 리버싱 8차시 과제 rev-basic-8 (0) | 2022.10.04 |
