首页 网络安全

Z3是一个微软研究院开源的theorem prover(定理证明器),支持位向量、布尔、数组、浮点数、字符串以及其他数据类型。Z3是一个SMT solver以及支持SMTLIB的格式。

求解步骤

  1. 首先给变量赋值
  2. 设置一个解方程的类Solver
  3. 添加约束条件
  4. 查看有没有解solver.check()
  5. 得到解 solver.model()

常用方法

  • BitVec是无符号数,Int是有符号数
  • check() 检查是否有解
  • model() 以列表的方式输出解

三元一次方程

#!/usr/bin/env python3
from z3 import *
x,y,z = Ints('x y z')
s = Solver()
s.add(2*x+3*y+z==6)
s.add(x-y+2*z==-1)
s.add(x+2*y-z==5)
print(s.check())
print(s.model())

求模运算

#!/usr/bin/env python3
from z3 import *
x = Int('x')
s = Solver()
a = 65537
b = 64837
c = 41958
s.add(x>0)
s.add(x%a == b)
s.add(x%b == c)
print(s.check())
print(s.model())

一道CTF题

from z3 import *

s = Solver()

v1 = [0x4f17,0x9cf6,0x8ddb,0x8ea6,0x6929,0x9911,0x40a2,0x2f3e,0x62b6,0x4b82,0x486c,0x4002,0x52d7,0x2def,0x28dc,0x640d,0x528f,0x613b,0x4781,0x6b17,0x3237,0x2a93,0x615f,0x50be,0x598e,0x4656,0x5b31,0x313a,0x3010,0x67fe,0x4d5f,0x58db,0x3799,0x60a0,0x2750,0x3759,0x8953,0x7122,0x81f9,0x5524,0x8971,0x3a1d]
v2 = [BitVec('intput_%d' % i,8) for i in range(42)]
# 确定约束条件
s.add(v1[0] == 34 * v2[3] + 12 * v2[0] + 53 * v2[1] + 6 * v2[2] + 58 * v2[4] + 36 * v2[5] + v2[6])
s.add(v1[1] == 27 * v2[4] + 73 * v2[3] + 12 * v2[2] + 83 * v2[0] + 85 * v2[1] + 96 * v2[5] + 52 * v2[6])
s.add(v1[2] == 24 * v2[2] + 78 * v2[0] + 53 * v2[1] + 36 * v2[3] + 86 * v2[4] + 25 * v2[5] + 46 * v2[6])
s.add(v1[3] == 78 * v2[1] + 39 * v2[0] + 52 * v2[2] + 9 * v2[3] + 62 * v2[4] + 37 * v2[5] + 84 * v2[6])
s.add(v1[4] == 48 * v2[4] + 14 * v2[2] + 23 * v2[0] + 6 * v2[1] + 74 * v2[3] + 12 * v2[5] + 83 * v2[6])
s.add(v1[5] == 15 * v2[5] + 48 * v2[4] + 92 * v2[2] + 85 * v2[1] + 27 * v2[0] + 42 * v2[3] + 72 * v2[6])
s.add(v1[6] == 26 * v2[5] + 67 * v2[3] + 6 * v2[1] + 4 * v2[0] + 3 * v2[2] + 68 * v2[6])
s.add(v1[7] == 34 * v2[10] + 12 * v2[7] + 53 * v2[8] + 6 * v2[9] + 58 * v2[11] + 36 * v2[12] + v2[13])
s.add(v1[8] == 27 * v2[11] + 73 * v2[10] + 12 * v2[9] + 83 * v2[7] + 85 * v2[8] + 96 * v2[12] + 52 * v2[13])
s.add(v1[9] == 24 * v2[9] + 78 * v2[7] + 53 * v2[8] + 36 * v2[10] + 86 * v2[11] + 25 * v2[12] + 46 * v2[13])
s.add(v1[10] == 78 * v2[8] + 39 * v2[7] + 52 * v2[9] + 9 * v2[10] + 62 * v2[11] + 37 * v2[12] + 84 * v2[13])
s.add(v1[11] == 48 * v2[11] + 14 * v2[9] + 23 * v2[7] + 6 * v2[8] + 74 * v2[10] + 12 * v2[12] + 83 * v2[13])
s.add(v1[12] == 15 * v2[12] + 48 * v2[11] + 92 * v2[9] + 85 * v2[8] + 27 * v2[7] + 42 * v2[10] + 72 * v2[13])
s.add(v1[13] == 26 * v2[12] + 67 * v2[10] + 6 * v2[8] + 4 * v2[7] + 3 * v2[9] + 68 * v2[13])
s.add(v1[14] == 34 * v2[17] + 12 * v2[14] + 53 * v2[15] + 6 * v2[16] + 58 * v2[18] + 36 * v2[19] + v2[20])
s.add(v1[15] == 27 * v2[18] + 73 * v2[17] + 12 * v2[16] + 83 * v2[14] + 85 * v2[15] + 96 * v2[19] + 52 * v2[20])
s.add(v1[16] == 24 * v2[16] + 78 * v2[14] + 53 * v2[15] + 36 * v2[17] + 86 * v2[18] + 25 * v2[19] + 46 * v2[20])
s.add(v1[17] == 78 * v2[15] + 39 * v2[14] + 52 * v2[16] + 9 * v2[17] + 62 * v2[18] + 37 * v2[19] + 84 * v2[20])
s.add(v1[18] == 48 * v2[18] + 14 * v2[16] + 23 * v2[14] + 6 * v2[15] + 74 * v2[17] + 12 * v2[19] + 83 * v2[20])
s.add(v1[19] == 15 * v2[19] + 48 * v2[18] + 92 * v2[16] + 85 * v2[15] + 27 * v2[14] + 42 * v2[17] + 72 * v2[20])
s.add(v1[20] == 26 * v2[19] + 67 * v2[17] + 6 * v2[15] + 4 * v2[14] + 3 * v2[16] + 68 * v2[20])
s.add(v1[21] == 34 * v2[24] + 12 * v2[21] + 53 * v2[22] + 6 * v2[23] + 58 * v2[25] + 36 * v2[26] + v2[27])
s.add(v1[22] == 27 * v2[25] + 73 * v2[24] + 12 * v2[23] + 83 * v2[21] + 85 * v2[22] + 96 * v2[26] + 52 * v2[27])
s.add(v1[23] == 24 * v2[23] + 78 * v2[21] + 53 * v2[22] + 36 * v2[24] + 86 * v2[25] + 25 * v2[26] + 46 * v2[27])
s.add(v1[24] == 78 * v2[22] + 39 * v2[21] + 52 * v2[23] + 9 * v2[24] + 62 * v2[25] + 37 * v2[26] + 84 * v2[27])
s.add(v1[25] == 48 * v2[25] + 14 * v2[23] + 23 * v2[21] + 6 * v2[22] + 74 * v2[24] + 12 * v2[26] + 83 * v2[27])
s.add(v1[26] == 15 * v2[26] + 48 * v2[25] + 92 * v2[23] + 85 * v2[22] + 27 * v2[21] + 42 * v2[24] + 72 * v2[27])
s.add(v1[27] == 26 * v2[26] + 67 * v2[24] + 6 * v2[22] + 4 * v2[21] + 3 * v2[23] + 68 * v2[27])
s.add(v1[28] == 34 * v2[31] + 12 * v2[28] + 53 * v2[29] + 6 * v2[30] + 58 * v2[32] + 36 * v2[33] + v2[34])
s.add(v1[29] == 27 * v2[32] + 73 * v2[31] + 12 * v2[30] + 83 * v2[28] + 85 * v2[29] + 96 * v2[33] + 52 * v2[34])
s.add(v1[30] == 24 * v2[30] + 78 * v2[28] + 53 * v2[29] + 36 * v2[31] + 86 * v2[32] + 25 * v2[33] + 46 * v2[34])
s.add(v1[31] == 78 * v2[29] + 39 * v2[28] + 52 * v2[30] + 9 * v2[31] + 62 * v2[32] + 37 * v2[33] + 84 * v2[34])
s.add(v1[32] == 48 * v2[32] + 14 * v2[30] + 23 * v2[28] + 6 * v2[29] + 74 * v2[31] + 12 * v2[33] + 83 * v2[34])
s.add(v1[33] == 15 * v2[33] + 48 * v2[32] + 92 * v2[30] + 85 * v2[29] + 27 * v2[28] + 42 * v2[31] + 72 * v2[34])
s.add(v1[34] == 26 * v2[33] + 67 * v2[31] + 6 * v2[29] + 4 * v2[28] + 3 * v2[30] + 68 * v2[34])
s.add(v1[35] == 34 * v2[38] + 12 * v2[35] + 53 * v2[36] + 6 * v2[37] + 58 * v2[39] + 36 * v2[40] + v2[41])
s.add(v1[36] == 27 * v2[39] + 73 * v2[38] + 12 * v2[37] + 83 * v2[35] + 85 * v2[36] + 96 * v2[40] + 52 * v2[41])
s.add(v1[37] == 24 * v2[37] + 78 * v2[35] + 53 * v2[36] + 36 * v2[38] + 86 * v2[39] + 25 * v2[40] + 46 * v2[41])
s.add(v1[38] == 78 * v2[36] + 39 * v2[35] + 52 * v2[37] + 9 * v2[38] + 62 * v2[39] + 37 * v2[40] + 84 * v2[41])
s.add(v1[39] == 48 * v2[39] + 14 * v2[37] + 23 * v2[35] + 6 * v2[36] + 74 * v2[38] + 12 * v2[40] + 83 * v2[41])
s.add(v1[40] == 15 * v2[40] + 48 * v2[39] + 92 * v2[37] + 85 * v2[36] + 27 * v2[35] + 42 * v2[38] + 72 * v2[41])
s.add(v1[41] == 26 * v2[40] + 67 * v2[38] + 6 * v2[36] + 4 * v2[35] + 3 * v2[37] + 68 * v2[41])

if s.check() != sat: #判断是否有解
    print('unsat!')
else:
    m = s.model()   #有解,输出答案赋值给m

    print(repr("".join([chr(m[v2[i]].as_long()) for i in range(42)])))

pycharm求解:
dUOQBt.md.png




文章评论