考点z3求解器查壳脱壳进入idasub_4009AE是关键函数进入查看_BOOL8 __fastcall sub_4009AE(char *a1) { if ( 1629056 * *a1 ! 166163712 ) return 0LL; if ( 6771600 * a1[1] ! 731332800 ) return 0LL; if ( 3682944 * a1[2] ! 357245568 ) return 0LL; if ( 10431000 * a1[3] ! 1074393000 ) return 0LL; if ( 3977328 * a1[4] ! 489211344 ) return 0LL; if ( 5138336 * a1[5] ! 518971936 ) return 0LL; if ( 7532250 * a1[7] ! 406741500 ) return 0LL; if ( 5551632 * a1[8] ! 294236496 ) return 0LL; if ( 3409728 * a1[9] ! 177305856 ) return 0LL; if ( 13013670 * a1[10] ! 650683500 ) return 0LL; if ( 6088797 * a1[11] ! 298351053 ) return 0LL; if ( 7884663 * a1[12] ! 386348487 ) return 0LL; if ( 8944053 * a1[13] ! 438258597 ) return 0LL; if ( 5198490 * a1[14] ! 249527520 ) return 0LL; if ( 4544518 * a1[15] ! 445362764 ) return 0LL; if ( 3645600 * a1[17] ! 174988800 ) return 0LL; if ( 10115280 * a1[16] ! 981182160 ) return 0LL; if ( 9667504 * a1[18] ! 493042704 ) return 0LL; if ( 5364450 * a1[19] ! 257493600 ) return 0LL; if ( 13464540 * a1[20] ! 767478780 ) return 0LL; if ( 5488432 * a1[21] ! 312840624 ) return 0LL; if ( 14479500 * a1[22] ! 1404511500 ) return 0LL; if ( 6451830 * a1[23] ! 316139670 ) return 0LL; if ( 6252576 * a1[24] ! 619005024 ) return 0LL; if ( 7763364 * a1[25] ! 372641472 ) return 0LL; if ( 7327320 * a1[26] ! 373693320 ) return 0LL; if ( 8741520 * a1[27] ! 498266640 ) return 0LL; if ( 8871876 * a1[28] ! 452465676 ) return 0LL; if ( 4086720 * a1[29] ! 208422720 ) return 0LL; if ( 9374400 * a1[30] 515592000 ) return 5759124 * a1[31] 719890500; return 0LL; }a1[6]没有给出其他的值用z3求解器求解脚本from z3 import * #定义32个整数变量a1[0]-a1[32] a1[Int(fa1_{i}) for i in range(32)] #创建求解器 sSolver() #添加限制条件 s.add(1629056 *a1[0] 166163712) s.add(6771600 * a1[1] 731332800) s.add(3682944 * a1[2] 357245568) s.add( 10431000 * a1[3] 1074393000 ) s.add( 3977328 * a1[4] 489211344 ) s.add( 5138336 * a1[5] 518971936 ) s.add( 7532250 * a1[7] 406741500 ) s.add( 5551632 * a1[8] 294236496 ) s.add( 3409728 * a1[9] 177305856 ) s.add( 13013670 * a1[10] 650683500 ) s.add ( 6088797 * a1[11] 298351053 ) s.add ( 7884663 * a1[12] 386348487 ) s.add ( 8944053 * a1[13] 438258597 ) s.add ( 5198490 * a1[14] 249527520 ) s.add ( 4544518 * a1[15] 445362764 ) s.add ( 3645600 * a1[17] 174988800 ) s.add ( 10115280 * a1[16] 981182160 ) s.add ( 9667504 * a1[18] 493042704 ) s.add ( 5364450 * a1[19] 257493600 ) s.add ( 13464540 * a1[20] 767478780 ) s.add ( 5488432 * a1[21] 312840624 ) s.add ( 14479500 * a1[22] 1404511500 ) s.add ( 6451830 * a1[23] 316139670 ) s.add ( 6252576 * a1[24] 619005024 ) s.add ( 7763364 * a1[25] 372641472 ) s.add ( 7327320 * a1[26] 373693320 ) s.add ( 8741520 * a1[27] 498266640 ) s.add ( 8871876 * a1[28] 452465676 ) s.add ( 4086720 * a1[29] 208422720 ) s.add ( 9374400 * a1[30] 515592000 ) s.add(5759124 * a1[31] 719890500) #检查解是否存在 if s.check()sat: models.model() flag #定义flag print(a1) for i in range(32): if i6: flag_ #a1[6]先取为_ continue valmodel.evaluate(a1[i]).as_long() if 0 val 127: flag chr(val) else: flagf[{val}] print(最终Flag: ,flag) else: print(无解)1-9一个一个试得a1[6]1flag{e165421110ba03099a1c039337}