python - 如何仅在 z3 中解决此问题

Question

我曾经遇到过 ctf 挑战，我知道如何解决但我只需要在z3中完全解决它，而不使用z3以外的任何工具，我尝试使用 user_input 作为 BitVec 数组，但 z3 未能找到解决方案，此处的目标是使最终 v3 等于 FLAG[i]
最终标志是 round_r0und ....

FLAG = [0x726F756E, 0xCABEE660, 0xDDC1997D, 0xAA93C38B, 0x87E21216]
user_input = bytearray("")

def n1(a1,a2,a3):
    return (a1 - a2 + a3) % 26 + a2

def ENC(a1,a2):
    if ( a1 > 96 and a1 <= 122 ):
        return n1(a1, 0x61, a2)
    if ( a1 <= 64 or a1 > 90 ):
        return a1
    return n1(a1, 0x41, a2)

def FINAL(a1,a2):
    return (a1 << (a2 & 0x1F)) | (a1 >> (-(a2 & 0x1F) & 0x1F))

for i in range(4):
   enc = 0;
   for  j in range(3):
     enc |= ENC(user_input[4 * i + j], i) << 8 * (3 - j)
   v3 = FLAG[i]

   if( v3 != FINAL(enc, i) ):
    break

Answer 1

这是我的解决方案:D

from z3 import *

flag_en = [0x726F756E, 0xCABEE660, 0xDDC1997D, 0xAA93C38B, 0x87E21216]


def toStr(h):
    hex_str = []
    while h != 0x0:
        hex_str.append(chr(h & 0xFF))
        h = h >> 8
    hex_str.reverse()
    return ''.join(hex_str)


def rotate(txt, key):
    def cipher(i, low=range(97, 123), upper=range(65, 91)):
        if i in low or i in upper:
            s = 65 if i in upper else 97
            i = (i - s - key) % 26 + s
        return chr(i)
    return ''.join([cipher(ord(s)) for s in txt])


Flag = ''

s = Solver()
a = BitVec('a', 32)
s = Solver()

for i in range(0, 5):
    s.reset()
    s.add(RotateLeft(a, i) == flag_en[i])
    s.check()
    m = s.model()
    x = toStr(m[a].as_long())
    Flag += rotate(x, i)

print 'flag{' + Flag + '}'