# Oooo

#### Whitehacks 2022 Oooo writeup

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

1 | #!/usr/bin/env python3 |

## Deobfuscating

yikes. The first thing to do here is to clean it up and deobfuscate it. I first ran`black`

on it to at least get it to a consistent format. (Not a CTF tool, just a standard formatter) :

1 | #!/usr/bin/env python3 |

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 | #!/usr/bin/env python3 |

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 | #!/usr/bin/env python3 |

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 | def func1(arg1, arg2=str()): |

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 | def func1(arg1, arg2=str()): |

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 | #!/usr/bin/env python3 |

We can rewrite that last condition:

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

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:

Define variables

1

2

3

4from z3 import *

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

y = Int("y") # an Int variable with name "y"Define equalities

1

2

3

4

5

6s = Solver() # define a solver object

s.add( # add conditions to it

x**2 + y**2 == 25,

0 < x,

x < y

)Hope z3 finds a solution

1

2

3

4

5s.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 | unicode_whitespace = ( |

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

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 | def func2(arg1, arg2=[0, 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 | def z3_func2(arg1, arg2=[0, 0]): |

sheesh. Put it all together:

1 | from z3 import * |

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

1 | string = "".join(chr(m[chars[i]].as_long()) for i in range(20)) |

1 | #!/usr/bin/env python3 |

Great success. Piping this into the challenge server:

1 | python -c "print(' \xa0\x85\x0b\u2002\u3000\u3000 \r\x0c\x0b\u2007\t\x0b\x0b\u2002\x0b \u2006\u2004')" |\ |

( ◕ ‿ ◕ ✿ )

## 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 | def func(arg = [0]): |

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 | s.add( |

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 | res = z3_func2(chars) |

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 as`20`

. But it’s still `%10 == 0`

, so it also passed!