Tags: reverse_engineering wasm
Rating: 5.0
From the html source, we can know `cs` has the form of `[a-z]{12}`. The key space expanding to ${26}^{12}$ which makes bruteforce impossible.
We fetch the `checker.wasm` and decompile it with some traditional approaches:
```sh
wget https://github.com/WebAssembly/wabt/releases/download/{version}/wabt-{version}-{platform}.tar.gz
tar zxvf wabt-{version}-{platform}.tar.gz
cd wabt-{version}
cp /PATH/TO/checker.wasm .
bin/wasm2c checker.wasm -o checker.c
cp wasm-rt-impl.c wasm-rt-impl.h wasm-rt.h
```
Then you can decompile it using `IDA(Pro)`:
```c
__int64 __fastcall w2c_checker_checker_0(unsigned int *a1, unsigned int a2, unsigned int a3)
{
unsigned int v5; // [rsp+18h] [rbp-118h]
unsigned int v6; // [rsp+1Ch] [rbp-114h]
unsigned int v7; // [rsp+1Ch] [rbp-114h]
unsigned int v8; // [rsp+20h] [rbp-110h]
unsigned int v9; // [rsp+20h] [rbp-110h]
unsigned int v10; // [rsp+24h] [rbp-10Ch]
unsigned int v11; // [rsp+24h] [rbp-10Ch]
unsigned int v12; // [rsp+58h] [rbp-D8h]
unsigned int v13; // [rsp+74h] [rbp-BCh]
unsigned int v14; // [rsp+78h] [rbp-B8h]
unsigned int v15; // [rsp+A0h] [rbp-90h]
char v16; // [rsp+C4h] [rbp-6Ch]
unsigned int v17; // [rsp+C8h] [rbp-68h]
int v18; // [rsp+D0h] [rbp-60h]
unsigned int v19; // [rsp+E4h] [rbp-4Ch]
unsigned int v20; // [rsp+F4h] [rbp-3Ch]
unsigned int v21; // [rsp+118h] [rbp-18h]
unsigned int v22; // [rsp+120h] [rbp-10h]
char v23; // [rsp+12Ch] [rbp-4h]
v22 = *a1 - 32;
*a1 = v22;
i32_store(a1 + 4, v22 + 28LL, a2);
i32_store(a1 + 4, v22 + 24LL, a3);
v21 = i32_load(a1 + 4, v22 + 24LL);
i32_store(a1 + 4, v22 + 20LL, v22);
v20 = v22 - ((4 * v21 + 15) & 0xFFFFFFF0);
*a1 = v20;
i32_store(a1 + 4, v22 + 16LL, v21);
i32_store(a1 + 4, v22 + 12LL, 0LL);
while ( 1 )
{
v19 = i32_load(a1 + 4, v22 + 12LL);
if ( v19 >= (unsigned int)i32_load(a1 + 4, v22 + 24LL) )
break;
v18 = i32_load(a1 + 4, v22 + 28LL);
v17 = i32_load(a1 + 4, v22 + 12LL) + v18;
v16 = i32_load8_u(a1 + 4, v17);
v15 = 4 * i32_load(a1 + 4, v22 + 12LL) + v20;
i32_store(a1 + 4, v15, (unsigned int)(v16 - 97));
v10 = i32_load(a1 + 4, v22 + 12LL) + 1;
i32_store(a1 + 4, v22 + 12LL, v10);
}
v23 = 0;
if ( !(unsigned int)i32_load(a1 + 4, v20 + 4LL) )
{
v23 = 0;
if ( !(unsigned int)i32_load(a1 + 4, v20 + 32LL) )
{
v23 = 0;
if ( !(unsigned int)i32_load(a1 + 4, v20 + 44LL) )
{
v14 = i32_load(a1 + 4, v20);
v13 = i32_load(a1 + 4, v20 + 8LL);
v8 = i32_load(a1 + 4, v20 + 12LL);
v6 = i32_load(a1 + 4, v20 + 16LL);
v23 = 0;
if ( (w2c_checker_f1(a1, v14, v13, v8, v6) & 1) != 0 )
{
v12 = i32_load(a1 + 4, v20 + 20LL);
v11 = i32_load(a1 + 4, v20 + 24LL);
v9 = i32_load(a1 + 4, v20 + 28LL);
v7 = i32_load(a1 + 4, v20 + 36LL);
v5 = i32_load(a1 + 4, v20 + 40LL);
v23 = w2c_checker_f2(a1, v12, v11, v9, v7, v5);
}
}
}
}
i32_load(a1 + 4, v22 + 20LL);
*a1 = v22 + 32;
return v23 & 1;
}
_BOOL8 __fastcall w2c_checker_f1(_DWORD *a1, unsigned int a2, unsigned int a3, unsigned int a4, unsigned int a5)
{
int v9; // [rsp+44h] [rbp-94h]
int v10; // [rsp+4Ch] [rbp-8Ch]
int v11; // [rsp+54h] [rbp-84h]
int v12; // [rsp+7Ch] [rbp-5Ch]
int v13; // [rsp+A4h] [rbp-34h]
unsigned int v14; // [rsp+C8h] [rbp-10h]
bool v15; // [rsp+D4h] [rbp-4h]
v14 = *a1 - 16;
i32_store(a1 + 4, v14 + 12LL, a2);
i32_store(a1 + 4, v14 + 8LL, a3);
i32_store(a1 + 4, v14 + 4LL, a4);
i32_store(a1 + 4, v14, a5);
v15 = 0;
if ( (unsigned int)i32_load(a1 + 4, v14 + 12LL) == 22 )
{
v13 = i32_load(a1 + 4, v14 + 8LL);
v15 = 0;
if ( (unsigned int)i32_load(a1 + 4, v14 + 4LL) + v13 == 30 )
{
v12 = i32_load(a1 + 4, v14 + 4LL);
v15 = 0;
if ( (unsigned int)i32_load(a1 + 4, v14) * v12 == 168 )
{
v11 = i32_load(a1 + 4, v14 + 12LL);
v10 = i32_load(a1 + 4, v14 + 8LL) + v11;
v9 = i32_load(a1 + 4, v14 + 4LL) + v10;
return (unsigned int)i32_load(a1 + 4, v14) + v9 == 66;
}
}
}
return v15;
}
_BOOL8 __fastcall w2c_checker_f2(
_DWORD *a1,
unsigned int a2,
unsigned int a3,
unsigned int a4,
unsigned int a5,
unsigned int a6)
{
int v11; // [rsp+4Ch] [rbp-154h]
int v12; // [rsp+74h] [rbp-12Ch]
int v13; // [rsp+9Ch] [rbp-104h]
int v14; // [rsp+C8h] [rbp-D8h]
int v15; // [rsp+CCh] [rbp-D4h]
int v16; // [rsp+D4h] [rbp-CCh]
int v17; // [rsp+100h] [rbp-A0h]
int v18; // [rsp+104h] [rbp-9Ch]
int v19; // [rsp+10Ch] [rbp-94h]
int v20; // [rsp+134h] [rbp-6Ch]
int v21; // [rsp+13Ch] [rbp-64h]
int v22; // [rsp+144h] [rbp-5Ch]
int v23; // [rsp+14Ch] [rbp-54h]
int v24; // [rsp+174h] [rbp-2Ch]
int v25; // [rsp+17Ch] [rbp-24h]
int v26; // [rsp+184h] [rbp-1Ch]
int v27; // [rsp+18Ch] [rbp-14h]
unsigned int v28; // [rsp+190h] [rbp-10h]
bool v29; // [rsp+19Ch] [rbp-4h]
v28 = *a1 - 32;
i32_store(a1 + 4, v28 + 28LL, a2);
i32_store(a1 + 4, v28 + 24LL, a3);
i32_store(a1 + 4, v28 + 20LL, a4);
i32_store(a1 + 4, v28 + 16LL, a5);
i32_store(a1 + 4, v28 + 12LL, a6);
v27 = i32_load(a1 + 4, v28 + 28LL);
v26 = i32_load(a1 + 4, v28 + 24LL) + v27;
v25 = i32_load(a1 + 4, v28 + 20LL) + v26;
v24 = i32_load(a1 + 4, v28 + 16LL) + v25;
v29 = 0;
if ( (unsigned int)i32_load(a1 + 4, v28 + 12LL) + v24 == 71 )
{
v23 = i32_load(a1 + 4, v28 + 28LL);
v22 = i32_load(a1 + 4, v28 + 24LL) * v23;
v21 = i32_load(a1 + 4, v28 + 20LL) * v22;
v20 = i32_load(a1 + 4, v28 + 16LL) * v21;
v29 = 0;
if ( (unsigned int)i32_load(a1 + 4, v28 + 12LL) * v20 == 449280 )
{
v19 = i32_load(a1 + 4, v28 + 28LL);
v18 = i32_load(a1 + 4, v28 + 28LL) * v19;
v17 = i32_load(a1 + 4, v28 + 24LL);
v29 = 0;
if ( (unsigned int)i32_load(a1 + 4, v28 + 24LL) * v17 + v18 == 724 )
{
v16 = i32_load(a1 + 4, v28 + 20LL);
v15 = i32_load(a1 + 4, v28 + 20LL) * v16;
v14 = i32_load(a1 + 4, v28 + 16LL);
v29 = 0;
if ( (unsigned int)i32_load(a1 + 4, v28 + 16LL) * v14 + v15 == 313 )
{
v13 = i32_load(a1 + 4, v28 + 12LL);
v29 = 0;
if ( (unsigned int)i32_load(a1 + 4, v28 + 12LL) * v13 == 64 )
{
v12 = i32_load(a1 + 4, v28 + 28LL);
v29 = 0;
if ( (unsigned int)i32_load(a1 + 4, v28 + 20LL) + v12 == 30 )
{
v11 = i32_load(a1 + 4, v28 + 28LL);
return v11 - (unsigned int)i32_load(a1 + 4, v28 + 16LL) == 5;
}
}
}
}
}
}
return v29;
}
```
***Or***, if you have `JEB Decompiler`:
```c
int checker(int param0, int param1) {
int* ptr0 = __g0 - 8;
__g0 -= 8;
*(ptr0 + 7) = param0;
*(ptr0 + 6) = param1;
int v0 = *(ptr0 + 6);
*(ptr0 + 5) = ptr0;
int* ptr1 = (int*)((int)ptr0 - ((v0 * 4 + 15) & 0xfffffff0));
__g0 = (int)ptr0 - ((v0 * 4 + 15) & 0xfffffff0);
*(ptr0 + 4) = v0;
*(ptr0 + 3) = 0;
while((unsigned int)*(ptr0 + 3) < (unsigned int)*(ptr0 + 6)) {
*(int*)(*(ptr0 + 3) * 4 + (int)ptr1) = (int)*(char*)(*(ptr0 + 3) + *(ptr0 + 7)) - 97;
++*(ptr0 + 3);
}
int v1 = 0;
if(!*(ptr1 + 1)) {
v1 = 0;
if(!*(ptr1 + 8)) {
v1 = 0;
if(!*(ptr1 + 11)) {
int v2 = __f1(*(ptr1 + 4), *(ptr1 + 3), *(ptr1 + 2), *ptr1);
v1 = 0;
if((v2 & 0x1) != 0) {
v1 = __f2(*(ptr1 + 10), *(ptr1 + 9), *(ptr1 + 7), *(ptr1 + 6), *(ptr1 + 5));
}
}
}
}
__g0 = ptr0 + 8;
return v1 & 0x1;
}
int __f1(int param0, int param1, int param2, int param3) {
int* ptr0 = __g0 - 4;
*(ptr0 + 3) = param0;
*(ptr0 + 2) = param1;
*(ptr0 + 1) = param2;
*ptr0 = param3;
int v0 = 0;
if(*(ptr0 + 3) == 22) {
v0 = 0;
if(*(ptr0 + 1) + *(ptr0 + 2) == 30) {
v0 = 0;
if(*(ptr0 + 1) * *ptr0 == 168) {
v0 = (unsigned int)(*(ptr0 + 1) + *(ptr0 + 2) + (*(ptr0 + 3) + *ptr0) == 66);
}
}
}
return v0 & 0x1;
}
int __f2(int param0, int param1, int param2, int param3, int param4) {
int* ptr0 = __g0 - 8;
*(ptr0 + 7) = param0;
*(ptr0 + 6) = param1;
*(ptr0 + 5) = param2;
*(ptr0 + 4) = param3;
*(ptr0 + 3) = param4;
int v0 = 0;
if(*(ptr0 + 3) + *(ptr0 + 4) + (*(ptr0 + 5) + *(ptr0 + 6)) + *(ptr0 + 7) == 71) {
v0 = 0;
if(*(ptr0 + 3) * *(ptr0 + 4) * (*(ptr0 + 5) * *(ptr0 + 6)) * *(ptr0 + 7) == 0x6db00) {
v0 = 0;
if(*(ptr0 + 6) * *(ptr0 + 6) + *(ptr0 + 7) * *(ptr0 + 7) == 724) {
v0 = 0;
if(*(ptr0 + 4) * *(ptr0 + 4) + *(ptr0 + 5) * *(ptr0 + 5) == 313) {
v0 = 0;
if(*(ptr0 + 3) * *(ptr0 + 3) == 64) {
v0 = 0;
if(*(ptr0 + 5) + *(ptr0 + 7) == 30) {
v0 = (unsigned int)(*(ptr0 + 7) - *(ptr0 + 4) == 5);
}
}
}
}
}
}
return v0 & 0x1;
}
```
which seems more readable.
However, if you compare the two codes, you will noticed that they pass arguments in the opposite order(Similar reports in [a writeup](https://ctftime.org/writeup/36277#:~:text=For%20some%20reason%2C%20in%20ReWasm%2C%20parameters%20appear%20in%20the%20reverse%20order%3A)).
By trying the both, it turned out that `IDA` was correct.
The constrains can then be simplified to this solve script:
```py
from z3 import *
x = [Int(f"x_{i}") for i in range(12)]
c = [i - 97 for i in x]
s = Solver()
s.add(
0 == c[1],
0 == c[8],
0 == c[11],
c[0] == 22,
c[3] + c[2] == 30,
c[3] * c[4] == 168,
c[3] + c[2] + c[0] + c[4] == 66,
c[10] + c[9] + (c[7] + c[6]) + c[5] == 71,
c[10] * c[9] * (c[7] * c[6]) * c[5] == 449280,
c[6] * c[6] + c[5] * c[5] == 724,
c[9] * c[9] + c[7] * c[7] == 313,
c[10] * c[10] == 64,
c[7] + c[5] == 30,
c[5] - c[9] == 5,
)
s.check()
m = s.model()
x = [m[i].as_long() for i in x]
print(bytes(x))
# osu{wasmosumania}
```
