解题过程

IDA打开，函数很多，而且全是sub_ 没有符号，查看下字符串，看到了/flag /check,还有很多oatpp3的字符串，查了下，这是个C++的web库和名字很符合，先编译一份，参考

编译完使用IDA打开，然后bindiff导入，全选导入符号，有的可能不准，能好看点就行，先打开我们自己编译的hello，world 我们的程序访问hello是有回显的，交叉引用找过去，这个函数看名字就挺像响应的

然后去题目里面找函数，虽然恢复了符号，但是函数的名称怪怪的，不是这种otapp::的格式，中间没有分割。搜索createResponse，找到两个，点进去，然后找交叉引用，看哪个比较像加密

第三个sub_40617E，一个大数组，后面是计算，一看就很像加密

这里大概就是两个数组，类似矩阵乘法，然后最后再遍历一遍，有个IF判断是否是0，如果是0就跳到正确的分支，使用Z3可以直接求解出来，

z3的一些语法

#创建了一个Solver对象s，用于解决后续添加的约束
s=Solver()
#添加约束条件
s.add(enc[i]==0)
#sat表示“满足的”或“可解的”，意味着所有约束都可以同时满足，并存在一个解决方案。
s.check()==sat
#获取解决方案
m = s.model()
​
​
.as_long()  从Z3模型中提取出的整数值。

solever.py

from z3 import *
key=[0x00000017, 0x0000000D, 0x00000004, 0x00000030, 0x00000029, 0x00000029, 0x0000002A, 0x00000021, 0x0000001E, 0x00000003, 0x00000045, 0x00000001, 0x0000000D, 0x0000002D, 0x00000029, 0x00000040, 0x00000008, 0x00000050, 0x0000000F, 0x0000002A, 0x00000038, 0x00000013, 0x0000003E, 0x00000046, 0x00000017, 0x0000003F, 0x0000001E, 0x00000044, 0x00000011, 0x00000038, 0x0000005C, 0x0000000C, 0x00000010, 0x00000040, 0x0000001F, 0x00000003, 0x00000011, 0x00000047, 0x0000003A, 0x00000009, 0x00000040, 0x00000053, 0x00000047, 0x00000034, 0x00000063, 0x00000059, 0x0000004C, 0x00000044, 0x00000001, 0x00000063, 0x00000010, 0x00000010, 0x00000034, 0x0000002B, 0x00000000, 0x0000002C, 0x00000032, 0x00000020, 0x00000032, 0x0000001F, 0x00000014, 0x0000003F, 0x00000002, 0x00000063, 0x00000000, 0x00000039, 0x0000004F, 0x0000002B, 0x00000047, 0x00000013, 0x00000050, 0x0000005C, 0x0000005D, 0x0000003A, 0x00000054, 0x0000004A, 0x00000051, 0x0000002D, 0x00000037, 0x00000015, 0x00000001, 0x00000063, 0x0000001E, 0x0000001C, 0x00000038, 0x00000001, 0x0000000C, 0x0000004D, 0x0000005C, 0x00000004, 0x00000025, 0x00000043, 0x0000003C, 0x00000036, 0x00000033, 0x0000004F, 0x00000026, 0x00000057, 0x00000030, 0x00000010]
enc=[0]*40
enc[0] = 33211
enc[1] = 36113
enc[2] = 28786
enc[3] = 44634
enc[4] = 30174
enc[5] = 39163
enc[6] = 34923
enc[7] = 44333
enc[8] = 33574
enc[9] = 23555
enc[10] = 35015
enc[11] = 42724
enc[12] = 34160
enc[13] = 49166
enc[14] = 35770
enc[15] = 45984
enc[16] = 39754
enc[17] = 51672
enc[18] = 38323
enc[19] = 27511
enc[20] = 31334
enc[21] = 34214
enc[22] = 28014
enc[23] = 41090
enc[24] = 29258
enc[25] = 37905
enc[26] = 33777
enc[27] = 39812
enc[28] = 29442
enc[29] = 22225
enc[30] = 30853
enc[31] = 35330
enc[32] = 30393
enc[33] = 41247
enc[34] = 30439
enc[35] = 39434
enc[36] = 31587
enc[37] = 46815
enc[38] = 35205
enc[39] = 20689
inp = [Int('inp%d' % i) for i in range(len(enc))]
s=Solver()
flag=''
for k in range(4):
    for m in range(10):
        for n in range(10):
            enc[10 * k + m] -=inp[10 * k +  n] * key[10 * n + m]
for i in range(len(enc)):
    s.add(enc[i]==0)
​
if s.check()==sat:
    m=s.model()
    for i in range(40):
        flag+=chr(m[inp[i]].as_long())
    print(flag)