用 z3py 解决一个crackme

Question

我想用Z3解决一个crackme。这个crackme非常庞大，但可以简化为以下内容：：

#! /usr/bin/python

import sys
T='Fguad2x-GP5_QqNi'
key=sys.argv[1]

if len(key) != 3:
    print "Bad key length"
    exit(1)

out=[]
for c in key:
    out.append(T[ord(c)>>4 ])
    out.append(T[ord(c) & 0xf])

if ''.join(out)=='--xPxN':
    print "You win"

解决方案是'赢'。

我猜这种事情可以用 z3 解决。我首先以 z3 风格翻译了所有来自crackme 的逻辑：

#! /usr/bin/python

from z3 import *

#Preparing data
map_array='Fguad2x-GP5_QqNi'
T=Array('T',IntSort(),IntSort())
for i,j in enumerate(map_array):
    T = Store(T, ord(j), i)
sol='--xPxN'

#We know input has 3 characters
a=BitVec('a',8)
b=BitVec('b',8)
c=BitVec('c',8)

#Ignite
s=Solver()

#String key is printable
s.add(BV2Int(a)>=65,BV2Int(a)<=122)
s.add(BV2Int(b)>=65,BV2Int(b)<=122)
s.add(BV2Int(c)>=65,BV2Int(c)<=122)

#Adding constraints
s.add(Select(T,BV2Int(a>>4))==ord(sol[0]))
s.add(Select(T,BV2Int(a&0xf))==ord(sol[1]))
s.add(Select(T,BV2Int(b>>4))==ord(sol[2]))
s.add(Select(T,BV2Int(b&0xf))==ord(sol[3]))
s.add(Select(T,BV2Int(c>>4))==ord(sol[4]))
s.add(Select(T,BV2Int(c&0xf))==ord(sol[5]))

#Verify solving
print s.check()
print s.model()

现在，我有一些问题：

• s.check() 说 'sat' 所以我至少有一个解决方案？
• 有没有更好的方法来定义数组？
• 有没有办法直接使用字符？

• 解决后如何只得到a，b和c？ s.model() 显示了一个非常奇怪的输出：

  $ ./stovlfw.py

  坐 [b = 1， a = 136, c = 0, T = [3 -> 78, 65 -> 120, 2 -> 80, 1 -> 45, 0 -> 45, 否则-> 45]， k!0 = [3 -> 78, 65 -> 120, 2 -> 80, 1 -> 45, 0 -> 45, 否则-> 45]]

这似乎与约束相矛盾（？？）我做错了什么，但在哪里？

谢谢

Answer 1

z3 中的数组的行为与 C 对应物不同。它们不应该用于模拟小的有限值集合。使用列表推导式创建不同的变量通常效率更高。

这是我的替代方法。在 z3 中创建一个函数，让您从字符串中选择第 n 个字符。

#! /usr/bin/python

from z3 import *

#Preparing data
nth = Function('nth', StringSort(), IntSort(), BitVecSort(8))
final = String('final')
sol='--xPxN'

#We know input has 3 characters
a=BitVec('a',8)
b=BitVec('b',8)
c=BitVec('c',8)

#Ignite
s=Solver()

#Adding constraints
for i,j in enumerate('Fguad2x-GP5_QqNi'):
    s.add(nth(final,i)==ord(j))

s.add(nth(final,BV2Int(a>>4))==ord(sol[0]))
s.add(nth(final,BV2Int(a&0xf))==ord(sol[1]))
s.add(nth(final,BV2Int(b>>4))==ord(sol[2]))
s.add(nth(final,BV2Int(b&0xf))==ord(sol[3]))
s.add(nth(final,BV2Int(c>>4))==ord(sol[4]))
s.add(nth(final,BV2Int(c&0xf))==ord(sol[5]))

#String key is printable
s.add((a)>=65,(a)<=122)
s.add((b)>=65,(b)<=122)
s.add((c)>=65,(c)<=122)

#Verify solving Fguad2x-GP5_QqNi
print s.check()
print s.model()
print ''.join(chr(s.model()[i].as_long()) for i in [a,b,c])

s.model() 可以用作字典来检索变量值。

PS : 将您的 z3 升级到最新版本才能正常工作。