Rating:
[Link to original writeup](https://wrecktheline.com/writeups/imaginary-2021/#password%20checker)
# Password Checker (15 solves, 450 points)
by JaGoTu
## Description
```
I seem to have forgotten my password. Before I lock myself out, I immediately went to my password checker that I coded, but it amounted to no avail. I guess I will leave it to the experts.
Wrap your flag in ictf before submitting.
Attachments
http://password-checker.chal.imaginaryctf.org
Author
Zyphen
Points
450
```
## Obfuscated JavaScript
The site has a single textbox to input the password, and after pressing the button it is checked in JavaScript.
The relevant part of the JavaScript after deobfuscation is this:
```JS
order = "3|2|0|1|4"["split"]("|"),
current_step = 0x0;
while ( !! []) {
switch (order[current_step++]) {
case 0:
var checksum = 0x0;
continue;
case 1:
for (var index = 0x0; index < password["length"]; index++) {
summed += password["charCodeAt"](index),
xored ^= password["charCodeAt"](index),
checksum = (checksum << 0x5) - checksum + password["charCodeAt"](index)
};
continue;
case 2:
var xored = 0x0;
continue;
case 3:
var summed = 0x0;
continue;
case 4:
console["log"](summed, xored, checksum); ! /[^ZYPH3NAFUR1GT_BMKLE.0]/ ["test"](password) &&
summed == 0x7e8 &&
xored == 0x7e &&
checksum == -0x28dd475e &&
password["charCodeAt"](0x0) - password["charCodeAt"](0x1) == 0x1 &&
Math["floor"](password["charCodeAt"](0x1) * password["charCodeAt"](0x2) * password["charCodeAt"](0x3) / 0x736) == 0x115 &&
password["charCodeAt"](0x4) + password["charCodeAt"](0x5) - password["charCodeAt"](0x6) + password["charCodeAt"](0x7) == 0x72 &&
Math["floor"](password["charCodeAt"](0x8) * password["charCodeAt"](0x9) / password["charCodeAt"](0xa) * password["charCodeAt"](0xb)) == 0xcb1 &&
Math["floor"](password["charCodeAt"](0xd) / password["charCodeAt"](0xc) / password["charCodeAt"](0xe) * password["charCodeAt"](0xf)) == 0x1 &&
(password["charCodeAt"](0x10) &&
password["charCodeAt"](0x12) == "ZYPH3NAFUR1GT_BMKLE.0"["length"] << 0x2) &&
password["charCodeAt"](0x6) == password["charCodeAt"](0x11) &&
Math["floor"](password["charCodeAt"](0x13) * password["charCodeAt"](0x14) / password["charCodeAt"](0x15)) == 0x2e &&
password["charCodeAt"](0x16) + password["charCodeAt"](0x17) - password["charCodeAt"](0x18) == 0x74 &&
password["charCodeAt"](0x19) + password["charCodeAt"](0x1a) + password["charCodeAt"](0x1b) == 0x8a &&
alert("Congrats!!!");
continue
};
break
}
```
The steps are in order 3-2-0-1-4, so first `summed`, `xored` and `checksum` are inited to zero, then in #1 the values of them are calculated, and then in #4 the actual checking takes place. The conditions mostly just take triplets of characters and check some conditions on them.
## Z3 and guessing
This looks like a task for z3, so we implement all the conditions:
```py
from z3 import *
chars = []
sum = 0
xored = 0
checksum = 0
s = SolverFor("QF_BV")
for i in range(28):
curr = BitVec('c' + str(i), 32)
chars.append(curr)
sum += curr
xored ^= curr
checksum = 31*checksum + curr
lol = (curr == ord('Z'))
for c in "YPH3NAFUR1GT_BMKLE.0":
lol = Or(lol, curr == ord(c))
s.add(lol)
def floor_div(top, bottom, res):
s.add(top > bottom*res)
s.add(top < bottom*res+bottom)
password = chars
s.add(sum==0x7e8)
s.add(xored == 0x7e)
s.add(checksum == 0xD722B8A2)
s.add(password[0x0] - password[0x1] == 0x1)
floor_div(password[0x1] * password[0x2] * password[0x3], 0x736, 0x115)
s.add(password[0x4] + password[0x5] - password[0x6] + password[0x7] == 0x72)
floor_div(password[0x8] * password[0x9] * password[0xb], password[0xa], 0xcb1)
floor_div(password[0xd]*password[0xf], password[0xc] * password[0xe],1 )
s.add(password[0x12] == 84)
s.add(password[0x6] == password[0x11])
floor_div(password[0x13] * password[0x14], password[0x15], 0x2e)
s.add(password[0x16] + password[0x17] - password[0x18] == 0x74)
s.add(password[0x19] + password[0x1a] + password[0x1b] == 0x8a)
print(s.check())
m = s.model()
out = ''
for i in range(28):
out += chr(m[password[i]].as_long())
print(out)
```
However, the search space is too large even when using the parallel evaluator ☹.
As we mentioned earlier, the characters are mostly conditioned in triplets. So let's try to go for
a more guessy approach, just see all the possible triplets and guess the ones that look the most english-y.
The last triplet is easy:
```py
$ cat test.py
import sys
lol = 'ZYPH3NAFUR1GT_BMKLE.0'
for a in lol:
for b in lol:
for c in lol:
if ((ord(a)+ord(b)+ord(c))) == 0x8a:
print(a+b+c)
$ python3 test.py
...
```
For the second to last triplet we get multiple options:
```py
$ cat test.py
import sys
lol = 'ZYPH3NAFUR1GT_BMKLE.0'
for a in lol:
for b in lol:
for c in lol:
if ((ord(a)+ord(b)-ord(c))) == 0x74:
print(a+b+c+"...")
$ python3 test.py
ZH....
Z_E...
ZM3...
ZK1...
YN3...
YK0...
YL1...
PU1...
PR....
PT0...
HZ....
H_3...
NY3...
NT....
F_1...
UP1...
UR3...
UM....
RP....
RU3...
RR0...
TP0...
TN....
_ZE...
_H3...
_F1...
_E0...
MZ3...
MU....
KZ1...
KY0...
LY1...
E_0...
```
After looking at this, the most english-like options are the `RU3...` and `UR3...`. So let's try the previous triplet with both of these:
```py
import sys
lol = 'ZYPH3NAFUR1GT_BMKLE.0'
for a in lol:
for b in lol:
for c in lol:
if (ord(a)*ord(b)//ord(c)) == 0x2e:
print(a+b+c+"UR3...")
print(a+b+c+"RU3...")
```
Not gonna include the full output, but one of them was `0RTUR3...`, which looks a lot like torture :) so we also guess `_T` before that.
Now let's try from the other side: the first three characters are actually a bit special, as the second character is in two conditions, `password["charCodeAt"](0x0) - password["charCodeAt"](0x1) == 0x1` and `Math["floor"](password["charCodeAt"](0x1) * password["charCodeAt"](0x2) * password["charCodeAt"](0x3) / 0x736) == 0x115`. Let's bruteforce both of them at once:
```py
$ cat test.py
import sys
lol = 'ZYPH3NAFUR1GT_BMKLE.0'
for a in lol:
if chr(ord(a)-1) in lol:
for b in lol:
for c in lol:
if ((ord(a)-1)*ord(b)*ord(c))//0x736== 0x115:
print(a+chr(ord(a)-1)+b+c)
$ python3 test.py
ZYPH
ZYHP
HGUU
HG_L
HGL_
NMF_
NM_F
GF_M
GFM_
MLZK
MLG_
ML_G
MLKZ
LKZL
LKH_
LK_H
LKLZ
```
Hm, one of them is ZYPH, and the author of this challenge is... Zyphen. :) Also, as `password[0x6] == password[0x11]`, we know the 7th character will be '_':
```py
import sys
lol = 'ZYPH3NAFUR1GT_BMKLE.0'
for a in lol:
for b in lol:
for c in ['_']:
for d in lol:
if ((ord(a)+ord(b)-ord(c))+ord(d)) == 0x72:
print("ZYPH" + a+b+c+d)
```
There's only one result containing ZYPHEN or ZYPH3N, and that is `ZYPH3N_P`.
To sum it all up, we know the password looks like the following:
`ZYPH3N_P?????????_T0RTUR3...`
That should be enough for our Z3 :) Let's add the following to the original script:
```py
s.add(password[27] == ord('.'))
s.add(password[26] == ord('.'))
s.add(password[25] == ord('.'))
s.add(password[24] == ord('3'))
s.add(password[23] == ord('R'))
s.add(password[22] == ord('U'))
s.add(password[21] == ord('T'))
s.add(password[20] == ord('R'))
s.add(password[19] == ord('0'))
s.add(password[18] == ord('T'))
s.add(password[17] == ord('_'))
s.add(password[0] == ord('Z'))
s.add(password[1] == ord('Y'))
s.add(password[2] == ord('P'))
s.add(password[3] == ord('H'))
s.add(password[4] == ord('3'))
s.add(password[5] == ord('N'))
s.add(password[6] == ord('_'))
s.add(password[7] == ord('P'))
```
And after a while we get the result:
```
$ python3 checker.py
sat
ZYPH3N_P1Z_F0RG3T_T0RTUR3..
```
The flag is `ictf{ZYPH3N_P1Z_F0RG3T_T0RTUR3...}`.
