2020强网杯

太久没打ctf了

re

xx_warmup_obf

一堆花指令，去除后z3解

# -*- coding: UTF-8 -*-
from z3 import *
s = Solver()
key = [BitVec('%d'%i,8) for i in range(28)]
s.add(key[0] == ord('f'))
s.add(key[1] == ord('l'))
s.add(key[2] == ord('a'))
s.add(key[3] == ord('g'))
s.add(key[4] == ord('{'))
s.add(key[27] == ord('}'))
s.add(key[23] == ord('_'))
s.add(23925 * key[0] == 2440350)
s.add(281400 * key[1] - 7037 * key[0] == 29673426)
s.add(174826 * key[0] - 255300 * key[2] - 283573 * key[1] == -37557732)
s.add( 259881 * key[2] + -98445 * key[1] - 276718 * key[0] + 4524 * key[3] == -13182867 )
s.add( 285576 * key[2] + -274569 * key[3] + 94721 * key[0] - 228216 * key[4] - 60353 * key[1] == -25506885 )
s.add( 17630 * key[0]+ -258397 * key[3]+ -244952 * key[1]+ -244086 * key[2]+ -130259 * key[5]- 190371 * key[6]- 109961 * key[4] == -111027477 )
s.add( 117817 * key[5] + 268397 * key[7] + -198175 * key[1] + 18513 * key[2] + 218992 * key[6] + -6727 * key[3] + 228408 * key[0] + 224658 * key[4] == 78775012 )
s.add(260927 * key[3]+ -5496 * key[1]+ -294195 * key[4]+ 264844 * key[2]+ 125853 * key[5] - 153661 * key[0] == 13075233  )
s.add( -196269 * key[8] + -64473 * key[7] + -142792 * key[5] + 171321 * key[4] + -39259 * key[9] + -269632 * key[2] + 229049 * key[6] + 96631 * key[3] - 280754 * key[1] - 168397 * key[0] == -70797046 )
s.add( -235026 * key[4] + 162669 * key[8] + -256202 * key[1] + -32946 * key[9] + -25900 * key[2] + 195039 * key[10] + 182157 * key[3] + 292706 * key[0] + -93524 * key[5] + 121516 * key[6] + 165207 * key[7] == 28263339 )
s.add( -288418 * key[3] + -218493 * key[7] + -236774 * key[0] + 77982 * key[2] + 190784 * key[4] + -84462 * key[1] + 92684 * key[8] + 52068 * key[5] - 243023 * key[6] == -52520267 )
s.add( -262820 * key[4] + 9710 * key[10] + 71182 * key[12] + -184125 * key[1] + -100280 * key[6] + 62018 * key[11] + 141532 * key[9] + -138253 * key[8] + 20489 * key[0] + -214348 * key[2] + 162962 * key[3] - 93199 * key[7] + 147171 * key[5] == -31396844 )
s.add( -131770 * key[6] + -92964 * key[9] + -111160 * key[8] + -258188 * key[7] + 133728 * key[1] + -272650 * key[5] + -4940 * key[10] + 272791 * key[3] + 80519 * key[2] + -165434 * key[11] + 50166 * key[0] + 148713 * key[4] == -22025185 )
s.add(-55254 * key[8]+ 220404 * key[12]+ -86956 * key[10]+ -200702 * key[5]+ -51437 * key[1]+ 25739 * key[6]+ 122945 * key[3]+ 116256 * key[7]+ 22859 * key[4]+ -61880 * key[9]+ -119275 * key[2]+ -224754 * key[13]- 75412 * key[0]+ 59999 * key[11] == -37063008)
s.add(111310 * key[0]+ 198502 * key[3]+ -189890 * key[13]+ 278745 * key[5]+ 157462 * key[9]+ 135809 * key[4]+ -2621 * key[2]+ 67553 * key[6]+ 144834 * key[1]+ -88326 * key[11]+ -228149 * key[10]+ 233663 * key[14]+ -249960 * key[12]+ 300012 * key[8]+ 91783 * key[7] == 93457153)
s.add(15897 * key[0]+ -11943 * key[13]+ 194067 * key[3]+ 125666 * key[2]+ 104421 * key[12]+ -181764 * key[5]+ -233813 * key[8]+ -235783 * key[4]+ 230636 * key[11]+ 148005 * key[6]+ -48167 * key[14]+ -163572 * key[9]+ 54553 * key[10]+ -129997 * key[1]+ 114175 * key[7]- 251681 * key[15] == -36640750)
s.add( -90549 * key[3]+ -228520 * key[14]+ 34835 * key[10]+ -203538 * key[15]+ 272318 * key[13]+ -68478 * key[8]+ 22454 * key[9]+ 74128 * key[12]+ 70051 * key[6]+ -289940 * key[7]+ -52501 * key[5]+ -1254 * key[4]+ 154844 * key[11]+ 254969 * key[2]+ -39495 * key[1]+ 277429 * key[16]- 132752 * key[0] == -6628237 )
s.add( 128092 * key[11]+ -5873 * key[17]+ -144172 * key[3]+ -148216 * key[13]+ 189050 * key[2]+ 66107 * key[5]+ 237987 * key[0]+ -53271 * key[9]+ -86968 * key[12]+ -94616 * key[10]+ -247882 * key[8]+ -5107 * key[1]+ 55085 * key[15]+ 10792 * key[14]+ -112241 * key[4]+ -36680 * key[16]- 210718 * key[7]- 249539 * key[6] == -53084017 )
s.add( -186088 * key[2]+ 19517 * key[13]+ -65515 * key[5]+ 195447 * key[1]+ 145470 * key[14]+ 58825 * key[16]+ 272227 * key[15]+ -155443 * key[8]+ 100397 * key[3]+ -238861 * key[18]+ 84628 * key[7]+ 1337 * key[17]+ 156976 * key[12]+ -74209 * key[4]+ 175077 * key[11]+ 134548 * key[0]+ -280672 * key[6]+ 12264 * key[10] + 56937 * key[9] == 60764977 )
s.add( -58873 * key[7]+ -283834 * key[9]+ 159144 * key[13]+ -199631 * key[0]+ 54404 * key[16]+ -190345 * key[8]+ 176103 * key[3]+ 137206 * key[17]+ -170051 * key[6]+ 281718 * key[11]+ 137214 * key[14]+ -104395 * key[19]+ -122090 * key[4]+ 162065 * key[15]+ -36580 * key[18]+ 245858 * key[12]+ -18520 * key[10]+ -138274 * key[1]+ 139185 * key[2]- 197535 * key[5] == 4912728 )
s.add( 293345 * key[9]+ 63329 * key[13]+ 74470 * key[8]+ -72984 * key[11]+ -162393 * key[20]+ 150036 * key[15]+ 127913 * key[19]+ 181147 * key[16]+ 27751 * key[6]+ -239133 * key[1]+ -28337 * key[17]+ 108149 * key[0]+ 148338 * key[2]+ 38137 * key[18]+ -199427 * key[14]+ -97284 * key[4]+ -39775 * key[3]+ -109205 * key[10]+ 270604 * key[5]- 193384 * key[12]+ 168963 * key[7] == 45577809 )
s.add( 45637 * key[6]+ 111858 * key[17]+ 244009 * key[19]+ -188979 * key[8]+ -220539 * key[16]+ 246135 * key[2]+ -174651 * key[14]+ 179514 * key[4]+ 153071 * key[15]+ -207716 * key[21]+ 64641 * key[7]+ 293781 * key[12]+ 263208 * key[10]+ 44675 * key[1]+ 131692 * key[3]+ 109605 * key[11]+ 293201 * key[5]+ -98937 * key[9]+ 60492 * key[20]+ -273571 * key[13]- 38942 * key[0]- 285946 * key[18] == 77539017 )
s.add( -160726 * key[9]+ 234971 * key[18]+ 32897 * key[4]+ -206184 * key[11]+ -86224 * key[20]+ 92896 * key[22]+ 295735 * key[15]+ -58530 * key[0]+ -197632 * key[13]+ -21957 * key[17]+ -43684 * key[6]+ -141434 * key[10]+ -194890 * key[1]+ -148390 * key[21]+ 105293 * key[14]+ 76213 * key[3]+ 9791 * key[12]+ -258754 * key[8]+ 59119 * key[16]+ 255675 * key[2]+ -130852 * key[7]- 71444 * key[5]+ 127285 * key[19] == -38197685 )
s.add( 205675 * key[20]+ 197685 * key[1]+ 144870 * key[4]+ 120347 * key[10]+ 202621 * key[14]+ -236806 * key[17]+ 268813 * key[3]+ 191822 * key[23]+ -40848 * key[6]+ 103466 * key[7]+ -211930 * key[5]+ -180522 * key[19]+ -188959 * key[15]+ -238839 * key[21]+ 281705 * key[11]+ 175825 * key[16]+ -44618 * key[12]+ 196370 * key[0]+ 89330 * key[22]+ -133696 * key[8]+ -60213 * key[2]+ 191404 * key[18]- 291063 * key[9]+ 13902 * key[13] == 67763764 )
s.add( 69341 * key[15]+ -19740 * key[21]+ 62004 * key[10]+ 29334 * key[8]+ -78459 * key[1]+ -261617 * key[3]+ 115716 * key[22]+ 7838 * key[16]+ -173902 * key[14]+ 115189 * key[9]+ 234832 * key[7]+ -54321 * key[5]+ -268221 * key[20]+ -210563 * key[18]+ -161113 * key[13]+ -199130 * key[23]+ -94067 * key[24]+ 9601 * key[11]+ -8509 * key[12]+ 14439 * key[2]+ -243227 * key[19]+ 37665 * key[17]+ 91076 * key[6]- 85246 * key[0]+ 39558 * key[4] == -98330271 )
s.add( 38468 * key[19]+ -75568 * key[2]+ 169299 * key[22]+ -252915 * key[3]+ 32044 * key[24]+ -260264 * key[8]+ -111200 * key[1]+ -78437 * key[20]+ -212633 * key[16]+ 180400 * key[5]+ -81477 * key[12]+ 232645 * key[0]+ -65268 * key[4]+ 263000 * key[6]+ 247654 * key[25]+ -242059 * key[17]+ -35931 * key[9]+ -271816 * key[21]+ 10191 * key[13]+ 41768 * key[23]+ 92844 * key[7]+ -73366 * key[14]+ -124307 * key[10]+ 197710 * key[18]+ 226192 * key[15]+ 3788 * key[11] == -13464859 )
s.add( -23897 * key[9]+ -188087 * key[24]+ -254282 * key[15]+ -102361 * key[23]+ -15606 * key[14]+ -74795 * key[21]+ 116581 * key[12]+ 77693 * key[5]+ -6866 * key[25]+ 215574 * key[22]+ 231326 * key[6]+ 77915 * key[2]+ 186585 * key[3]+ 219151 * key[4]+ 271210 * key[13]+ -78913 * key[20]+ 83918 * key[8]+ -153409 * key[18]+ -84952 * key[7]+ -121854 * key[0]+ -253617 * key[26]+ -213665 * key[19]+ -293146 * key[17]+ -166693 * key[16]+ -206964 * key[1]- 155664 * key[10]+ 180598 * key[11] == -55504393 )
s.add( 264405 * key[11]+ 135302 * key[12]+ 278196 * key[9]+ -132906 * key[23]+ 138308 * key[7]+ 40423 * key[21]+ 157781 * key[0]+ -38949 * key[27]+ -143324 * key[14]+ -120743 * key[10]+ 77375 * key[5]+ -164339 * key[3]+ 167370 * key[25]+ -225830 * key[4]+ -136952 * key[2]+ -14347 * key[8]+ 6966 * key[26]+ 88628 * key[18]+ 138998 * key[22]+ 147747 * key[19]+ -106792 * key[6]+ -113009 * key[20]+ 98136 * key[15]+ 231264 * key[24]+ -109447 * key[17]+ 258890 * key[1]+ 167885 * key[16]+ 246315 * key[13] == 133068723 )


flag = ''
if s.check() == sat:
    result = s.model()
    print s.model()
    for i in range(28):
        flag += chr(result[key[i]].as_long().real)
    print flag
    print len('flag{g0_Fuck_xx_5egm3nt')

imitation_game

开头一个aes

后面提示chip8，google工具redasm直接反编译能看出大致逻辑

# -*- coding: UTF-8 -*-
from z3 import *
s = Solver()
key = [BitVec('%d'%i,8) for i in range(3)]

s.add(key[0]+2*key[1]+key[2] == 0x37)
s.add(2*key[0]+key[1]+key[2] == 0x37)
s.add(key[0]+2*key[1]+2*key[2] == 0x3b)
flag = ''
if s.check() == sat:
    print s.model()
aaa = [10,2,13,14,15,1,2,12,1,3]
flag = 'flag{6c8f1d78770fe672122478c6f9a150e6'
for i in range(len(aaa)):
    flag += str(hex(aaa[i]).replace('0x',''))
flag += '}'
print flag