메뉴 닫기

z3 에서 Object를 Index로 사용하는법

; 부제 : z3 TypeError: object cannot be interpreted as an index 해결하기

일단 시작하기에 앞서… 이렇게 하면 속도가 매우! 떨어진다. 꼭 필요한 경우가 아니면 사용하지 말자!!!

예를들어 이런 코드가 있다고 하자.

이 코드의 작성자는 z3가 3 이 몇번쨰 인덱스에 들어있는지 찾아주기를 바랬을 것이다.

그러나 파이썬의 문법상의 제약으로 object (혹은 인스턴스) 는 배열의 인덱스로 사용되지 못한다.

이러한 문법적 제약을 극복하려면 Array 와 Store, Select를 사용하면 된다.

Array 의 첫번째 인자는 z3 내부에서 사용될 이름, 두번째 인자는 인덱스의 Sort(-자료형 이라고 이해하면 편하다-), 세번째 인자는 값의 Sort 이다.

아래 예시는 z3를 이용해 crc32 역연산을 하는 것이다. 테이블을 사용하는 것과 테이블을 사용하지 않는 것 모두를 구현하였는데, 돌려보면 알겠지만 속도차이가 상당하다.

<crc32 reverse with table>

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75

 

 

from z3 import *
 
 
crc32_tab = [
    0x000000000x770730960xee0e612c0x990951ba0x076dc4190x706af48f,
    0xe963a5350x9e6495a3, 0x0edb88320x79dcb8a40xe0d5e91e0x97d2d988,
    0x09b64c2b0x7eb17cbd0xe7b82d070x90bf1d910x1db710640x6ab020f2,
    0xf3b971480x84be41de, 0x1adad47d0x6ddde4eb0xf4d4b5510x83d385c7,
    0x136c98560x646ba8c00xfd62f97a0x8a65c9ec, 0x14015c4f0x63066cd9,
    0xfa0f3d630x8d080df5, 0x3b6e20c80x4c69105e0xd56041e40xa2677172,
    0x3c03e4d10x4b04d4470xd20d85fd0xa50ab56b, 0x35b5a8fa0x42b2986c,
    0xdbbbc9d60xacbcf940, 0x32d86ce30x45df5c750xdcd60dcf0xabd13d59,
    0x26d930ac0x51de003a0xc8d751800xbfd061160x21b4f4b50x56b3c423,
    0xcfba95990xb8bda50f0x2802b89e0x5f0588080xc60cd9b20xb10be924,
    0x2f6f7c870x58684c110xc1611dab0xb6662d3d, 0x76dc41900x01db7106,
    0x98d220bc0xefd5102a0x71b185890x06b6b51f0x9fbfe4a50xe8b8d433,
    0x7807c9a20x0f00f9340x9609a88e0xe10e98180x7f6a0dbb0x086d3d2d,
    0x91646c970xe6635c010x6b6b51f40x1c6c61620x856530d80xf262004e,
    0x6c0695ed0x1b01a57b0x8208f4c10xf50fc4570x65b0d9c60x12b7e950,
    0x8bbeb8ea0xfcb9887c0x62dd1ddf0x15da2d490x8cd37cf30xfbd44c65,
    0x4db261580x3ab551ce0xa3bc00740xd4bb30e20x4adfa5410x3dd895d7,
    0xa4d1c46d0xd3d6f4fb0x4369e96a0x346ed9fc0xad6788460xda60b8d0,
    0x44042d730x33031de50xaa0a4c5f0xdd0d7cc90x5005713c0x270241aa,
    0xbe0b10100xc90c20860x5768b5250x206f85b30xb966d4090xce61e49f,
    0x5edef90e0x29d9c9980xb0d098220xc7d7a8b40x59b33d170x2eb40d81,
    0xb7bd5c3b0xc0ba6cad0xedb883200x9abfb3b60x03b6e20c0x74b1d29a,
    0xead547390x9dd277af0x04db26150x73dc16830xe3630b120x94643b84,
    0x0d6d6a3e0x7a6a5aa80xe40ecf0b0x9309ff9d0x0a00ae270x7d079eb1,
    0xf00f93440x8708a3d20x1e01f2680x6906c2fe0xf762575d0x806567cb,
    0x196c36710x6e6b06e70xfed41b760x89d32be00x10da7a5a0x67dd4acc,
    0xf9b9df6f0x8ebeeff90x17b7be430x60b08ed50xd6d6a3e80xa1d1937e,
    0x38d8c2c40x4fdff2520xd1bb67f10xa6bc57670x3fb506dd0x48b2364b,
    0xd80d2bda0xaf0a1b4c0x36034af60x41047a600xdf60efc30xa867df55,
    0x316e8eef0x4669be790xcb61b38c0xbc66831a0x256fd2a00x5268e236,
    0xcc0c77950xbb0b47030x220216b90x5505262f0xc5ba3bbe0xb2bd0b28,
    0x2bb45a920x5cb36a040xc2d7ffa70xb5d0cf310x2cd99e8b0x5bdeae1d,
    0x9b64c2b00xec63f2260x756aa39c0x026d930a0x9c0906a90xeb0e363f,
    0x720767850x050057130x95bf4a820xe2b87a140x7bb12bae0x0cb61b38,
    0x92d28e9b0xe5d5be0d0x7cdcefb70x0bdbdf210x86d3d2d40xf1d4e242,
    0x68ddb3f80x1fda836e0x81be16cd0xf6b9265b0x6fb077e10x18b74777,
    0x88085ae60xff0f6a700x66063bca0x11010b5c0x8f659eff0xf862ae69,
    0x616bffd30x166ccf450xa00ae2780xd70dd2ee0x4e0483540x3903b3c2,
    0xa76726610xd06016f70x4969474d0x3e6e77db0xaed16a4a0xd9d65adc,
    0x40df0b660x37d83bf00xa9bcae530xdebb9ec50x47b2cf7f0x30b5ffe9,
    0xbdbdf21c0xcabac28a0x53b393300x24b4a3a60xbad036050xcdd70693,
    0x54de57290x23d967bf0xb3667a2e0xc4614ab80x5d681b020x2a6f2b94,
    0xb40bbe370xc30c8ea10x5a05df1b0x2d02ef8d
]
 
def z3crc32new(data,length):
    Z3CrcTab = Array('Z3CrcTab',BitVecSort(32),BitVecSort(32))
    for i in range(0,len(crc32_tab)):
        Z3CrcTab = Store(Z3CrcTab,i,BitVecVal(crc32_tab[i],32))
 
    crc = BitVecVal(0xffffffff,32)
    for pos in range(0,length):
        idx = (crc ^ ZeroExt(24,data[pos])) & 0xff
        crc = (Select(Z3CrcTab,  idx) ^ LShR(crc,8)) & 0xffffffff
    return crc ^ BitVecVal(0xffffffff,32)
 
LEN_STR = 5
 
arr = [ BitVec('a%i'%i,8for i in range(0,LEN_STR)]
= Solver()
s.add(z3crc32new(arr,len(arr)) == 0xdeadbeef)
for i in range(0,len(arr)):
    s.add(And(arr[i] >= 0x20, arr[i] < 0x7f))
print s.check()
= s.model()
 
sTemp = ""
for i in range(0,LEN_STR):
    sTemp += chr(m[arr[i]].as_long())
print sTemp
 

 

 

cs

 <crc32 reverse without table>

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

 

 

from z3 import *
def isAscii(s,x,length):
    for i in range(length):
        s.add( And(0x20 <= x[i],x[i] < 0x7f))
 
def z3crc32(data,length):
    crc = BitVecVal(0xffffffff,32)
    for block in range(0,length):
        crc ^= ZeroExt(24,data[block])
        for i in range(8):
            crc = If(crc & 1 == BitVecVal(1,32), LShR(crc, 1) ^ 0xedb88320, LShR(crc, 1))
            crc &= BitVecVal(0xffffffff,32)
    return crc ^ 0xffffffff
def Breakcrc32(_crc,length):
    s = Solver()
    data = [ BitVec('a%i'%i,8for i in range(0,length)]
    crc = z3crc32(data,length)
    isAscii(s,data,length)
    s.add(crc == _crc)
    print  s.check()
    while s.check() == sat:
      m = s.model()
 
      #Print
      sTemp = ""
      for i in range(0,length):
          sTemp += chr(m[data[i]].as_long())
      print sTemp
 
      #Get Multiple Solution
      OrList = []
      for i in range(0,length):
          OrList.append(data[i] != m[data[i]])
      s.add(Or(OrList))
 
Breakcrc32(0xdeadbeef,5)
print "End"
 

 

 

cs

 

댓글 남기기

이메일은 공개되지 않습니다.