# Oooo

#### Whitehacks 2022 Oooo writeup

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

## 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) :

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.

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

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.

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.

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.

We can rewrite that last condition:

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

2. Define equalities

3. Hope z3 finds a solution

## Finding a solution

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

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.

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

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.

sheesh. Put it all together:

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

Great success. Piping this into the challenge server:

( ◕ ‿ ◕ ✿ )

## 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:

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:

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:

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!