# Dice Is You [RE]

A wasm reversing challenge using closure compiler to simplify code, and z3 to solve for final solution.

# Challenge Description

``````DICE IS YOU

Controls:
- wasd/arrows: movement
- space: advance a tick without moving
- q: quit to main menu
- r: restart current level
- z: undo a move (only works for past 256 moves and super buggy)

Play: dice-is-you.dicec.tf
``````

# Solution

## Level 1-4

This challenge was quite well made as you get to play through a game before the real challenge comes. The first four levels were all quite trivial after you understand the game mechanics through some trial and error.

It’s not really required for you to play through but I found that it helped me understand the game’s lifecycle a bit, I’ll save you the hassle though: Change the value of the cookie to 5 to unlock level 5.

## Level 5

This level is basically unsolvable by just playing the game, so let’s finally do some RE.

Opening the network tab in the developer’s tools, we can copy the url (https://dice-is-you.dicec.tf/app.wasm) to the wasm binary and download that.

You can get the wasm file here

Then, we can use a wasm decompiler to decompile the binary to, what is known as, dcmp (which is syntactically very similar to JavaScript).

``````wasm-decompile app.wasm -o app.js
cat app.js | grep function | grep -v "emscripten" | grep -v "SDL" > functions.txt
``````

Since decompiled code is usually very big, it’s also useful to extract the lines which contain function names, just to find out the more important functions easier.

Looking inside the txt file, notice some important functions:

``````function level1() {
function level2() {
function level3() {
function level4() {
function level_flag_fin() {
function flag_rules(a:int, b:int) {
...
function check_code(a:int, b:int, c:int, d:int):int {
function get_code_value(a:int):int {
function code(a:int, b:int, c:int, d:int, e:int):int {
function reset(a:int) {
function check_rule(a:int, b:int, c:int, d:int, e:int, f:int, g:int, h:int):int {
function check_win_condition(a:int, b:int, c:int):int {
``````

The function names were pretty self explanatory – at least that’s what I hoped for, since the code was basically unreadable. So we have the functions for the respective levels, and the last level is called `level_flag_fin`, which implies that the flag will be given after we solve it (?)

### What are the blocks?

Looking at the function,

``````function level_flag_fin() {
...
var j:int = 198;
var k:int = 324;
var l:int = 330;
var m:int = 2;
var n:int = 8;
var o:int = -2;
var p:int = 7;
var q:int = 6;
var r:int = 342;
spawn_entity(m, m, r);
spawn_entity(d, d, o);
spawn_entity(m, d, o);
spawn_entity(e, d, o);
spawn_entity(h, d, o);
spawn_entity(f, d, o);
spawn_entity(q, d, o);
spawn_entity(p, d, o);
...
}
``````

It seems like this level functions spawns the blocks (entities), we can tidy the code using a closure compiler after cleaning it into proper JavaScript, which wasn’t really hard to do.

``````function level_flag_fin() {
var a = g_a - 16;
a < g_c && handle_stack_overflow();
g_a = a;
spawn_entity(2, 2, 342);
spawn_entity(1, 1, -2);
spawn_entity(2, 1, -2);
...
spawn_entity(3, 4, 264);
spawn_entity(3, 5, 138);
for (c = 1; c <= 12; c++) {
spawn_entity(c, 13, -2);
spawn_entity(c, 17, -2);
if (c <= 8) spawn_entity(c, 15, -2);
if (c <= 5) spawn_entity(c, 19, -2);
}
spawn_entity(1, 14, -2);
spawn_entity(1, 16, -2);
spawn_entity(1, 18, -2);
spawn_entity(8, 14, -2);
...
a = c + 16;
a < g_c && handle_stack_overflow();
g_a = a;
}
``````

Much more readable! After staring at this for probably half an hour, a reasonable hypothesis I made was that `spawn_entity` takes in `x_coords`, `y_coords`, `entity_id` as its arguments. So, I added some comments to identify which lines corresponded to what block.

``````  ...
spawn_entity(3, 3, 330); // y
spawn_entity(4, 3, 324); // x
spawn_entity(5, 3, 198); // o+
spawn_entity(3, 4, 264); // E
spawn_entity(3, 5, 138); // ∆
...
spawn_entity(16, 3, 240); //O.
spawn_entity(18, 3, 252); //D
spawn_entity(10, 3, 294); //I
spawn_entity(12, 3, 276); //|_
spawn_entity(14, 3, 288); //L mirror
spawn_entity(16, 5, 300); //∆filled
spawn_entity(18, 5, 312); //J
spawn_entity(10, 5, 306); //K
spawn_entity(12, 5, 318); //F
spawn_entity(14, 5, 348); //G
spawn_entity(16, 7, 336); //N
spawn_entity(18, 7, 150); //square half fill
spawn_entity(10, 7, 162); //Z
spawn_entity(12, 7, 174); //+
spawn_entity(14, 7, 186); //square
spawn_entity(16, 9, 258); // /
spawn_entity(18, 9, 210); // o-
spawn_entity(10, 9, 222); // R mirror
spawn_entity(12, 9, 234); // T
spawn_entity(14, 9, 246); // π
...
``````

### How do you win?

After poking around for a really long time, I figured `check_win_condition` wasn’t really the function that I should be looking at, instead there was this mysterious function above it called `code` which takes in 5 arguments…

Same as the number of blocks in a row/column of the grid. Coincidence? I think not

Doing the same thing: clean up, closure compile…

``````function code(b, c, d, e, f) {
var a = g_a - 16;
a = b;
a = c;
a = d;
a = e;
a = f;
return 42 * (a & 255) + 1337 * (a & 255) + (a & 255) + (a & 255 ^ a & 255) + ((a & 255) << 1) & 255;
}
``````

This looks promising! So I searched what function called it, and found myself in `check_code` (oddly enough, this function was never actually called anywhere else). Here’s the simplified code:

``````function check_code(c, g, h, k) {
...
c = get_code_value(a);
a = c;
c = get_code_value(a);
a = c;
c = get_code_value(a);
a = c;
c = get_code_value(a);
a = c;
c = get_code_value(a);
a = c;
...
b = code(a & 255, a & 255, a & 255, a & 255, a & 255);
a = b;
if (!(a & 255)) {
// returns 1
return ..., a = 1, b = a, b &= 1, ..., b;
}
a = 0;
b = a;
b &= 1;
...
// returns 0
return b;
}
``````

Intuitively, we expect `check_code` to return 1. The result of `code` is masked with 255, so `code` must return 0 in order to satisfy the if-statement. We can test this out using the example in the level (the one that is highlighted)

Firing up python, we can verify that our concept is corr…

``````>>> 42*(210&255)+1337*(174&255)+(324&255)+((324&255)^(330&255))+((198&255)<<1)&255
16
``````

Wait, what? Maybe I got it revers…

``````>>> 42*(198&255)+1337*(330&255)+(324&255)+((324&255)^(174&255))+((210&255)<<1)&255
200
``````

So… It seems like `code` doesn’t take in `entity_id`s to compute the result. But luckily I noticed that what’s being passed is the result of `get_code_value`, and its argument is hopefully the `entity_id`.

In summary, `get_code_value` takes in an argument, minus 138 from it, then puts it through a switch statement (210 cases O.o). Each case will return a different value, so I plugged in the `entity_id`s and gathered their respective “code_value”.

``````y, 212
x, 194
o+, 189
E, 48
∆, 192
O., 18
D, 25
I, 120
|_, 55
L mirror, 1
∆filled, 61
J, 135
K, 138
F, 49
G, 96
N, 148
square half fill, 119
Z, 247
+, 160
square, 179
/, 163
o-, 171
R mirror, 5
T, 183
π, 150
``````

Am I finally on the right track? Well…

``````>>> 42*(171&255)+1337*(160&255)+(194&255)+((194&255)^(212&255))+((189&255)<<1)&255
0
``````

YES! So what’s left to do is to write a z3 solver to solve for the correct configuration, then push the blocks accordingly and get the flag!

# Final Script

``````from z3 import *
s = Solver()
ans = [BitVec(str(i), 9) for i in range(25)]
cond = "42*(ans[%s]&255)+1337*(ans[%s]&255)+(ans[%s]&255)+(ans[%s]&255^ans[%s]&255)+((ans[%s]&255)<<1)&255 == 0"

values = [212, 194, 189, 48, 192, 18, 25, 120, 55, 1, 61, 135, 138, 49, 96, 148, 119, 247, 160, 179, 163, 171, 5, 183, 150]

for i in range(len(ans)):
scond = "ans[%d] == %d" % (i, values)
for j in values[1:]:
scond = "Or(%s, ans[%d] == %d)" % (scond, i, j)

for i in range(5):
# row
x = 5*i
# col

for i in range(24):
for j in range(i+1, 25):
s.add(eval("ans[%s] != ans[%s]" % (str(i), str(j))))

values.sort()
while s.check() == sat:
model = s.model()
result = str(s.model())
result = list(map(lambda x: int((x.split(' = ')).replace(']', '')), ''.join(result.split("\n")).split(',')))
result.sort()
ok = True
for i in range(len(result)):
if values[i] != result[i]:
ok = False
break
if ok:
print(model)
break
``````

There’s definitely a better way to script this but oh well ¯\_(ツ)_/¯