0x00 日常查壳

无壳64位

0x01 加载BPF!

新架构又出现了！一题一个新架构，搜索引擎使用能力还是不太行，还是多google多bing多badiu。

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

原文：

http://blog.leanote.com/post/xp0int/2022-%E8%99%8E%E7%AC%A6%E7%BD%91%E7%BB%9C%E5%AE%89%E5%85%A8

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

于是题目的SHA256当然不是我们的突破点，关键就是内联编译的BPF程序

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

进去4f4018一看，明显的.elf开头，确定是bpf内联程序，大小也给了，直接dump出来

设定大小直接导出

0x02 分析BPF！

IDA装下bpf的插件：https://github.com/cylance/eBPF_processor

拿刚刚dump出的bpf程序即可

然后就可以对着文档分析

https://www.kernel.org/doc/html/latest/bpf/instruction-set.html

或者 llvm-objdump

打下草稿发现是大数约束，直接丢入Z3

0x03 GetFlag!

EXP:

from z3 import *

f = [BitVec('f%d' % i, 32) for i in range(4)]
sol = Solver()

sol.add(f[0] * 52366 + f[1] * 29179 + f[2] * 64392 + f[3] * 28096 == 209012997183893)
sol.add(f[0] * 37508 + f[1] * 44499 + f[2] * 27365 + f[3] * 61887 == 181792633258816)
sol.add(f[0] * 59154 + f[1] * 25901 + f[2] * 32808 + f[3] * 56709 == 183564558159267)
sol.add(f[0] * 62010 + f[1] * 31886 + f[2] * 51779 + f[3] * 33324 == 204080879923831)

if sat == sol.check():
    s =  sol.model()
    flag = [s[f[i]].as_long().to_bytes(4, 'little').decode() for i in range(4)]
    print("HFCTF{" + ''.join(flag[::-1]) + "}")
    # 由于正反序都不确定于是都试下即可
    # sol.add(Or([f[i] != s[f[i]] for i in range(4)]))

GetFlag!