Are you bored with x86? Enjoy this x87 VM.
NetFS 2の非想定解に涙こぼれながら解いた。
与えられたバイナリを実行すると、次のようにフラグチェッカーであることがわかる。
pwn@85720d268bb0:~/ctf/fvm$ ./fvm
FLAG: TAPIOKA
NG.
また、このバイナリファイルを読むと、x87をベースにしたVMがC++で実装されていることがわかる。
main関数から以下のfvm::emulateという関数が呼ばれていて、その引数にVMに読み込むバイトコードが与えられる。
fvm::emulateは、そのバイトコードのオペコードを逐次読み込んで実行する。
バイトコードは以下。
23384124435424435473243838414327412443547324383823514343435473232441243843435473233838514343244354732338384343542241732162940162b20162840139053f11f4ff2957810e406503003253323a395e57f3b4a38c7fba07406503003153313a62670162850162570139b77380e1b07287f203406503003253323a393f68a3e4049a3b8f07406503003153313a623a01625801622a01395427b5b695525dcd0b406503003253323a3928919a4aa271379107406503003153313a620d01622b0162fd0039a3861405418c74e50b406503003253323a39bc61edf2e96ec1ab06406503003153313a62e00062fe0062d0003988923ae0693f549206406503003253323a390fd1bee339a196c505406503003153313a62b30062d10062a3003983ea7b97e54cd3ea06406503003253323a3987efb0d15cfe86ad04406503003153313a62860062a4006276003919426cd4caf6f2d909406503003253323a39efffda1513eaaedb06406503003153313a62590062770062490039fe1397dfcd127ef00a406503003253323a391cafcf1f964541a506406503003153313a72233843254124384343546405003a3a637d003a395a883414a0c305bdfe3f648e00636b00323832383243324132617262420072623e00222241234343243841542438434354244354443852424331617262210072621d002222412343432438415424384343542443544438532241315243433161312338432343542241670f00243843244325412443546802003161232543244123384343547323244124384343547322234124384343547363210023224541243838434343547324382623412441434354732338432443547363000023384354737100
VMはシンプルなスタックマシンで、浮動小数点数の算術演算や比較演算、入出力命令などが実装されている。 オペコード数は40個くらい。
いくつか解く手段が考えられるけど、眠かったしオペコード少ないし眠かったしだったので、雑にPythonでエミュレートして条件をシンボリックに列挙する方法を取った。
安定して解ける。
（float80はインターネットに転がってたコード。）
import math
from float80 import float80
with open("fvm", "rb") as f:
fvm = f.read()
code = fvm[0x2004:0x2280]
def u8(x):
return (x + 0x80) % 0x80
class Stack:
def __init__(self):
self.stack = []
def push(self, x):
self.stack.append(x)
def pop(self):
return self.stack.pop()
def swap(self, i, j):
self.stack[-(i + 1)], self.stack[-(j + 1)] = self.stack[-(j + 1)], self.stack[-(i + 1)]
def __getitem__(self, i):
return self.stack[-(i + 1)]
def to_string(self):
return str(self.stack[::-1])
def emulate(input_flag, debug=False) -> list[str]:
initial_flag = input_flag[:]
stack = Stack()
conditions = []
i = 0
count = 0
output = ""
while True:
opcode = code[i]
if debug:
print(f"({count}) {hex(i)[2:]}: {hex(opcode)[2:]}", end=" ")
count += 1
i += 1
# 0x62 ~ 0x70
if u8(opcode - 0x62) <= 0xD:
arg = code[i : i + 2]
if debug:
print("arg", arg.hex(), end=" ")
i += 2
# 0x21 ~ 0x73
if u8(opcode - 0x21) <= 0x52:
match opcode:
case 0x21:
if debug:
print("fldz")
stack.push(0.0)
case 0x22:
if debug:
print("fld1")
stack.push(1.0)
case 0x23:
if debug:
print("fldpi")
stack.push(math.pi)
case 0x24:
if debug:
print("fldl2t")
stack.push(math.log2(10))
case 0x25:
if debug:
print("fldl2e")
stack.push(math.log2(math.e))
case 0x26:
if debug:
print("fldlg2")
stack.push(math.log10(2))
case 0x27:
if debug:
print("fldln2")
stack.push(math.log(2))
case 0x31:
if debug:
print("fxch st0 st1")
stack.swap(0, 1)
case 0x32:
if debug:
print("fxch st0 st2")
stack.swap(0, 2)
case 0x33:
if debug:
print("fxch st0 st3")
stack.swap(0, 3)
case 0x34:
if debug:
print("fxch st0 st4")
stack.swap(0, 4)
case 0x35:
if debug:
print("fxch st0 st5")
stack.swap(0, 5)
case 0x36:
if debug:
print("fxch st0 st6")
stack.swap(0, 6)
case 0x37:
if debug:
print("fxch st0 st7")
stack.swap(0, 7)
case 0x38:
if debug:
print("fst st7")
stack.push(stack[0])
case 0x39:
if debug:
print("fld")
arg = code[i : i + 0xA]
stack.push(float80(arg.hex()))
i += 0xA
case 0x3A:
if debug:
print("ffree")
stack.pop()
# assert False
case 0x41:
if debug:
print("faddp st(1), st")
a, b = stack.pop(), stack.pop()
if type(a) is float and type(b) is float:
stack.push(a + b)
else:
stack.push(f"({a} + {b})")
case 0x42:
if debug:
print("fsubp")
a, b = stack.pop(), stack.pop()
if type(a) is float and type(b) is float:
stack.push(b - a)
else:
stack.push(f"({b} - {a})")
case 0x43:
if debug:
print("fmulp")
a, b = stack.pop(), stack.pop()
if type(a) is float and type(b) is float:
stack.push(a * b)
else:
stack.push(f"({a} * {b})")
case 0x44:
if debug:
print("fdivp")
a, b = stack.pop(), stack.pop()
if type(a) is float and type(b) is float:
stack.push(b / a)
else:
stack.push(f"({b} / {a})")
case 0x45:
if debug:
print("fchs")
stack.push(-stack.pop())
case 0x51:
if debug:
print("fsqrt")
x = stack.pop()
if type(x) is float:
stack.push(math.sqrt(x))
else:
stack.push(f"sqrt({x})")
case 0x52:
if debug:
print("fsin")
x = stack.pop()
if type(x) is float:
stack.push(math.sin(x))
else:
stack.push(f"sin({x})")
case 0x53:
if debug:
print("fcos")
x = stack.pop()
if type(x) is float:
stack.push(math.cos(x))
else:
stack.push(f"cos({x})")
case 0x54:
if debug:
print("frndint")
x = stack.pop()
if type(x) is float:
stack.push(float(round(x)))
else:
stack.push(f"round({x})")
case 0x61:
if debug:
print("fistp QWORD PTR [r13+0x0]")
i = int(stack.pop())
case 0x62:
if debug:
print("fild")
v = int.from_bytes(arg, "little", signed=True)
stack.push(float(i))
i += v
case 0x64:
# sete
condition = f"{stack[0]} != {stack[1]}"
if debug:
print(f"fcomp {condition}")
if type(stack[0]) is float and type(stack[1]) is float:
assert stack[0] == stack[1]
else:
if debug:
print("skip")
conditions.append(condition)
stack.pop()
case 0x65:
# setne: not equalだとZF=0
condition = f"{stack[0]} == {stack[1]}"
if debug:
print(f"fcomp {condition}")
if type(stack[0]) is float and type(stack[1]) is float:
assert stack[0] == stack[1]
else:
if debug:
print("skip")
conditions.append(condition)
stack.pop()
case 0x66:
# setae
condition = f"{stack[0]} <= {stack[1]}"
if debug:
print(f"fcomp {condition}")
if type(stack[0]) is float and type(stack[1]) is float:
assert stack[0] <= stack[1] + 1e-5
else:
if debug:
print("skip")
conditions.append(condition)
stack.pop()
case 0x67:
# seta < じゃないとNG
condition = f"{stack[0]} < {stack[1]}"
if debug:
print(f"fcomp {condition}")
if type(stack[0]) is float and type(stack[1]) is float:
assert stack[0] < stack[1], f"not {condition}"
else:
if debug:
print("skip")
conditions.append(condition)
stack.pop()
case 0x68:
# setbe >= じゃないとNG
condition = f"{stack[0]} >= {stack[1]}"
if debug:
print(f"fcomp {condition}")
if type(stack[0]) is float and type(stack[1]) is float:
assert stack[0] >= stack[1], f"not {condition}"
else:
if debug:
print("skip")
conditions.append(condition)
stack.pop()
case 0x69:
# setb > じゃないとNG
condition = f"{stack[0]} > {stack[1]}"
if debug:
print(f"fcomp {condition}")
if type(stack[0]) is float and type(stack[1]) is float:
assert stack[0] > stack[1], f"not {condition}"
else:
if debug:
print("skip")
conditions.append(condition)
stack.pop()
case 0x71:
break
case 0x72:
if debug:
print("get")
assert len(input_flag) > 0, initial_flag
stack.push(input_flag[0])
input_flag = input_flag[1:]
case 0x73:
if debug:
print("fistp")
output += chr(int(stack.pop()))
if debug:
print(output)
case 0x63:
if debug:
print("END?")
break
case _:
assert False, "unknown opcode end"
else:
assert False, "unknown opcode end"
if debug:
print(" ", stack.to_string())
return conditions
xs = []
for i in range(100):
xs.append("x" + str(i))
# emulate(list(map(float, map(ord, "zer0"))), True)
conditions = emulate(xs, False)
for condition in conditions:
print(condition)フラグの入力を変数にしてシンボリックに実行したところ、次の条件を満たせば良いことがわかった（<と<=などが逆かもしれないが重要じゃないので気にしていない）。
32.0 < x0
127.0 >= x0
32.0 < x1
127.0 >= x1
32.0 < x2
127.0 >= x2
32.0 < x3
127.0 >= x3
33111.16406178876 == (((((6.283185307179586 * x1) / 256.0) - sin(((6.283185307179586 * x1) / 256.0))) * x0) * ((sin(((6.283185307179586 * x3) / 256.0)) * (1.0 + cos(((6.283185307179586 * x3) / 256.0)))) * x2))
372.99647947631337 == (((((6.283185307179586 * x1) / 256.0) - sin(((6.283185307179586 * x1) / 256.0))) * x0) + ((sin(((6.283185307179586 * x3) / 256.0)) * (1.0 + cos(((6.283185307179586 * x3) / 256.0)))) * x2))
32.0 < x4
127.0 >= x4
32.0 < x5
127.0 >= x5
32.0 < x6
127.0 >= x6
32.0 < x7
127.0 >= x7
30.31613672435929 == (((((6.283185307179586 * x5) / 256.0) - sin(((6.283185307179586 * x5) / 256.0))) * x4) * ((sin(((6.283185307179586 * x7) / 256.0)) * (1.0 + cos(((6.283185307179586 * x7) / 256.0)))) * x6))
286.4656377903364 == (((((6.283185307179586 * x5) / 256.0) - sin(((6.283185307179586 * x5) / 256.0))) * x4) + ((sin(((6.283185307179586 * x7) / 256.0)) * (1.0 + cos(((6.283185307179586 * x7) / 256.0)))) * x6))
32.0 < x8
127.0 >= x8
32.0 < x9
127.0 >= x9
32.0 < x10
127.0 >= x10
32.0 < x11
127.0 >= x11
6571.665324618724 == (((((6.283185307179586 * x9) / 256.0) - sin(((6.283185307179586 * x9) / 256.0))) * x8) * ((sin(((6.283185307179586 * x11) / 256.0)) * (1.0 + cos(((6.283185307179586 * x11) / 256.0)))) * x10))
290.4331553329731 == (((((6.283185307179586 * x9) / 256.0) - sin(((6.283185307179586 * x9) / 256.0))) * x8) + ((sin(((6.283185307179586 * x11) / 256.0)) * (1.0 + cos(((6.283185307179586 * x11) / 256.0)))) * x10))
32.0 < x12
127.0 >= x12
32.0 < x13
127.0 >= x13
32.0 < x14
127.0 >= x14
32.0 < x15
127.0 >= x15
7342.568483390512 == (((((6.283185307179586 * x13) / 256.0) - sin(((6.283185307179586 * x13) / 256.0))) * x12) * ((sin(((6.283185307179586 * x15) / 256.0)) * (1.0 + cos(((6.283185307179586 * x15) / 256.0)))) * x14))
171.75559866124001 == (((((6.283185307179586 * x13) / 256.0) - sin(((6.283185307179586 * x13) / 256.0))) * x12) + ((sin(((6.283185307179586 * x15) / 256.0)) * (1.0 + cos(((6.283185307179586 * x15) / 256.0)))) * x14))
32.0 < x16
127.0 >= x16
32.0 < x17
127.0 >= x17
32.0 < x18
127.0 >= x18
32.0 < x19
127.0 >= x19
146.32909261440597 == (((((6.283185307179586 * x17) / 256.0) - sin(((6.283185307179586 * x17) / 256.0))) * x16) * ((sin(((6.283185307179586 * x19) / 256.0)) * (1.0 + cos(((6.283185307179586 * x19) / 256.0)))) * x18))
98.79419880776496 == (((((6.283185307179586 * x17) / 256.0) - sin(((6.283185307179586 * x17) / 256.0))) * x16) + ((sin(((6.283185307179586 * x19) / 256.0)) * (1.0 + cos(((6.283185307179586 * x19) / 256.0)))) * x18))
32.0 < x20
127.0 >= x20
32.0 < x21
127.0 >= x21
32.0 < x22
127.0 >= x22
32.0 < x23
127.0 >= x23
234.82539210270252 == (((((6.283185307179586 * x21) / 256.0) - sin(((6.283185307179586 * x21) / 256.0))) * x20) * ((sin(((6.283185307179586 * x23) / 256.0)) * (1.0 + cos(((6.283185307179586 * x23) / 256.0)))) * x22))
43.38182969121793 == (((((6.283185307179586 * x21) / 256.0) - sin(((6.283185307179586 * x21) / 256.0))) * x20) + ((sin(((6.283185307179586 * x23) / 256.0)) * (1.0 + cos(((6.283185307179586 * x23) / 256.0)))) * x22))
32.0 < x24
127.0 >= x24
32.0 < x25
127.0 >= x25
32.0 < x26
127.0 >= x26
32.0 < x27
127.0 >= x27
1743.5926260136494 == (((((6.283185307179586 * x25) / 256.0) - sin(((6.283185307179586 * x25) / 256.0))) * x24) * ((sin(((6.283185307179586 * x27) / 256.0)) * (1.0 + cos(((6.283185307179586 * x27) / 256.0)))) * x26))
219.6832591942175 == (((((6.283185307179586 * x25) / 256.0) - sin(((6.283185307179586 * x25) / 256.0))) * x24) + ((sin(((6.283185307179586 * x27) / 256.0)) * (1.0 + cos(((6.283185307179586 * x27) / 256.0)))) * x26))
32.0 < x28
127.0 >= x28
32.0 < x29
127.0 >= x29
32.0 < x30
127.0 >= x30
32.0 < x31
127.0 >= x31
3847.879590867423 == (((((6.283185307179586 * x29) / 256.0) - sin(((6.283185307179586 * x29) / 256.0))) * x28) * ((sin(((6.283185307179586 * x31) / 256.0)) * (1.0 + cos(((6.283185307179586 * x31) / 256.0)))) * x30))
165.25496805454867 == (((((6.283185307179586 * x29) / 256.0) - sin(((6.283185307179586 * x29) / 256.0))) * x28) + ((sin(((6.283185307179586 * x31) / 256.0)) * (1.0 + cos(((6.283185307179586 * x31) / 256.0)))) * x30))
125.0 == x324バイトごとに条件式があって、その4バイトを確定させるのはたかだか
Flag: zer0pts{fun_0f_FPU_st4ck_m4ch1n3}