Real_world_crackme

Real_world_crackme_writeup

WEB Crackme

Author : X3eRo0
Language : JS
Upload : Fri, 29 May 2020 05:09:29
Difficulty: 5 (this is relative lol)
Platform : Unix/Linux etc.
Crackme : WEB Crackme

Desc: 

    - find the correct password for the crackme to display "Correct Password" message.
    - your goal is not to make the app display "Correct Password" but to find the correct password which does that for you.
    - bruteforcing wont help but you can do whatever you want.
    - this challenge is not supposed to be hosted, please do not deploy     this in the real world this is only for purpose of this challenge.
    - flag format ritsCTF{<---flag-here--->}.
    - Good Luck.

Hey there! This week’s crackme from f5-experts was from me. So here i am with another shitty writeup.

This was one of the less solved WEB Crackme, yes web crackmes do exists. so it was’nt super hard or anything just some basic anti-debugging tricks and obfuscated js. the challenge was to get the script in a somewhat readable form and understand the check function.

The crackme looks like this when loaded in browser.

You can enter your password, there is not input box. The crackme gets the keystrokes directly.

if you check the source code for crackme.html, you will see that all the logic is in crackme.js

...
<script src="crackme.js"></script>
...

But if you look into crackme.js you will find an

eval(atob('....'))

After get the base64 decoded js we see that its heavily obfuscated, but function names are still preserved.

At this point you can try to load the script in browser and do dynamic analysis but you will end up crashing your browser. The script detects if its running in debugger and it will start an infinite loop.

you can use the anti-anti-debugging script and this script actually works.

Now we can finally take a look at the check function. Looking at the if conditions you can see that you will use z3 here, because the checks are linear equations here, if your password’s characters satisfies these checks then it will print Correct Password.

...
var check = function (password) {
...

I renamed the parameter to the check function as password because the parameter is an array so it has to be the password array.

So lets look at some of the checks -

if (password[0x8] == password[0x23]) {
    if (password[0x9] != password[0x22]) {
        return False;
    }
    if (password[0x9] != '-') {
        return False;
    }
    if (password[0x22] != password[0x23]) {
        return False;
    }
    var _0x873b25 = password[0x22].charCodeAt();
    if (_0x873b25 % 0x9 != 0x0) {
        return False;
    }
    if (_0x873b25 % 0x5 != 0x0) {
        return False;
    }
    if (_0x873b25 % 0x28 != 0x5) {
        return False;
    }
} else {
    return False;
}

In this check you can see it will fail if password[0x8] does’nt match with password[0x23], if they do match however, there are some more checks. So you can see its super easy to build a solver script for it.

if you are not familiar with z3, i will give you a breif introduction to it. We will use the python z3-solver to get the flag. BUT WHAT IS z3

z3

Z3 is a POWERFULL Theorem Prover, it is an Efficient SMT-Solver library build by Microsoft. So basically z3 is able to solve math equations for us, its super helpfull when we encounter challenges like this where our little brain can’t solve equations, we use z3 when the equations are either very complex to solve or if they are large in number.

To get started we will initialize the z3 vectors. These vectors are z3 types that will be used to make equations.

from z3 import * # import everything from z3

# this inp list is the list of 'password' vectors
# basically i have defined each character of password
# as a vector.
inp = [BitVec("inp[%d]" % i, 32) for i in range(0, 0x25)]

# initialize the z3 solver
z3_solver = Solver()

flag = "" # the string where we will get the flag

So you have initialized z3, all you have to do now is express the check function in form of equations and give those equations to z3.

For example this is one of the checks in the check function.

if (password[0x9] != '-') {
    return False;
}
if (password[0x22] != password[0x23]) {
    return False;
}

You can translate this checks into z3 equations like this.

	z3_solver.add(inp[0x9] == 45)
	z3_solver.add(inp[0x22] == inp[0x23])

After you have added all the equations to z3, z3 will now solve this equations and it will create a model for those equations. if the set of equations is satisfiable, then z3_solver.check() will return sat, otherwise unsat. If it returns sat you can ask z3 to give you the model.

if z3_solver.check() == sat:
    sol = z3_solver.model()
    for i in range(0x25):
        try:
            #print(str(hex(i)) + ": " + str(sol[inp[i]]))
            flag += chr(int(str(sol[inp[i]])))
        except:
            pass
            #print(str(hex(i)) + ": " + str(sol[inp[i]]))

The full solver script is here.

#!/usr/bin/python

from z3 import *

inp = [BitVec("inp[%d]" % i,32)for i in range(0,0x25)]

z3_solver = Solver()
flag = ""

# inp
for i in range(0,len(inp)):

	z3_solver.add(inp[14] == 95)
	z3_solver.add(inp[0x24] - inp[0x7] == 2)
	z3_solver.add(inp[0x24] == 125)
	z3_solver.add(inp[0x8] == inp[0x23])
	z3_solver.add(inp[0x9] == inp[0x22])
	z3_solver.add(inp[0x9] == 45)
	z3_solver.add(inp[0x22] == inp[0x23])
	z3_solver.add(inp[0xa] - inp[0x8]*3 + 0xe == 0)
	z3_solver.add(inp[0xb] == 0x30)
	z3_solver.add(inp[0xc] == 117) 
	z3_solver.add(inp[0x15] == 119) 
	z3_solver.add(inp[0xd]%0x6 == 0)
	z3_solver.add(inp[0xd] == 114)
	z3_solver.add(inp[0xe] ^ inp[0x14] ^ inp[0x18] ^ inp[0x1f] == 0)
	z3_solver.add(inp[0xf] == 102)
	z3_solver.add(inp[0x10] == 0x31)
	z3_solver.add(inp[0x11] == 114)
	z3_solver.add(inp[0x11] + 0x1 == inp[0x12])
	z3_solver.add(inp[0x11] + 0x2 == inp[0x13])
	z3_solver.add(inp[0x15] == 119)
	z3_solver.add(inp[0x16] == 0x33)
	z3_solver.add(inp[24] == (inp[26] - 19))
	z3_solver.add(inp[20] == inp[24])
	z3_solver.add(inp[0x17] == 98)
	z3_solver.add(inp[0x19] == 99)
	z3_solver.add(inp[0x1a] == 114)
	z3_solver.add(inp[0x1b] == 0x34)
	z3_solver.add(inp[0x1c] ^ 0x20 == 75)
	z3_solver.add(inp[0x1d] == 109)
	z3_solver.add(inp[0x1e] == 101)
	z3_solver.add(inp[0x20] == 88)
	z3_solver.add(inp[0x21] == 79)
	z3_solver.add(inp[0x0] == 114)
	z3_solver.add(inp[0x1] == 105)
	z3_solver.add(inp[0x2] == 102)
	z3_solver.add(inp[0x3] == 116)
	z3_solver.add(inp[0x4] == 67)
	z3_solver.add(inp[0x5] == 84)
	z3_solver.add(inp[0x6] == 70)

	if z3_solver.check() == sat:
		sol = z3_solver.model()
		for i in range(0x25):
			try:
				flag += chr(int(str(sol[inp[i]])))
			except:
				pass
		break

print(flag)

The Output –

~/web_crackme » python solve.py
riftCTF{--y0ur_f1rst_w3b_cr4kme_XO--}

AND THATS HOW YOU USE Z3 FOLKS.