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から翻訳すべてのロジックで始まる：

• s.check（）と言うので、私は少なくとも一つの解決策を持っている「座っ」：

  #! /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() 
  

  は今、私はいくつかの質問がありますか？

• 配列を定義するより良い方法はありますか？
• 文字を直接使用する方法はありますか？

• ソリューションの後にa、b、cのみを取得するにはどうすればよいですか？ - > 78

  $ ./stovlfw.py

  座っ[B = 1、 = 136、 C = 0、 T = [3：s.model（）は、非常に奇妙な出力を示しています> 120、 - 、 65 - > 120、 2 - > 80、 1 - > 45、 0 - > 45、他 - > 45]、 K 0 = [3 - ！> 78、 65 2 - > 80、 1 - > 45、 0 - > 45、 else - > 45]]

これは制約と矛盾しているようです（??）私は何か間違っていますが、どこですか？

ありがとう

Answer 1

z3の配列はCの対応するものとして動作しません。小さな値のコレクションをモデル化するために使用すべきではありません。通常、リスト内包表記を使用してさまざまな変数を作成する方が効率的です。

私の代わりの方法です。文字列からn番目の文字を選択できるz3の関数を作成します。

#! /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を最新バージョンにアップグレードしてください。