Oooo

Whitehacks 2022 Oooo writeup

cyber
,

1 Solve
We’ve found this alien attached to a password verification device, help us get verified!

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
#!/usr/bin/env python3
ⲟ=str;𝗼ο=int;Ο=ord;ഠ=print;𝗢=Ο('ⲟ')//Ο('о')
𝝾="o" #flOg
o=input()[:O+𝐎]
assert 𝗼.isspace(), "o"
def о(𝝾,ဝ=ⲟ()):
 for ഠ in 𝝾:ဝ+=ⲟ(Ο(ഠ))
 ဝ=o𝝾(ဝ);ο=(ဝ==𝗼)
 while ဝ>(O>>𝐎):𝝾*=𝗢;𝝾+=ဝ%O;ဝ//=𝗢
 return 𝝾-(𝗢-Ο('O')+𝗢+~𝐎+O)*Ο(' ')
def ဝ(о,o=[oο(Ο==𝐎),o𝝾(O==Ο)]):
 for ο in о:o[o𝝾(o==ο)]=(𝗼[o𝝾(о==o)]*𝗢)+(Ο(𝝾)-Ο(' '));o[-𝐎-~O]+=Ο(ο)-Ο(' ')
 return 𝗼
if o𝝾(ဝ(𝗼)[~-𝗢//𝐎]==о("(◕‿◕✿)"))&oο(ဝ(o)[Ο('о')//Ο('ο')]%O==(о(ⲟ(𝐎))==о(ⲟ(O<<𝗢)))):ഠ(f"<TOXT> {ο}");ഠ("( ◕ ‿ ◕ ✿ )")
else:ഠ("G0d effort")

Deobfuscating

yikes. The first thing to do here is to clean it up and deobfuscate it. I first ranblack on it to at least get it to a consistent format. (Not a CTF tool, just a standard formatter) :

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
#!/usr/bin/env python3
ⲟ = str
𝗼ο = int
Ο = ord
ഠ = print
𝗢 = Ο("ⲟ") // Ο("о")
𝝾 = "o"  # flOg
o = input()[: O + 𝐎]
assert 𝗼.isspace(), "o"


def о(𝝾, ဝ=ⲟ()):
    for ഠ in 𝝾:
        ဝ += ⲟ(Ο(ഠ))
    ဝ = o𝝾(ဝ)
    ο = ဝ == 𝗼
    while ဝ > (O >> 𝐎):
        𝝾 *= 𝗢
        𝝾 += ဝ % O
        ဝ //= 𝗢
    return 𝝾 - (𝗢 - Ο("O") + 𝗢 + ~𝐎 + O) * Ο(" ")


def ဝ(о, o=[oο(Ο == 𝐎), o𝝾(O == Ο)]):
    for ο in о:
        o[o𝝾(o == ο)] = (𝗼[o𝝾(о == o)] * 𝗢) + (Ο(𝝾) - Ο(" "))
        o[-𝐎 - ~O] += Ο(ο) - Ο(" ")
    return 𝗼


if o𝝾(ဝ(𝗼)[~-𝗢 // 𝐎] == о("(◕‿◕✿)")) & oο(
    ဝ(o)[Ο("о") // Ο("ο")] % O == (о(ⲟ(𝐎)) == о(ⲟ(O << 𝗢)))
):
    ഠ(f"<TOXT> {ο}")
    ഠ("( ◕ ‿ ◕ ✿ )")
else:
    ഠ("G0d effort")

Already looking much better. We see a bunch of constant declarations. Let’s do a first pass of renaming symbols (F2 in vsc). ord("ⲟ") // ord("о") is evaluated to 10. 

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
#!/usr/bin/env python3
flag = "o"  # flOg
inp = input()[: 10 + 10]
assert inp.isspace(), "o"


def о(𝝾, ဝ=str()):
    for ഠ in 𝝾:
        ဝ += str(ord(ഠ))
    ဝ = int(ဝ)
    ο = ဝ == inp
    while ဝ > (10 >> 10):
        𝝾 *= 10
        𝝾 += ဝ % 10
        ဝ //= 10
    return 𝝾 - (10 - ord("O") + 10 + ~10 + 10) * ord(" ")


def ဝ(о, o=[int(ord == 10), int(10 == ord)]):
    for ο in о:
        o[int(o == ο)] = (𝗼[int(о == o)] * 10) + (ord(𝝾) - ord(" "))
        o[-10 - ~10] += ord(ο) - ord(" ")
    return 𝗼


if int(ဝ(inp)[~-10 // 10] == о("(◕‿◕✿)")) & int(
    ဝ(inp)[ord("о") // ord("ο")] % 10 == (о(str(10)) == о(str(10 << 10)))
):
    print(f"<TOXT> {flag}")
    print("( ◕ ‿ ◕ ✿ )")
else:
    print("G0d effort")

We’re getting there. Now, let’s do a second pass, renaming everything to a generic readable name like arg1, func1 and so on. 

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
#!/usr/bin/env python3
flag = "o"  # flOg
inp = input()[: 10 + 10]
assert inp.isspace(), "o"


def func1(arg1, arg2=str()):
    for x1 in arg1:
        arg2 += str(ord(x1))
    arg2 = int(arg2)
    arg1 = arg2 == inp
    while arg2 > (10 >> 10):
        arg1 *= 10
        arg1 += arg2 % 10
        arg2 //= 10
    return arg1 - (10 - ord("O") + 10 + ~10 + 10) * ord(" ")


def func2(arg1, arg2=[int(ord == 10), int(10 == ord)]):
    for x1 in arg1:
        arg2[int(arg2 == x1)] = (arg2[int(arg1 == arg2)] * 10) + (ord(x1) - ord(" "))
        arg2[-10 - ~10] += ord(x1) - ord(" ")
    return arg2


if int(func2(inp)[~-10 // 10] == func1("(◕‿◕✿)")) & int(
    func2(inp)[ord("о") // ord("ο")] % 10 == (func1(str(10)) == func1(str(10 << 10)))
):
    print(f"<TOXT> {flag}")
    print("( ◕ ‿ ◕ ✿ )")
else:
    print("G0d effort")

Now, let’s evaluate some constants. There are the obvious ones, like inp = input()[: 10 + 10], and some not so obvious ones, like int(arg2 == x1). Despite it being an expression, we can observe that arg2 and x1 are very different, and hence unlikely to be equal. We can replace this with a int(False), turning into 0.

This is the first accident prone stage of the deobfuscation. You might make a wrong assumption, or evaluate the constants wrong. Take your time, try to understand roughly what the code is doing first.

One interesting thing we see is that all calls to func1 are on constants. This means that we don’t even need to understand func1! We can just execute each call and replace it with its value.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
>>> def func1(arg1, arg2=str()):
    for x1 in arg1:
        arg2 += str(ord(x1))
    arg2 = int(arg2)
    arg1 = arg2 == inp
    while arg2 > (10 >> 10):
        arg1 *= 10
        arg1 += arg2 % 10
        arg2 //= 10
    return arg1 - (10 - ord("O") + 10 + ~10 + 10) * ord(" ")

>>> func1("(◕‿◕✿)")
Traceback (most recent call last):
  File "<pyshell#2>", line 1, in <module>
    func1("(◕‿◕✿)")
  File "<pyshell#1>", line 5, in func1
    arg1 = arg2 == inp
NameError: name 'inp' is not defined

Ah. func1 depends on inp. No bother, inp seems to be a 20 (max) character string, which arg2 is clearly not equal to. Let’s replace it with False, or equivalently, 0.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
>>> def func1(arg1, arg2=str()):
    for x1 in arg1:
        arg2 += str(ord(x1))
    arg2 = int(arg2)
    arg1 = 0
    while arg2 > (10 >> 10):
        arg1 *= 10
        arg1 += arg2 % 10
        arg2 //= 10
    return arg1 - (10 - ord("O") + 10 + ~10 + 10) * ord(" ")

>>> func1("(◕‿◕✿)")
147400158695528588824
>>> func1(str(10)) == func1(str(10 << 10))
False

With those constants done, let’s plug them in and get rid of func1. Let’s also evaluate other trivial constants while we’re at it. 

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
#!/usr/bin/env python3
flag = "o"  # flOg
inp = input()[:20]
assert inp.isspace(), "o"


def func2(arg1, arg2=[0, 0]):
    for x1 in arg1:
        arg2[0] = (arg2[0] * 10) + (ord(x1) - 32)
        arg2[1] += ord(x1) - 32
    return arg2


if int(func2(inp)[0] == 147400158695528588824) & int(func2(inp)[1] % 10 == False):
    print(f"<TOXT> {flag}")
    print("( ◕ ‿ ◕ ✿ )")
else:
    print("G0d effort")

We can rewrite that last condition:

1
2
if  func2(inp)[0]      == 147400158695528588824 and 
    func2(inp)[1] % 10 == 0

Now at this point, it should be pretty clear what we need to do. We’re asked for (a maximum of) 20 characters, all of which must be isspace. We pass that into func2, and need the first output to be a specific value, while the second value should be divisible by 10. (kinda. see this section for more info)

z3 mini tutorial

Now, we could try to find a solution by hand, but that’s silly. We’ll use z3! The gist of z3 is:

  1. Define variables

    1
    2
    3
    4
    from z3 import * 

    x = Int("x")    # an Int variable with name "x"
    y = Int("y")    # an Int variable with name "y"

  2. Define equalities

    1
    2
    3
    4
    5
    6
    s = Solver()    # define a solver object
    s.add(          # add conditions to it
        x**2 + y**2 == 25,
        0 < x,
        x < y
    )

  3. Hope z3 finds a solution

    1
    2
    3
    4
    5
    s.check()       # check for a solution. returns sat(isfied) or unsat
    m = s.model()   # raises error if check couldn't find a solution

    print(f"{m[x] = }, {m[y] = }") 
    # m[x] = 3, m[y] = 4

Finding a solution

The first thing to deal with is the isspace() assertation. Searching on stackoverflow:

1
2
3
4
unicode_whitespace = (
    "\t\x0b\x0c\r\x1c\x1d\x1e\x1f \x85\xa0\u1680\u2000\u2001\u2002\u2003\u2004\u2005\u2006"
    "\u2007\u2008\u2009\u200a\u2028\u2029\u202f\u205f\u3000"
)

A newline is a whitespace, but since that terminates the output I’ve removed it. These are the remaining characters we’ll have to work with. z3 doesn’t have a function to describe the condition val in set, so instead we can just say Or(val == i for i in set). We’ll apply this condition to each of the 20 characters.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
from z3 import *

chars = [Int(i) for i in range(20)]
s = Solver()

whitespace = (
    "\t\x0b\x0c\r\x1c\x1d\x1e\x1f \x85\xa0\u1680\u2000\u2001\u2002\u2003\u2004\u2005\u2006"
    "\u2007\u2008\u2009\u200a\u2028\u2029\u202f\u205f\u3000"
)

for char in chars:
    s.add(Or([char == ord(c) for c in whitespace]))

s.check()
m = s.model()
print(m)
# k!0 = 9,
# k!1 = 9,
# k!2 = 9,
# ...

With the script as it, it only forces the solved values to be a whitespace character. Hence when we check for a solution, it’s just a trivial solution of all 9s (tabs).

Now let’s add the actual function and equalities. Recall

1
2
3
4
5
6
7
8
def func2(arg1, arg2=[0, 0]):
    for x1 in arg1:
        arg2[0] = (arg2[0] * 10) + (ord(x1) - 32)
        arg2[1] += ord(x1) - 32
    return arg2

if  func2(inp)[0]      == 147400158695528588824 and 
    func2(inp)[1] % 10 == 0

At first, arg2[0] is 0. Each iteration, its value is multiplied by 10 and (ord(x1) - 32) is added to it. Observe that it’s just a polynomial in 10. Now we could write the expression by hand. But since there’s no branching, we can just pass in the list of z3 Ints and get out the exact expression, the lazy :tm: way. 

1
2
3
4
5
6
7
8
9
10
11
12
13
14
def z3_func2(arg1, arg2=[0, 0]):
    for x1 in arg1:
        arg2[0] = (arg2[0] * 10) + (x1 - 32)
        arg2[1] += x1 - 32
    return arg2

z3_func2(chars)
'''
[((((((((((... + ...)*10 + k!10 - 32)*10 + k!11 - 32)*10 +
       k!12 - 32)*
      10 +
      k!13 - 32)*
      ...
'''

sheesh. Put it all together:

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
from z3 import *

chars = [Int(i) for i in range(20)]
s = Solver()

whitespace = (
    "\t\x0b\x0c\r\x1c\x1d\x1e\x1f \x85\xa0\u1680\u2000\u2001\u2002\u2003\u2004\u2005\u2006"
    "\u2007\u2008\u2009\u200a\u2028\u2029\u202f\u205f\u3000"
)

for char in chars:
    s.add(Or([char == ord(c) for c in whitespace]))


def z3_func2(arg1, arg2=[0, 0]):
    for x1 in arg1:
        arg2[0] = (arg2[0] * 10) + (x1 - 32)
        arg2[1] += x1 - 32
    return arg2

s.add(
    z3_func2(chars)[0] == 147400158695528588824,
    z3_func2(chars)[1] % 10 == 0
)

s.check()
m = s.model()
print(m)
#[k!0 = 32,   
# k!1 = 160,  
# k!2 = 133,

Looks promising. Let’s join the string back together and pass it into the original script!

1
2
3
string = "".join(chr(m[chars[i]].as_long()) for i in range(20))
print(repr(string))
#' \xa0\x85\x0b\u2002\u3000\u3000 \r\x0c\x0b\u2007\t\x0b\x0b\u2002\x0b \u2006\u2004'
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
#!/usr/bin/env python3
ⲟ=str;𝗼ο=int;Ο=ord;ഠ=print;𝗢=Ο('ⲟ')//Ο('о')
𝝾="flOg" #flOg

o=' \xa0\x85\x0b\u2002\u3000\u3000 \r\x0c\x0b\u2007\t\x0b\x0b\u2002\x0b \u2006\u2004'

assert 𝗼.isspace(), "o"
def о(𝝾,ဝ=ⲟ()):
 for ഠ in 𝝾:ဝ+=ⲟ(Ο(ഠ))
 ဝ=o𝝾(ဝ);ο=(ဝ==𝗼)
 while ဝ>(O>>𝐎):𝝾*=𝗢;𝝾+=ဝ%O;ဝ//=𝗢
 return 𝝾-(𝗢-Ο('O')+𝗢+~𝐎+O)*Ο(' ')
def ဝ(о,o=[oο(Ο==𝐎),o𝝾(O==Ο)]):
 for ο in о:o[o𝝾(o==ο)]=(𝗼[o𝝾(о==o)]*𝗢)+(Ο(𝝾)-Ο(' '));o[-𝐎-~O]+=Ο(ο)-Ο(' ')
 return 𝗼
if o𝝾(ဝ(𝗼)[~-𝗢//𝐎]==о("(◕‿◕✿)"))&oο(ဝ(o)[Ο('о')//Ο('ο')]%O==(о(ⲟ(𝐎))==о(ⲟ(O<<𝗢)))):ഠ(f"<TOXT> {ο}");ഠ("( ◕ ‿ ◕ ✿ )")
else:ഠ("G0d effort")

# <TOXT> flOg
# ( ◕ ‿ ◕ ✿ )

Great success. Piping this into the challenge server:

1
2
3
4
5
python -c "print(' \xa0\x85\x0b\u2002\u3000\u3000 \r\x0c\x0b\u2007\t\x0b\x0b\u2002\x0b \u2006\u2004')" |\
nc challenges1.whitehacks.xyz 35566

# W0Ws, yo Gots FLOG WH2022{000o0OO0o0OoO0O0o0o000}
# ( ◕ ‿ ◕ ✿ )

( ◕ ‿ ◕ ✿ )

Bound default argument

This section discusses some potential pitfalls related to the most interesting (imo) part of the challenge: the bound default argument arg2 = [0, 0].

We’re lucky that func2 had no branching. If it did, we would have to write the z3 expression by hand, perhaps needing to know how the polynomial and sum worked.

Another benefit of using the function is that we didn’t need to deal with the bound argument default. Observe:

1
2
3
4
5
6
def func(arg = [0]):
    arg[0] += 1
    return arg
print(func()) # [1]
print(func()) # [2]
print(func()) # [3]

The list is actually the same across calls! This could have been a real roadblock if we didn’t know about it and had to write the z3 expression by hand. Since we used z3_func2, this quirk was built into the z3 expression for us.

Let’s look at some subtle differences and how they change the result:

Wrong order z3

Had the z3 expressions been in a different order:

1
2
3
4
s.add(
    z3_func2(chars)[1] % 10 == 0,
    z3_func2(chars)[0] == 147400158695528588824
)

we end up with no solution. Remember that arg2[0] is a polynomial. Thus, by reusing arg2, we’ve doubled the degree of the final polynomial, making the resulting values much bigger than the original, hence no solution can be found.

Reused value

Had the function call been reused, under the assumption that the second call is identical:

1
2
3
4
5
6
7
res = z3_func2(chars)
s.add(
    res[0] == 147400158695528588824,
    res[1] % 10 == 0
)
...
# '\x1c\x85\r\u2006\u1680\u200a\u2028\u3000\u2028\u2002\xa0\u2008\u3000\u2001\r\xa0\u2029\x1d\x1c\u2004'

We would have gotten a correct, but different solution. How? On the second z3_func2 call, arg2 is reused, causing the addition loop to happen twice, hence causing arg2[1] to be double of what it’s value was from the first call. Now if we only called it once, z3 would solve arg2[1] to some value, say 10. When the string is run in the real script, the value of arg2[1] would come out as20. But it’s still %10 == 0, so it also passed!