CODEWITHSUNDEEP
pythonz3z3py
Ahmed Ezzat
Ahmed Ezzat

Reputation: 85

How to Solve this in z3 only

i have past ctf challange which i know how to solve but i need to solve it completely in z3 only without using any tools other than z3, i tried to use the user_input as array of BitVec but z3 failed to find the solution the goal here to make the final v3 equal to FLAG[i]
the final flag is 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

Upvotes: 1

Views: 597

Answers (1)

Coldzer0
Coldzer0

Reputation: 38

here's my solution :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 + '}'

Upvotes: 1

Related Questions