推薦肉絲r0ysue課程（包含安卓逆向與js逆向）：

新手一枚，如有錯誤（不足）請指正，謝謝！！
個人博客：點擊進入
題目鏈接：[GUET-CTF2019]re
題目下載：點擊下載

IDA64位載入

大概率被加殼，使用exeinfope查看

upx殼，使用官方upx脫殼

脫殼后IDA64載入，shift+F12查找字符串

找到關鍵代碼

查看sub_4009AE()函數

典型z3約束器求解題
（當然你想一個個挨個手動算的話也行……）
z3安裝請查看
linux筆記 CTF-pwn環境搭建
Z3約束器詳細學習（0）—Z3安裝|語句詳解

編寫腳本

from z3 import * s = Solver() a1 = [0]*32 for i in range(32):a1[i] = Int('a1['+str(i)+']')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) s.check() print(s.model())

之后提取出數據，轉化為字符輸出就好
因為沒有a1[6]，所以跳過

a1 = [0]*32 a1[31] = 125 a1[30] = 55 a1[29] = 51 a1[28] = 51 a1[27] = 57 a1[26] = 51 a1[25] = 48 a1[24] = 99 a1[23] = 49 a1[22] = 97 a1[21] = 57 a1[20] = 57 a1[19] = 48 a1[18] = 51 a1[16] = 97 a1[17] = 48 a1[15] = 98 a1[14] = 48 a1[13] = 49 a1[12] = 49 a1[11] = 49 a1[10] = 50 a1[9] = 52 a1[8] = 53 a1[7] = 54 a1[5] = 101 a1[4] = 123 a1[3] = 103 a1[2] = 97 a1[1] = 108 a1[0] = 102 for i in range(32):if i == 6:continueprint(chr(a1[i]), end="")

出題人少給了一位a1[6]，
@羊毛羊指正使用burp爆破出來a1[6]=1
所以最終flag為flag{e165421110ba03099a1c039337}

總結

以上是生活随笔為你收集整理的re学习笔记（37）BUUCTF-re-[GUET-CTF2019]re Z3约束求解器的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。