2022 虎符逆向FBPE复现

拿到程序拖入PE可以发现是一个64位程序，拖入IDA中反编译出来我们可以明显看到有一个BPF program的提示信息

BPF就是实现了一个内核虚拟机，也是ELF格式，通常以文件形式存在或内联编译进程序

参考文章：

http://blog.leanote.com/post/xp0int/2022-虎符网络安全

https://blog.csdn.net/pwl999/article/details/82884882

所以此题的关键就是内联编译的BPF程序

调用顺序：fpbe_bpf__open_and_load -> fpbe_bpf__open -> fpbe_bpf__open_opts -> fpbe_bpf__create_skeleton

我们可以直接手动进行dump下来进行观察该程序内联的一个程序信息，通过一个Github开源的项目，我们可以将其反编译为汇编形式

Github项目链接：

https://github.com/cylance/eBPF_processor

之后将程序选择解析为ebpf

之后可以反编译得到对应的汇编语句

在ida中似乎并不能转换为对应的伪C代码，但是我们可以使用llvm-objdump让其看起来更好看一些

经过翻译可以得到是一个大数约束求解的一个过程，写出对应z3脚本进行约束求解即可

from z3 import *
from Crypto.Util.number import *
r1 = Int('r1')
r2 = Int('r2')
r3 = Int('r3')
r4 = Int('r4')
s = Solver()

s.add(28096*r1+64392*r2+29179*r3+52366*r4 == 209012997183893)
s.add(61887*r1+27365*r2+44499*r3+37508*r4 == 181792633258816)
s.add(56709*r1+32808*r2+25901*r3+59154*r4 == 183564558159267)
s.add(33324*r1+51779*r2+31886*r3+62010*r4 == 204080879923831)

if s.check() == sat:
	flag = b""
	m = s.model()
	for i in [r1, r2, r3, r4]:
		flag += long_to_bytes(m[i].as_long())[::-1]
	print(flag)
# HFCTF{0vR3sAlbs8pD2h53}