首页
社区
课程
招聘
问答 CTF 排行榜 知识库 工具下载 峰会 看雪商城 证书查询
  1. 社区
  2. CTF对抗
    3. 发新帖
[原创]z3学习实战re PicoCTF2013 Harder_Serial
发表于: 2019-1-18 21:52 3240

[原创]z3学习实战re PicoCTF2013 Harder_Serial

wwzzww 活跃值
2019-1-18 21:52
3240
1.题目比较简单，是一段pythond代码，需要输入一段20个数字构成的序列，然后程序会对序列号一一验证，满足各种要求，难度不大，但是完全手工验证难度比较大，使用z3，定义好对应的条件，就可以得到满足条件的值。
import sys
print ("Please enter a valid serial number from your RoboCorpIntergalactic purchase")
if len(sys.argv) < 2:
    print ("Usage: %s [serial number]"%sys.argv[0])
    exit()
print ("#>" + sys.argv[1] + "<#")

def check_serial(serial):
    if (not set(serial).issubset(set(map(str,range(10))))):
        print ("only numbers allowed")
        return False
    if len(serial) != 20:
        return False
    if int(serial[15]) + int(serial[4]) != 10:
        return False
    if int(serial[1]) * int(serial[18]) != 2:
        return False
    if int(serial[15]) / int(serial[9]) != 1:
        return False
    if int(serial[17]) - int(serial[0]) != 4:
        return False
    if int(serial[5]) - int(serial[17]) != -1:
        return False
    if int(serial[15]) - int(serial[1]) != 5:
        return False
    if int(serial[1]) * int(serial[10]) != 18:
        return False
    if int(serial[8]) + int(serial[13]) != 14:
        return False
    if int(serial[18]) * int(serial[8]) != 5:
        return False
    if int(serial[4]) * int(serial[11]) != 0:
        return False
    if int(serial[8]) + int(serial[9]) != 12:
        return False
    if int(serial[12]) - int(serial[19]) != 1:
        return False
    if int(serial[9]) % int(serial[17]) != 7:
        return False
    if int(serial[14]) * int(serial[16]) != 40:
        return False
    if int(serial[7]) - int(serial[4]) != 1:
        return False
    if int(serial[6]) + int(serial[0]) != 6:
        return False
    if int(serial[2]) - int(serial[16]) != 0:
        return False
    if int(serial[4]) - int(serial[6]) != 1:
        return False
    if int(serial[0]) % int(serial[5]) != 4:
        return False
    if int(serial[5]) * int(serial[11]) != 0:
        return False
    if int(serial[10]) % int(serial[15]) != 2:
        return False
    if int(serial[11]) / int(serial[3]) != 0:
        return False
    if int(serial[14]) - int(serial[13]) != -4:
        return False
    if int(serial[18]) + int(serial[19]) != 3:
        return False
    return True
if check_serial(sys.argv[1]):
    print ("Thank you! Your product has been verified!")
else:
    print ("I'm sorry that is incorrect. Please use a valid RoboCorpIntergalactic serial number")
解题代码如下，这个题很适合用z3来做，这里也是刚开始学习，练练手
from z3 import *
'''serial=[]
for i in range(20):
    serial[i]=Int('serial['+str(i)+']')
'''
serial=[Int('serial[%d]'%i) for i in range(20)]
solver=Solver()
solver.add(serial[15] + serial[4] == 10)
solver.add(serial[1] * serial[18] == 2 )
solver.add(serial[15] / serial[9] == 1)
solver.add(serial[17] - serial[0] == 4)
solver.add(serial[5] - serial[17] == -1)
solver.add(serial[15] - serial[1] == 5)
solver.add(serial[1] * serial[10] == 18)
solver.add(serial[8] + serial[13] == 14)
solver.add(serial[18] * serial[8] == 5)
solver.add(serial[4] * serial[11] == 0)
solver.add(serial[8] + serial[9] == 12)
solver.add(serial[12] - serial[19] == 1)
solver.add(serial[9] % serial[17] == 7)
solver.add(serial[14] * serial[16] == 40)
solver.add(serial[7] - serial[4] == 1)
solver.add(serial[6] + serial[0] == 6)
solver.add(serial[2] - serial[16] == 0)
solver.add(serial[4] - serial[6] == 1)
solver.add(serial[0] % serial[5] == 4)
solver.add(serial[5] * serial[11] == 0)
solver.add(serial[10] % serial[15] == 2)
solver.add(serial[11] / serial[3] == 0)
solver.add(serial[14] - serial[13] == -4)
solver.add(serial[18] + serial[19] == 3)


for i in range(20):
    solver.add(serial[i]>=0,serial[i]<10)

solver.add(serial[3]!=0)

if solver.check()==sat:
    m=solver.model()
    #print(m.decls())
    print(m)
    for i in m.decls():
        print(m[i]),




import sys
print ("Please enter a valid serial number from your RoboCorpIntergalactic purchase")
if len(sys.argv) < 2:
    print ("Usage: %s [serial number]"%sys.argv[0])
    exit()
print ("#>" + sys.argv[1] + "<#")

def check_serial(serial):
    if (not set(serial).issubset(set(map(str,range(10))))):
        print ("only numbers allowed")
        return False
    if len(serial) != 20:
        return False
    if int(serial[15]) + int(serial[4]) != 10:
        return False
    if int(serial[1]) * int(serial[18]) != 2:
        return False
    if int(serial[15]) / int(serial[9]) != 1:
        return False
    if int(serial[17]) - int(serial[0]) != 4:
        return False
    if int(serial[5]) - int(serial[17]) != -1:
        return False
    if int(serial[15]) - int(serial[1]) != 5:
        return False
    if int(serial[1]) * int(serial[10]) != 18:
        return False
    if int(serial[8]) + int(serial[13]) != 14:
        return False
    if int(serial[18]) * int(serial[8]) != 5:
        return False
    if int(serial[4]) * int(serial[11]) != 0:
        return False
    if int(serial[8]) + int(serial[9]) != 12:
        return False
    if int(serial[12]) - int(serial[19]) != 1:
        return False
    if int(serial[9]) % int(serial[17]) != 7:
        return False
    if int(serial[14]) * int(serial[16]) != 40:
        return False
    if int(serial[7]) - int(serial[4]) != 1:
        return False
    if int(serial[6]) + int(serial[0]) != 6:
        return False
    if int(serial[2]) - int(serial[16]) != 0:
        return False
    if int(serial[4]) - int(serial[6]) != 1:
        return False
    if int(serial[0]) % int(serial[5]) != 4:
        return False
    if int(serial[5]) * int(serial[11]) != 0:
        return False
    if int(serial[10]) % int(serial[15]) != 2:
        return False
    if int(serial[11]) / int(serial[3]) != 0:
        return False
    if int(serial[14]) - int(serial[13]) != -4:
        return False
    if int(serial[18]) + int(serial[19]) != 3:
        return False
    return True
if check_serial(sys.argv[1]):
    print ("Thank you! Your product has been verified!")
else:
    print ("I'm sorry that is incorrect. Please use a valid RoboCorpIntergalactic serial number")
解题代码如下，这个题很适合用z3来做，这里也是刚开始学习，练练手
from z3 import *
'''serial=[]
for i in range(20):
    serial[i]=Int('serial['+str(i)+']')
'''
serial=[Int('serial[%d]'%i) for i in range(20)]
solver=Solver()
solver.add(serial[15] + serial[4] == 10)
solver.add(serial[1] * serial[18] == 2 )
solver.add(serial[15] / serial[9] == 1)
solver.add(serial[17] - serial[0] == 4)
solver.add(serial[5] - serial[17] == -1)
solver.add(serial[15] - serial[1] == 5)
solver.add(serial[1] * serial[10] == 18)
solver.add(serial[8] + serial[13] == 14)
solver.add(serial[18] * serial[8] == 5)
solver.add(serial[4] * serial[11] == 0)
solver.add(serial[8] + serial[9] == 12)
solver.add(serial[12] - serial[19] == 1)
solver.add(serial[9] % serial[17] == 7)
solver.add(serial[14] * serial[16] == 40)
solver.add(serial[7] - serial[4] == 1)
solver.add(serial[6] + serial[0] == 6)
solver.add(serial[2] - serial[16] == 0)
solver.add(serial[4] - serial[6] == 1)
solver.add(serial[0] % serial[5] == 4)
solver.add(serial[5] * serial[11] == 0)
solver.add(serial[10] % serial[15] == 2)
solver.add(serial[11] / serial[3] == 0)
solver.add(serial[14] - serial[13] == -4)
solver.add(serial[18] + serial[19] == 3)


for i in range(20):
    solver.add(serial[i]>=0,serial[i]<10)

solver.add(serial[3]!=0)

if solver.check()==sat:
    m=solver.model()
    #print(m.decls())
    print(m)
    for i in m.decls():
        print(m[i]),




from z3 import *
'''serial=[]
for i in range(20):
    serial[i]=Int('serial['+str(i)+']')
'''
serial=[Int('serial[%d]'%i) for i in range(20)]
solver=Solver()
solver.add(serial[15] + serial[4] == 10)
solver.add(serial[1] * serial[18] == 2 )
solver.add(serial[15] / serial[9] == 1)
solver.add(serial[17] - serial[0] == 4)
solver.add(serial[5] - serial[17] == -1)
solver.add(serial[15] - serial[1] == 5)
solver.add(serial[1] * serial[10] == 18)
solver.add(serial[8] + serial[13] == 14)
solver.add(serial[18] * serial[8] == 5)
solver.add(serial[4] * serial[11] == 0)
solver.add(serial[8] + serial[9] == 12)
solver.add(serial[12] - serial[19] == 1)
solver.add(serial[9] % serial[17] == 7)
solver.add(serial[14] * serial[16] == 40)
solver.add(serial[7] - serial[4] == 1)
solver.add(serial[6] + serial[0] == 6)
solver.add(serial[2] - serial[16] == 0)
solver.add(serial[4] - serial[6] == 1)
solver.add(serial[0] % serial[5] == 4)
solver.add(serial[5] * serial[11] == 0)
solver.add(serial[10] % serial[15] == 2)
solver.add(serial[11] / serial[3] == 0)
solver.add(serial[14] - serial[13] == -4)
solver.add(serial[18] + serial[19] == 3)


for i in range(20):
    solver.add(serial[i]>=0,serial[i]<10)

solver.add(serial[3]!=0)

if solver.check()==sat:
    m=solver.model()
    #print(m.decls())
    print(m)
    for i in m.decls():
        print(m[i]),


[招生]科锐逆向工程师培训(2024年11月15日实地，远程教学同时开班, 第51期)

上传的附件：
收藏
免费 ・2
支持
分享
最新回复 (0)
游客
登录 | 注册 方可回帖
回帖 表情 雪币赚取及消费
高级回复
返回
//