看了xctf訓練平臺

發現了這道題  可以用兩種方法

最簡單的就是用angr跑一下   過程不再列舉(我試過了 可以成功)

具體方法可以看安裝使用Angr符號執行來求解CTF逆向題

還有就是用指令碼跑一下

載入IDA x32(雖然後綴是.ppp  但是一猜就知道elf   不知到位數  就先用32位IDA試一下唄)

可以看到程式就是獲取我們的輸入 nptr這個字串   然後設定位數是4位

v4 = atoi(&nptr)    這個用到了atoi()這個函式    作用是把我們輸入的字串轉成整型

事實上我們可以直接考慮輸入的就是一個整型資料   那就不用管這個函式    而nptr也就可以直接寫作v4

v5對100取餘再對10取整  那麼就相當於v4的十位上的數字

v4對10取餘是個位  v4除以1000是千位  v4 % 1000 / 100就是百位    

前段時間又學習了下z3(用來解方程的py庫  具體可以看https://blog.csdn.net/xiangshangbashaonian/article/details/82788155)

程式碼如下：

from z3 import *
v4 = Int('v4')
v5 = Int('v5')
s = Solver()
s.add(v4 >= 1000)#這裡我不知道長度怎樣設定成四位   就直接這樣子了
s.add(v4 <= 9999)
s.add(v5 == v4 % 100 / 10)#v5對100取餘再對10取整  那麼就相當於v4的十位上的數字
s.add(v4 % 10 + v5 + v4 / 1000 + v4 % 1000 / 100 == 23)#個位+十位+百位+千位等於23
s.add(v5 / (v4 % 10) == 2)#十位數字 / 個位 = 2
s.add(v4 % 1000 / 100 - v5 == -1)#剩下的自己分析吧 哈哈
s.add(v4 / 1000 % v5 == 3)#感覺用z3解有點大材小用
if s.check() != sat:
	print 'unsat'
else:
	m = s.model()
	print m
 

那麼驗證一下

正確！