约束求解与符号执行在逆向中应用

笔记

angrEXP.py

1
2
3
4
5
6
7
8
9
10
11
12
import angr,sys
path="D:\\CTF-Workbench\\signal.exe"
project=angr.Project(path,auto_load_libs=False)
initial_state=project.factory.entry_state()
simulation=project.factory.simulation_manager(initial_state)
simulation.explore(find=0x0040179E,avoid=0x004016E6)
if simulation.found:
    for i in simulation.found:
        solution_state=i
        print(solution_state.posix.dumps(0))
else:
    print("no\n")

做题

[GDOUCTF 2023]Check_Your_Luck

解这个方程组：

$$
\displaylines{
\displaystyle
\begin{cases}
23v-32w+98x+55y+90z=333322\\
123v-322w+69x+67y+32z=707724\\
266v-34w+43x+8y+32z=1272529\\
343v-352w+58x+65y+5z=1672457\\
231v-321w+938x+555y+970z=3372367
\end{cases}
}
$$
没有找到合适的chatgpt…都很蠢…于是z3

1
2
3
4
5
6
7
8
9
10
from z3 import *
s = Solver()
v , w, x, y ,z = Ints('v w x y z')
s.add(v * 23 + w * -32 + x * 98 + y * 55 + z * 90 == 333322)
s.add(v * 123 + w * -322 + x * 68 + y * 67 + z * 32 == 707724)
s.add(v * 266 + w * -34 + x * 43 + y * 8 + z * 32 == 1272529)
s.add(v * 343 + w * -352 + x * 58 + y * 65 + z * 5 == 1672457)
s.add(v * 231 + w * -321 + x * 938 + y * 555 + z * 970 == 3372367)
if s.check() == sat:
    print(s.model())

[羊城杯 2020]login

python逆向，z3求解：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
from z3 import *
a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14=Ints('a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14')
sol=Solver()
sol.add(a1*88+a2*67+a3*65-a4*5+a5*43+a6*89+a7*25+a8*13-a9*36+a10*15+a11*11+a12*47-a13*60+a14*29==22748)
sol.add(a1*89+a2*7+a3*12-a4*25+a5*41+a6*23+a7*20-a8*66+a9*31+a10*8+a11*2-a12*41-a13*39+a14*17==7258)
sol.add(a1*28+a2*35+a3*16-a4*65+a5*53+a6*39+a7*27+a8*15-a9*33+a10*13+a11*101+a12*90-a13*34+a14*23==26190)
sol.add(a1*23+a2*34+a3*35-a4*59+a5*49+a6*81+a7*25+a8*128-a9*32+a10*75+a11*81+a12*47-a13*60+a14*29==37136)
sol.add(a1*38+a2*97+a3*35-a4*52+a5*42+a6*79+a7*90+a8*23-a9*36+a10*57+a11*81+a12*42-a13*62-a14*11==27915)
sol.add(a1*22+a2*27+a3*35-a4*45+a5*47+a6*49+a7*29+a8*18-a9*26+a10*35+a11*41+a12*40-a13*61+a14*28==17298)
sol.add(a1*12+a2*45+a3*35-a4*9-a5*42+a6*86+a7*23+a8*85-a9*47+a10*34+a11*76+a12*43-a13*44+a14*65==19875)
sol.add(a1*79+a2*62+a3*35-a4*85+a5*33+a6*79+a7*86+a8*14-a9*30+a10*25+a11*11+a12*57-a13*50-a14*9==22784)
sol.add(a1*8+a2*6+a3*64-a4*85+a5*73+a6*29+a7*2+a8*23-a9*36+a10*5+a11*2+a12*47-a13*64+a14*27==9710)
sol.add(a1*67-a2*68+a3*68-a4*51-a5*43+a6*81+a7*22-a8*12-a9*38+a10*75+a11*41+a12*27-a13*52+a14*31==13376)
sol.add(a1*85+a2*63+a3*5-a4*51+a5*44+a6*36+a7*28+a8*15-a9*6+a10*45+a11*31+a12*7-a13*67+a14*78==24065)
sol.add(a1*47+a2*64+a3*66-a4*5+a5*43+a6*112+a7*25+a8*13-a9*35+a10*95+a11*21+a12*43-a13*61+a14*20==27687)
sol.add(a1*89+a2*67+a3*85-a4*25+a5*49+a6*89+a7*23+a8*56-a9*92+a10*14+a11*89+a12*47-a13*61-a14*29==29250)
sol.add(a1*95+a2*34+a3*62-a4*9-a5*43+a6*83+a7*25+a8*12-a9*36+a10*16+a11*51+a12*47-a13*60-a14*24==15317)
check=sol.check()
print(check)
model=sol.model()
print(model)
# sat
# [a13 = 88,
#  a3 = 10,
#  a4 = 7,
#  a10 = 108,
#  a12 = 74,
#  a1 = 119,
#  a7 = 28,
#  a6 = 43,
#  a9 = 52,
#  a14 = 33,
#  a5 = 104,
#  a8 = 91,
#  a2 = 24,
#  a11 = 88]

xor逆向：

1
2
3
4
5
6
7
8
9
10
#include <cstdio>
using namespace std;
int map[14]={10,24,119,7,104,43,28,91,108,52,88,74,88,33};
int main(void){
    for(register int i=12;i>=0;i--)
        map[i]^=map[i+1];
    for(register int i=0;i<=13;i++)
        printf("%c",map[i]);
    return 0;
};

[柏鹭杯 2021]baby_python

pyinstxtractor发现被加密，反编译pyimod00_crypto_key.pyc，取得密钥，反编译pyimod02_archive.pyc，发现加密逻辑为zlib加密，exp：

1
2
3
4
5
6
7
8
9
inf=open(r'...\baby_python.baby_core.pyc.encrypted','rb')
c=Cipher()
buf=c.decrypt(inf.read())
buf=zlib.decompress(buf)
out=open(r'...\baby_python.baby_core.pyc','wb')
out.write(buf)
print('written down %d bytes'%len(buf))
inf.close()
out.close()

反汇编，用z3+md5解决

[HGAME 2023 week2]math

注意第2~4行一定不能写成这样：

1
v10=v11=v12=[0]*25

这样v10、v11、v12会指向同一个地址，即为同一个变量。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
from z3 import *
v10=[0]*25
v12=[0]*25
v11=[0]*25
v10[0]=126
v10[1]=225
v10[2]=62
v10[3]=40
v10[4]=216
v10[5]=253
v10[6]=20
v10[7]=124
v10[8]=232
v10[9]=122
v10[10]=62
v10[11]=23
v10[12]=100
v10[13]=161
v10[14]=36
v10[15]=118
v10[16]=21
v10[17]=184
v10[18]=26
v10[19]=142
v10[20]=59
v10[21]=31
v10[22]=186
v10[23]=82
v10[24]=79
v12[0]=63998
v12[1]=33111
v12[2]=67762
v12[3]=54789
v12[4]=61979
v12[5]=69619
v12[6]=37190
v12[7]=70162
v12[8]=53110
v12[9]=68678
v12[10]=63339
v12[11]=30687
v12[12]=66494
v12[13]=50936
v12[14]=60810
v12[15]=48784
v12[16]=30188
v12[17]=60104
v12[18]=44599
v12[19]=52265
v12[20]=43048
v12[21]=23660
v12[22]=43850
v12[23]=33646
v12[24]=44270
x=Solver()
flag=[Int('%d'%i) for i in range(25)]
for i in range(5):
    for j in range(5):
        for k in range(5):
            v11[5*i+j]+=flag[5*i+k]*v10[5*k+j]
for i in range(25):
    x.add(v11[i]==v12[i])
x.check()
model=x.model()
for i in range(25):
    print(chr(model[flag[i]].as_long()),end='')

挺烦的z3

[MoeCTF 2022]EquationPy

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
from z3 import *
ans=[Int('%d'%i) for i in range(22)]
x=Solver()
x.add(ans[0]*7072+ans[1]*2523+ans[2]*6714+ans[3]*8810+ans[4]*6796+ans[5]*2647+ans[6]*1347+ans[7]*1289+ans[8]*8917+ans[9]*2304+ans[10]*5001+ans[11]*2882+ans[12]*7232+ans[13]*3192+ans[14]*9676+ans[15]*5436+ans[16]*4407+ans[17]*6269+ans[18]*9623+ans[19]*6230+ans[20]*6292+ans[21]*57==10743134)
x.add(ans[0]*3492+ans[1]*1613+ans[2]*3234+ans[3]*5656+ans[4]*9182+ans[5]*4240+ans[6]*8808+ans[7]*9484+ans[8]*4000+ans[9]*1475+ans[10]*2616+ans[11]*2766+ans[12]*6822+ans[13]*1068+ans[14]*9768+ans[15]*1420+ans[16]*4528+ans[17]*1031+ans[18]*8388+ans[19]*2029+ans[20]*2463+ans[21]*32==9663091)
x.add(ans[0]*9661+ans[1]*1108+ans[2]*2229+ans[3]*1256+ans[4]*7747+ans[5]*5775+ans[6]*5211+ans[7]*2387+ans[8]*1997+ans[9]*4045+ans[10]*7102+ans[11]*7853+ans[12]*5596+ans[13]*6952+ans[14]*8883+ans[15]*5125+ans[16]*9572+ans[17]*1149+ans[18]*7583+ans[19]*1075+ans[20]*9804+ans[21]*72==10521461)
x.add(ans[0]*4314+ans[1]*3509+ans[2]*6200+ans[3]*5546+ans[4]*1705+ans[5]*9518+ans[6]*2975+ans[7]*2689+ans[8]*2412+ans[9]*8659+ans[10]*5459+ans[11]*7572+ans[12]*3042+ans[13]*9701+ans[14]*4697+ans[15]*9863+ans[16]*1296+ans[17]*1278+ans[18]*5721+ans[19]*5116+ans[20]*4147+ans[21]*52==9714028)
x.add(ans[0]*2310+ans[1]*1379+ans[2]*5900+ans[3]*4876+ans[4]*5329+ans[5]*6485+ans[6]*6610+ans[7]*7179+ans[8]*7897+ans[9]*1094+ans[10]*4825+ans[11]*8101+ans[12]*9519+ans[13]*3048+ans[14]*3168+ans[15]*2775+ans[16]*4366+ans[17]*4066+ans[18]*7490+ans[19]*5533+ans[20]*2139+ans[21]*87==10030960)
x.add(ans[0]*1549+ans[1]*8554+ans[2]*6510+ans[3]*6559+ans[4]*5570+ans[5]*1003+ans[6]*8562+ans[7]*6793+ans[8]*3509+ans[9]*4965+ans[10]*6111+ans[11]*1229+ans[12]*5654+ans[13]*2204+ans[14]*2217+ans[15]*5039+ans[16]*5657+ans[17]*9426+ans[18]*7604+ans[19]*5883+ans[20]*5285+ans[21]*17==10946682)
x.add(ans[0]*2678+ans[1]*4369+ans[2]*7509+ans[3]*1564+ans[4]*7777+ans[5]*2271+ans[6]*9696+ans[7]*3874+ans[8]*2212+ans[9]*6764+ans[10]*5727+ans[11]*5971+ans[12]*5876+ans[13]*9959+ans[14]*4604+ans[15]*8461+ans[16]*2350+ans[17]*3564+ans[18]*1831+ans[19]*6088+ans[20]*4575+ans[21]*9==10286414)
x.add(ans[0]*8916+ans[1]*8647+ans[2]*4522+ans[3]*3579+ans[4]*5319+ans[5]*9124+ans[6]*9535+ans[7]*5125+ans[8]*3235+ans[9]*3246+ans[10]*3378+ans[11]*9221+ans[12]*1875+ans[13]*1008+ans[14]*6262+ans[15]*1524+ans[16]*8851+ans[17]*4367+ans[18]*7628+ans[19]*9404+ans[20]*2065+ans[21]*9==11809388)
x.add(ans[0]*9781+ans[1]*9174+ans[2]*3771+ans[3]*6972+ans[4]*6425+ans[5]*7631+ans[6]*8864+ans[7]*9117+ans[8]*4328+ans[9]*3919+ans[10]*6517+ans[11]*7165+ans[12]*6895+ans[13]*3609+ans[14]*3878+ans[15]*1593+ans[16]*9098+ans[17]*6432+ans[18]*2584+ans[19]*8403+ans[20]*4029+ans[21]*30==13060508)
x.add(ans[0]*2511+ans[1]*8583+ans[2]*2428+ans[3]*9439+ans[4]*3662+ans[5]*3278+ans[6]*8305+ans[7]*1100+ans[8]*7972+ans[9]*8510+ans[10]*8552+ans[11]*9993+ans[12]*6855+ans[13]*1702+ans[14]*1640+ans[15]*3787+ans[16]*8161+ans[17]*2110+ans[18]*5320+ans[19]*3313+ans[20]*9286+ans[21]*74==10568195)
x.add(ans[0]*4974+ans[1]*4445+ans[2]*7368+ans[3]*9132+ans[4]*5894+ans[5]*7822+ans[6]*7923+ans[7]*6822+ans[8]*2698+ans[9]*3643+ans[10]*8392+ans[11]*4126+ans[12]*1941+ans[13]*6641+ans[14]*2949+ans[15]*7405+ans[16]*9980+ans[17]*6349+ans[18]*3328+ans[19]*8766+ans[20]*9508+ans[21]*65==12514783)
x.add(ans[0]*4127+ans[1]*4703+ans[2]*6409+ans[3]*4907+ans[4]*5230+ans[5]*3371+ans[6]*5666+ans[7]*3194+ans[8]*5448+ans[9]*8415+ans[10]*4525+ans[11]*4152+ans[12]*1467+ans[13]*5254+ans[14]*2256+ans[15]*1643+ans[16]*9113+ans[17]*8805+ans[18]*4315+ans[19]*8371+ans[20]*1919+ans[21]*2==10299950)
x.add(ans[0]*6245+ans[1]*8783+ans[2]*6059+ans[3]*9375+ans[4]*9253+ans[5]*1974+ans[6]*8867+ans[7]*6423+ans[8]*2577+ans[9]*6613+ans[10]*2040+ans[11]*2209+ans[12]*4147+ans[13]*7151+ans[14]*1011+ans[15]*9446+ans[16]*4362+ans[17]*3073+ans[18]*3006+ans[19]*5499+ans[20]*8850+ans[21]*23==11180727)
x.add(ans[0]*1907+ans[1]*9038+ans[2]*3932+ans[3]*7054+ans[4]*1135+ans[5]*5095+ans[6]*6962+ans[7]*6481+ans[8]*7049+ans[9]*5995+ans[10]*6233+ans[11]*1321+ans[12]*4455+ans[13]*8181+ans[14]*5757+ans[15]*6953+ans[16]*3167+ans[17]*5508+ans[18]*4602+ans[19]*1420+ans[20]*3075+ans[21]*25==10167536)
x.add(ans[0]*1489+ans[1]*9236+ans[2]*7398+ans[3]*4088+ans[4]*4131+ans[5]*1657+ans[6]*9068+ans[7]*6420+ans[8]*3970+ans[9]*3265+ans[10]*5343+ans[11]*5386+ans[12]*2583+ans[13]*2813+ans[14]*7181+ans[15]*9116+ans[16]*4836+ans[17]*6917+ans[18]*1123+ans[19]*7276+ans[20]*2257+ans[21]*65==10202212)
x.add(ans[0]*2097+ans[1]*1253+ans[2]*1469+ans[3]*2731+ans[4]*9565+ans[5]*9185+ans[6]*1095+ans[7]*8666+ans[8]*2919+ans[9]*7962+ans[10]*1497+ans[11]*6642+ans[12]*4108+ans[13]*6892+ans[14]*7161+ans[15]*7552+ans[16]*5666+ans[17]*4060+ans[18]*7799+ans[19]*5080+ans[20]*8516+ans[21]*43==10435786)
x.add(ans[0]*1461+ans[1]*1676+ans[2]*4755+ans[3]*7982+ans[4]*3860+ans[5]*1067+ans[6]*6715+ans[7]*4019+ans[8]*4983+ans[9]*2031+ans[10]*1173+ans[11]*2241+ans[12]*2594+ans[13]*8672+ans[14]*4810+ans[15]*7963+ans[16]*7749+ans[17]*5730+ans[18]*9855+ans[19]*5858+ans[20]*2349+ans[21]*71==9526385)
x.add(ans[0]*9025+ans[1]*9536+ans[2]*1515+ans[3]*8177+ans[4]*6109+ans[5]*4856+ans[6]*6692+ans[7]*4929+ans[8]*1010+ans[9]*3995+ans[10]*3511+ans[11]*5910+ans[12]*3501+ans[13]*3731+ans[14]*6601+ans[15]*6200+ans[16]*8177+ans[17]*5488+ans[18]*5957+ans[19]*9661+ans[20]*4956+ans[21]*48==11822714)
x.add(ans[0]*4462+ans[1]*1940+ans[2]*5956+ans[3]*4965+ans[4]*9268+ans[5]*9627+ans[6]*3564+ans[7]*5417+ans[8]*2039+ans[9]*7269+ans[10]*9667+ans[11]*4158+ans[12]*2856+ans[13]*2851+ans[14]*9696+ans[15]*5986+ans[16]*6237+ans[17]*5845+ans[18]*5467+ans[19]*5227+ans[20]*4771+ans[21]*72==11486796)
x.add(ans[0]*4618+ans[1]*8621+ans[2]*8144+ans[3]*7115+ans[4]*1577+ans[5]*8602+ans[6]*3886+ans[7]*3712+ans[8]*1258+ans[9]*7063+ans[10]*1872+ans[11]*9855+ans[12]*4167+ans[13]*7615+ans[14]*6298+ans[15]*7682+ans[16]*8795+ans[17]*3856+ans[18]*6217+ans[19]*5764+ans[20]*5076+ans[21]*93==11540145)
x.add(ans[0]*7466+ans[1]*8442+ans[2]*4822+ans[3]*7639+ans[4]*2049+ans[5]*7311+ans[6]*5816+ans[7]*8433+ans[8]*5905+ans[9]*4838+ans[10]*1251+ans[11]*8184+ans[12]*6465+ans[13]*4634+ans[14]*5513+ans[15]*3160+ans[16]*6720+ans[17]*9205+ans[18]*6671+ans[19]*7716+ans[20]*1905+ans[21]*29==12227250)
x.add(ans[0]*5926+ans[1]*9095+ans[2]*2048+ans[3]*4639+ans[4]*3035+ans[5]*9560+ans[6]*1591+ans[7]*2392+ans[8]*1812+ans[9]*6732+ans[10]*9454+ans[11]*8175+ans[12]*7346+ans[13]*6333+ans[14]*9812+ans[15]*2034+ans[16]*6634+ans[17]*1762+ans[18]*7058+ans[19]*3524+ans[20]*7462+ans[21]*11==11118093)
x.check()
model=x.model()
for i in range(22):
    print(chr(model[ans[i]].as_long()),end='')

[网鼎杯 2020 青龙组]singal

符号执行

1
2
3
4
5
6
7
8
9
10
11
12
import angr,sys
path="D:\\CTF-Workbench\\signal.exe"
project=angr.Project(path,auto_load_libs=False)
initial_state=project.factory.entry_state()
simulation=project.factory.simulation_manager(initial_state)
simulation.explore(find=0x0040179E,avoid=0x004016E6)
if simulation.found:
    for i in simulation.found:
        solution_state=i
        print(solution_state.posix.dumps(0))
else:
    print("no\n")

[HUBUCTF 2022 新生赛]Anger？Angr

这题离谱，尝试angr，发现结果是一堆乱码…

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
import angr
import sys
import claripy
p = angr.Project('./anger', auto_load_libs = True)
initial_state = p.factory.entry_state(
    add_options = { angr.options.SYMBOL_FILL_UNCONSTRAINED_MEMORY,
                    angr.options.SYMBOL_FILL_UNCONSTRAINED_REGISTERS}
  )
s = p.factory.simgr(initial_state)
s.one_active.options.add(angr.options.LAZY_SOLVES)
def is_successful(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    if "Cor".encode() in stdout_output:
        return True
    else:
        return False
def should_abort(state):
    stdout_output = state.posix.dumps(sys.stdout.fileno())
    if "Incor".encode() in stdout_output:
        return True
    else:
        return False
s.explore(find=is_successful,avoid=should_abort)
f = s.found[0].posix.dumps(sys.stdin.fileno())
print(f)

尝试z3，就是麻烦点。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
from z3 import *
a1 =  [BitVec('a1%s' % i,8) for i in range(32) ]
s=Solver()
s.add(BV2Int(a1[10]) <= 40 , 24 * BV2Int(a1[30]) % 84 == 12 , BV2Int(a1[16]) != 66)
s.add(BV2Int(a1[4]) > 51 , BV2Int(a1[15]) > 90 , BV2Int(a1[18]) != 38)
s.add(BV2Int(a1[3]) <= 107 , 61 * BV2Int(a1[20]) % 95 == 2 , BV2Int(a1[27]) != 67)
s.add(BV2Int(a1[29]) <= 69 , 39 * BV2Int(a1[18]) % 57 == 27 , BV2Int(a1[29]) <= 90)
s.add(a1[21] > 42 , a1[0] > 35 , a1[7] != 74)
s.add(a1[19] <= 79 , a1[15] > 74 , a1[22] > 92)
s.add(a1[14]<=89,a1[24]!=95)
s.add( a1[26] > 36)
s.add(a1[22]>53,BV2Int(a1[12])!=33)
s.add( (29 * BV2Int(a1[6])) % 33 == 24)
s.add( 41 * BV2Int(a1[26]) % 31 == 27)
s.add(BV2Int(a1[16]) != 71  )
s.add( 22 * BV2Int(a1[24]) % 96 == 60)
s.add(a1[25] != 102  , a1[18] != 95)
s.add( 38 * BV2Int(a1[6]) % 54 == 36)
s.add(a1[4]>52)
s.add(a1[11]<=76)
s.add( 72 * BV2Int(a1[6]) % 86 == 42 )
s.add(a1[5] <= 109 , a1[9] > 44 , a1[8] > 77)
s.add(a1[28] != 107  , a1[17] > 73)
s.add( 69 * BV2Int(a1[5]) % 3==0)
s.add(a1[0] != 70 , a1[13] > 72 , a1[1] <= 108)
s.add(a1[14]!=97)
s.add(a1[1]<=90)
s.add( 87 * BV2Int(a1[31]) % 69 == 45)
s.add(a1[11] <= 99 , a1[24] != 107 , a1[26] <= 111)
s.add(a1[0] > 36 , a1[3] <= 65 , a1[2] > 41)
s.add(a1[23] != 84 , a1[16] != 101 , a1[13] <= 99)
s.add(a1[19] > 33 , a1[25] <= 122 , a1[28] != 67)
s.add(86 * BV2Int(a1[17]) % 74 == 64 , BV2Int(a1[10]) != 87 , BV2Int(a1[30]) <= 108)
s.add(BV2Int(a1[8])!=87)
s.add(46 * BV2Int(a1[12]) % 26 == 20 , 50 * BV2Int(a1[9]) % 52 == 22)
s.add(BV2Int(a1[8]) > 47 ,BV2Int(a1[21]) <= 100 , BV2Int(a1[11]) > 34)
s.add(BV2Int(a1[27]) != 127 , BV2Int(a1[21]) > 42 )
s.add( 5 * BV2Int(a1[10]) % 32 == 20)
s.add( BV2Int(a1[12]) <= 107)
s.add(BV2Int(a1[19]) != 91  , BV2Int(a1[29]) != 124)
s.add( 57 * BV2Int(a1[13]) % 13 == 2 , BV2Int(a1[27]) <= 100 , 61 * BV2Int(a1[22]) % 67 == 66)
s.add(BV2Int(a1[7]) <= 118 , BV2Int(a1[1]) != 64 , BV2Int(a1[30]) > 44)
s.add(BV2Int(a1[5]) != 43 , BV2Int(a1[31]) != 88 , BV2Int(a1[31]) > 35)
s.add(BV2Int(a1[20]) <= 101 , BV2Int(a1[15]) > 64 , BV2Int(a1[4]) != 43)
s.add(BV2Int(a1[17])>56)
s.add(BV2Int(a1[28])<=115)
s.add( (BV2Int(a1[25]) *64) % 21 == 4 )
s.add(BV2Int(a1[20]) != 43 , BV2Int(a1[2]) <= 82 , BV2Int(a1[2]) > 39)
s.add(BV2Int(a1[23]) > 34 , BV2Int(a1[7]) > 52 , BV2Int(a1[14]) > 44)
s.add(BV2Int(a1[3]) <= 83 , 59 * BV2Int(a1[9]) % 86 == 69 , BV2Int(a1[23]) <= 103)
for i in range(0,32):
    s.add(BV2Int(a1[i])<127)
    s.add(BV2Int(a1[i])>30)
s.check()
m=s.model()
print(m)
res=''
for i in range(0,32):
    res+=(chr(m[a1[i]].as_long()))
print(res)

[网鼎杯 2020 青龙组]singal

学习Ponce插件的使用。

随便输入15个字符，在read函数的scanf后下断点，找到输入字符后，选中右键“Symbolic->Symbolize memory”，然后在vm_operad中判断失败的jz跳转处下断点，并右键“SMT Solver->Solve Formula->最后一个”，即可解出1字节。因为输入不对，手动把EIP设为正确并进入下一轮，再次求解1字节，重复可得flag。

[CISCN 2021初赛]babybc

5x5线性规划，z3做：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
from z3 import *
import hashlib
map=[[None]*5,
     [None]*5,
     [None]*5,
     [None]*5,
     [None]*5]
row=[[0x00,0x00,0x00,0x01],
     [0x01,0x00,0x00,0x00],
     [0x02,0x00,0x00,0x01],
     [0x00,0x00,0x00,0x00],
     [0x01,0x00,0x01,0x00]]
col=[[0x00,0x00,0x02,0x00,0x02],
     [0x00,0x00,0x00,0x00,0x00],
     [0x00,0x00,0x00,0x01,0x00],
     [0x00,0x01,0x00,0x00,0x01]]
for i in range(5):
    for j in range(5):
        map[i][j]=Int('map%d%d'%(i,j))
s=Solver()
s.add(map[2][2]==0x04)
s.add(map[3][3]==0x03)
for i in range(5):
    for j in range(5):
        s.add(map[i][j]>=1)
        s.add(map[i][j]<=5)
for i in range(5):
    for j in range(5):
        for k in range(j+1,5):
            s.add(map[i][j]!=map[i][k])
for i in range(5):
    for j in range(5):
        for k in range(j+1,5):
            s.add(map[j][i]!=map[k][i])
for i in range(5):
    for j in range(4):
        if row[i][j]==0x01:
            s.add(map[i][j]>map[i][j+1])
        elif row[i][j]==0x02:
            s.add(map[i][j]<map[i][j+1])
for i in range(4):
    for j in range(5):
        if col[i][j]==0x01:
            s.add(map[i][j]<map[i+1][j])
        elif col[i][j]==0x02:
            s.add(map[i][j]>map[i+1][j])
if s.check()==sat:
    res=s.model()
    s=''
    for i in range(5):
        for j in range(5):
            if ((i==2)and(j==2))or((i==3)and(j==3)):
                s+='0'
            else:
                s+=str(res[map[i][j]].as_long())
    print('CISCN{%s}'%(hashlib.md5(s.encode()).hexdigest()))