0%

wp

2025-08-29 04:05By
niuyi
Reverse动态调试Z3

Problem: [虎符CTF 2022]fpbe

思路

1.打开ida发现使用了eBPF框架编写的程序,需要我们找到其中的可以找到加载进内核的 ebfp程序的二进制数据
NSSIMAGE
2.这个程序一般在main -> Berkeley_bpfopen_and_load -> Berkeley_bpf__open -> Berkeley_bpfopen_opts -> Berkeley_bpfcreate_skeleton -> Berkeley_bpfelf_bytes 这个路径下
NSSIMAGE
3.找到存储程序的地址和文件的大小为 1648,使用idapython dump出来,但是ida不能识别ebpf框架编写的程序,需要使用ghidra来进行分析
NSSIMAGE
是对我们输入的flag进行校验

EXP

from z3 import *
import binascii
a=[]
for i in range(4):
a.append(Int(f'a[{i}]'))
s=Solver()
s.add(a[1] * 0xfb88 + a[2] * 0x6dc0 + a[3] * 0x71fb + a[0] * 0xcc8e == 0xbe18a1735995)
s.add(a[1] * 0x6ae5 + a[2] * 0xf1bf + a[3] * 0xadd3 + a[0] * 0x9284 == 0xa556e5540340)
s.add(a[1] * 0x8028 + a[2] * 0xdd85 + a[3] * 0x652d + a[0] * 0xe712 == 0xa6f374484da3)
s.add(a[1] * 0xca43 + a[2] * 0x822c + a[3] * 0x7c8e + a[0] * 0xf23a == 0xb99c485a7277)
if s.check()==sat:
m=s.model()
v=[]
for i in a:
v.append(int(str(m[i])))
byte1=binascii.unhexlify(hex(v[0])[2:]).decode()#b'0vR3sAlbs8pD2h53'
byte2 = binascii.unhexlify(hex(v[3])[2:]).decode()
byte3 = binascii.unhexlify(hex(v[2])[2:]).decode()
byte4 = binascii.unhexlify(hex(v[1])[2:]).decode()
byte=byte1+byte2+byte4+byte3
print(byte[::-1],end='')

总结

  • 对该题的考点总结
还没有人赞赏,快来当第一个赞赏的人吧!
  
© 著作权归作者所有
加载失败
广告
×
评论区
添加新评论