# free_play (HackTM Quals 2023)
We're given a web application that expects us to input a 256-character flag, then encrypts it with AES128-CBC with fixed key and IV and passes the result into `checkFlag` function implemented in wasm.
## WASM disassembly
The initial thought is to pass wasm to `wasm-decompile`. Unfortunately, that idea immediately fails miserably:
```
$ wasm-decompile --enable-all main.wasm
wasm-decompile: ./src/decompiler.cc:688: std::string wabt::Decompiler::InitExp(const ExprList&): Assertion `!el.empty()' failed.
Aborted
```
All the other tools (rewasm, JEB, ghidra-wasm-plugin) also fail to process that wasm for some reason, so we might need to go the hard way.
First of all, let's generate textual representation of the wasm with `wasm2wat` and open it with text editor.
Quick inspection shows that `checkFlag` is function 47, it calls functions 45 and 46, and function 45 in turn calls functions 41 through 44. Then we can safely remove everything else (including the imported functions), renumber relevant functions as 1-7 (by dropping 4) and fix all respective calls. We also should add a dummy function 0.
After that we can convert it back to wasm with `wat2wasm`.
Now at least `ghidra-wasm-plugin` can understand and load it!
## Analysis
Let's take a look at the `checkFlag` function:
```clike=
uint export::checkFlag(int param1)
{
uint uVar1;
uint local_628;
uint local_624;
ulonglong local_620;
ushort local_612;
ulonglong local_610 [65];
undefined local_408 [1028];
int local_4;
memory_fill(0,0x400,0,local_408);
memory_fill(0,0x200,0,local_610);
memory_copy(0,0,0x200,0x10110,local_610);
for (local_612 = 0; local_612 < 0x100; local_612 += 1) {
*(byte *)(param1 + (uint)local_612) = *(byte *)(param1 + (uint)local_612) ^ *(byte *)(local_612 + 0x10010);
}
local_620 = 0;
for (local_624 = 0; local_624 < 0x40; local_624 += 1) {
for (local_628 = 0; local_628 < 0x40; local_628 += 1) {
if ((*(ulonglong *)(local_624 * 8 + 0x10310) >> ((ulonglong)(0x3f - local_628) & 0x3f) & 1) != 0) {
local_610[local_624] =
local_610[local_624] |
(longlong)
(int)((int)(uint)*(byte *)(param1 + (int)(local_620 >> 3)) >> (7 - ((uint)local_620 & 7) & 0x1f) & 1) <<
((ulonglong)(0x3f - local_628) & 0x3f);
local_620 += 1;
}
}
}
local_4 = param1;
unnamed_function_6(local_610,local_408);
uVar1 = unnamed_function_5(local_408);
return uVar1 & 1;
}
```
It already looks somewhat readable, but let's clean it up a bit first. From js we know it should return `bool` and takes `byte *` as argument. Also some variable names can be inferred.
```clike=
bool export::checkFlag(byte *enc_flag)
{
undefined4 uVar1;
uint j;
uint i;
ulonglong k;
ushort t;
ulonglong data1 [64];
ulonglong data2 [128];
memory_fill(0,0x400,0,data2);
memory_fill(0,0x200,0,data1);
memory_copy(0,0,0x200,0x10110,data1);
for (t = 0; t < 0x100; t += 1) {
enc_flag[t] = enc_flag[t] ^ BYTE_ARRAY_ram_00010010[t];
}
k = 0;
for (i = 0; i < 0x40; i += 1) {
for (j = 0; j < 0x40; j += 1) {
if ((ULONGLONG_ARRAY_ram_00010310[i] >> ((ulonglong)(0x3f - j) & 0x3f) & 1) != 0) {
data1[i] = data1[i] |
(longlong)(int)((int)(uint)enc_flag[(int)(k >> 3)] >> (7 - ((uint)k & 7) & 0x1f) & 1) <<
((ulonglong)(0x3f - j) & 0x3f);
k += 1;
}
}
}
unnamed_function_6(data1,data2);
uVar1 = unnamed_function_5(data2);
return (bool)((byte)uVar1 & 1);
}
```
First, two arrays of `int64` are initialized with zeroes, then one of them is filled with static data at `0x10110`. Then the encrypted flag is xored with static array at `0x10010`, and array of bitmasks at `0x10310` is used to OR flag bits with static data from `0x10110`. After that, the result is somehow transformed with `unnamed_function_6` (originally 46), and transformation result is then passed to `unnamed_function_5` (originally 45) to check for match.
Let's look at `unnamed_function_6`. We know the argument types it expects, so can retype those and name variables immediately for better readability:
```clike=
void unnamed_function_6(ulonglong *input,ulonglong *output)
{
byte j;
byte local_a;
byte i;
memory_copy(0,0,0x200,input,output);
for (i = 0; i < 0x40; i += 1) {
for (j = 0; j < 0x40; j += 1) {
output[i + 0x40] = output[i + 0x40] << 1;
output[i + 0x40] = output[i + 0x40] | input[j] >> ((ulonglong)(byte)(0x3f - i) & 0x3f) & 1;
}
}
return;
}
```
We can see it just copies input to the lower half of the output, and then fills the upper half with transposed input bits.
Now, let's look at the `unnamed_function_5`:
```clike=
bool unnamed_function_5(ulonglong *param1)
{
bool bVar1;
bool bVar2;
bVar1 = unnamed_function_1(param1);
bVar2 = false;
if (bVar1) {
bVar1 = unnamed_function_1(param1 + 0x40);
bVar2 = false;
if (bVar1) {
bVar1 = unnamed_function_2(param1);
bVar2 = false;
if (bVar1) {
bVar1 = unnamed_function_2(param1 + 0x40);
bVar2 = false;
if (bVar1) {
bVar1 = unnamed_function_4(param1);
bVar2 = false;
if (bVar1) {
bVar1 = unnamed_function_4(param1 + 0x40);
bVar2 = false;
if (bVar1) {
bVar1 = unnamed_function_3(param1);
bVar2 = false;
if (bVar1) {
bVar2 = unnamed_function_3(param1 + 0x40);
}
}
}
}
}
}
}
return bVar2;
}
```
We can see it runs four check on each half of the input, and all of them should be `true` for the final result to be `true`.
### unnamed_function_1 (originally 41)
```clike=
bool unnamed_function_1(ulonglong *param1)
{
undefined auVar1 [16];
undefined local_350 [16];
undefined local_340 [16];
undefined local_330 [16];
undefined local_320 [16];
undefined local_310 [16];
undefined local_300 [16];
undefined local_2f0 [16];
undefined local_2e0 [16];
char local_2d0;
undefined local_2c0 [16];
undefined local_2b0 [16];
undefined local_2a0 [16];
undefined local_290 [16];
undefined local_280 [16];
undefined local_270 [16];
undefined local_260 [31];
byte local_241;
byte i;
byte local_215;
i = 0;
while( true ) {
if (7 < i) {
return true;
}
auVar1 = i8x16_popcnt(*(undefined (*) [16])(param1 + i));
local_2d0 = SUB161(auVar1,0);
if ((char)(local_2d0 + *(char *)((uint)local_2c0 | 1) + *(char *)((uint)local_2b0 | 2) +
*(char *)((uint)local_2a0 | 3) + *(char *)((uint)local_290 | 4) + *(char *)((uint)local_280 | 5) +
*(char *)((uint)local_270 | 6) + *(char *)((uint)local_260 | 7)) != 32) break;
if ((char)(*(char *)((uint)local_350 | 8) + *(char *)((uint)local_340 | 9) + *(char *)((uint)local_330 | 10) +
*(char *)((uint)local_320 | 0xb) + *(char *)((uint)local_310 | 0xc) + *(char *)((uint)local_300 | 0xd) +
*(char *)((uint)local_2f0 | 0xe) + *(char *)((uint)local_2e0 | 0xf)) != 32) {
return false;
}
i += 2;
}
return false;
}
```
Here, the decompiler didn't do a particularly good job. We can see each `int128` word is loaded from the input array, then `i8x16_popcnt` is called to count `1` bits in each byte, and then some unclear checks are performed on the result twice, each of which should result in 32.
Analyzing the `wat` shows it actually sums bit counts in bytes 0-7 and 8-15, but we'll omit that tedious part here :)
So, wrapping it up, sums of set bits in each `int64` shoud equal 32 for the check to pass.
### unnamed_function_2 (originally 42)
```clike=
bool unnamed_function_2(ulonglong *param1)
{
int iVar1;
undefined auVar2 [16];
byte j;
byte i;
byte local_39;
i = 0;
do {
if (7 < i) {
return true;
}
for (j = i + 1; j < 7; j += 2) {
auVar2 = i64x2_eq(*(undefined (*) [16])(param1 + j),*(undefined (*) [16])(param1 + i));
iVar1 = v128_any_true(auVar2);
if (iVar1 != 0) {
return false;
}
}
i += 2;
} while( true );
}
```
Here the result is much better. We can see it requires all array elements to be different.
### unnamed_function_3 (originally 43)
```clike=
bool unnamed_function_3(ulonglong *param1)
{
int iVar1;
undefined x [16];
undefined t [16];
byte i;
byte local_95;
i = 0;
while( true ) {
if (7 < i) {
return true;
}
x = *(undefined (*) [16])(param1 + i);
t = i64x2_shr_u(1,x);
t = v128_and(t,x);
x = i64x2_shr_u(2,x);
x = v128_and(x,t);
iVar1 = v128_any_true(x);
if (iVar1 != 0) break;
i += 2;
}
return false;
}
```
Here we can see it uses `i64x2_shr_u` to right shift each 64-bit part of `int128` and ANDs those together, and cheks if any of those are non-zero. Basically, for each element `x` of input, `x & (x >> 1) & (x >> 2)` should be zero for the function to succeed.
### unnamed_function_4 (originally 44)
```clike=
bool unnamed_function_4(ulonglong *param1)
{
int iVar1;
undefined x [16];
undefined t [16];
byte i;
byte local_a5;
i = 0;
while( true ) {
if (7 < i) {
return true;
}
x = v128_not(*(undefined (*) [16])(param1 + i));
t = i64x2_shr_u(1,x);
t = v128_and(t,x);
x = i64x2_shr_u(2,x);
x = v128_and(x,t);
iVar1 = v128_any_true(x);
if (iVar1 != 0) break;
i += 2;
}
return false;
}
```
This one is extremely similar to the previous one, but inverted values are shifted and checked instead. So, `~x & (~x >> 1) & (~x >> 2)` should be zeroes.
## Solving
Now we have all the pieces, so it's time to wrap it all together.
```python=
from array import array
from Crypto.Cipher import AES
from z3 import *
IV = bytes([81, 62, 98, 66, 69, 240, 205, 237, 65, 41, 101, 220, 140, 39, 27, 180])
KEY = bytes([202, 102, 28, 101, 4, 34, 8, 203, 208, 209, 107, 44, 182, 218, 153, 203])
# raw data from wasm disassembly
data = b"\xf0n\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80z\x88(]\xe7$p6\xd0j\xba\xab-\x1d\xd5\x86U2\xf9S\xa8\xf8\xd7\xc9\xd5s\x0eO\x94\x89\x08\x95\x14\x7f\x9b\xb3k% =\xed\x9fh\x08S\xa2+\x8c\xa3\x06_\xeeRn\xf2?Y\xc0\xe7F\xf2Ne@\x00[T\x99<@%\xf5\xfc\xf6u\xfd\xdb\xc0%\xea-\x01\xf6\x03\x0f\xd6\x95\x80\xa5\x98\xc1\x8fR\x0b\xdb*\xce8\xec\xc2Y\xfb\x05\x0e\xf4y/\x80' i\xca+H\x0e\xf8\xdf\xb9\x9e;i\xde\xffg\xcf\x9a\xa5\x14\xfa\xe4`\xaf\x5c\xb4\xa3\xfa\xefx\xcb\x12H\xe40Pbr\xb1o\xfaY\x06g\xa2\xd2\x9e_\xfd\x19\xaaI\x7f\xa5*\xe6\x06\xcf\xf3\x1a\x86<\xb1p\xa4\xc95\xe9\x92\xec\x97\xc7\x04\xaf$Q\xe98vW\x8djD\xf6\xd7!^\xad\xef\xf0\x94\x01{\xa5\xb39Z\x80\x94i\xf7:\x80\xc7\xa6\x1b\xda\xb3\x1a\x0a\xcc\xe9,\x1e\xd2T\x0e\x16\x0ee*\x03b\xb2VX~\xe6\x10\x96\xd5L\xe6e-\x1f0;\x09\x5c\x08\x94\xc36?\xb93\x0b\x10U!\xc8BA@$\xad\x01\x92bR\x02@\x12@\x12\x01\x81\x00\x05\xaaEH\x8c\xb4(2j@)\xb0R\x02\x06\x001B\x12I\x00K\x88\x96\xcc\x00\x03\x83 $\x00\x22\x0a\x14\xc0`\x00\x01`\x00\x00\x00H\x82ED\x88!\x08J\x01B\xa2\x00\x19\xd0\xb2\xa5\xa0\x0c\x08\x98\x00\x00\x01\x02\x82\x10\x14$\x08\x010\x084\x00\xa8\x11DV\x01 !\x84\x04\x02\x89@\x05$J\xc3\x10\x04!\xa0$\x1ad*\x08\xc32\x08\x88&\x80\x80\x04B\x91\x80\xc8 \x94\x04\x08 \x08\x084\x10Bj\x04\x000\xa1\xb0b\x852\x00B\x0c\x04\x0b\x1a\x00\x00$\x10H\x09\x11\x00\x02C\x00T\xb4\xb0H\x01\x95\xa5\x11\x01\x00\x10%\xa0JRR\x98\x02\x0a\x89\x90\xa0\xa0%\xa0\xa4\xa0\x0c\x0a\x01\x04\x1a\x22\x01\x93`\x19\x1a\x92\x04\x85\x80D\x91\x14\x0c\x15\x10\x10\x0d\xd1\x00)\x91*\x06d\x081\x98\x81\x02\x09(\x83\x90H\x05\x80! \xc0h`\x02\xc0\x02\x84\xa0,\xc1\x0a\x91 \x89XP\x01\xb4P\x90\x12\x00\x98\x84P\x04\x88\x08il\xa4\x01\x01\x88\x0cH\x03D\x08\x82\x86\xc0\x90@\x0c\x00\x11\x04\x86$ \x08 \x02\x06\x84(\x00\x84\x04\x82\xa9 X\x02\x00\x08\x0a\x94E\x92\x89\x04\x08\x805i\x88@\x82\x84\x00\x11J,\x04\x04\x0c\x89I\x02\x99\x82\x1a\x04\x80d\x16\x10@\x90\x01I`\x08D6I\x0b\x01\x19\x00&\x02$\x80D\x84 %\x90\x10\x0a`\x04I\x02\x00@$%P@\x80\x00\x04(K\x00\x94\xa0$\x01\xa8\x14\x04\x00h\x96\x08\x10\x10\x11l\x00\x12\x08 \xa1,@\x00\x12\xa6LP\x14\x90%\xb4\x08\x09\x12*\x12\x80D\x01\x04\x22\x14\x00I2\x89\x1a\xa0\x81 K\x93`\x06d\xd9\x22$\x09\x00I@\x98!A\x8b4\x03!\x90,\x90\x04 !\x90\xa0\x10D\x80\x88Y\x91\xa0\x14(\x00\x0a\x0aX\x14\x22\x08\x09\xb1\xa1\x00\xa4\x00\x19\xa4\x91`\xb6\x02\x00\x010\x08\x16\x80I\x80P @\x96\x22\x81\x14\x90\x01 \x06M\x02\x11\x16\x1a\x14\xe0-\xaa\x8e#\xa9\xae\x14\xc1\x02\xd8%\x9c\x89\xf9\x1b\xe8\xb3,\xdax\xf7\xe8\x11\xaa\x91s\x03U\x80\x91\x9d\xd6M\xa9\xf1\xd0iJ\x9dm\x86w\x847a1\xbdl\x18\xdd\x81\x9f\xd8\xe4K\x1f\x9e_\xfe\x9e\x7f\x9f\xde3u\xaa:RFe!v\xbd\x1c\xfb\xc6'\x00J_rcf/\xdb\xfa\xf4X\xef\x89\xd1q\xf4\x0e\xd5\x88\xfbWD\x92!l\xd6\x8e p]v\x1f\x9a\x825\x1c\x85\xb2LO\x93a\x99T\xe3<\x84\xa3S\x08Z<\x9b5h^\x15\xd4k\x9b\xf5\xdfDe\xc1\xcf8\x15#\xfb\xc7\x1a\x0b\x0d:M\xf9\xa4\xb1\xbbt\x84\x96\xdd\x8a\xef\xb2\xd0\xe6\xbf\xdd,\xf7\x8b\x02F\xb6\xfehJl\xfe\xcd\x8f\x90S\xb5\xa1\x0de\xfdtvoO\x0c\xc0\x16J\x14\xe1p\xb4\xc9d\xc9\xe8\x0c\x0e\xc4Ea\xfb\x1a\x1a+(\xa3a\xc2f\xaf\xf2\x0c\xfe\xd0.P\xa8\x92\x97\x86#\x14\xddV\xc7T*7b[Z\x87;\x97\x9dd\x1f\xfdzL\xd2*\xb0N\x94p\xa7'\xd8\x0a'\x0a\xec\x97gc\x0ec%\xe5\x06\x01R.nB\xb0\xa7X3\xf3|1\x17B\x96\xf3\x9f\xeey1\xc8\xdb\x97]\xdd\x90cW\xefi\xea\x5cD\xcd\xa7\xfd\xd5\xb1\xd5J\x92\x09tSU~@\x10#\xbf-b\xfaD\xb4\xc0\xe9\xe1`2\x84\xe8&tDk_\x18a\xaf?\x05\xa6\x96\x17\xb7\xaa\xc9\xa6$\xce\xe0R\xd9y\xd9\x1a\x1a;\xd6\x8a'M\xf5\x07\xb9\x22\xfd)\x9f\xd8\x8a/)w\xf9\xf2G\xb4\xeb(N[N\x03\xeb\x90\xff\x85\x08\xe7\xebg\xce\x93wHg\xd6\x5c\xc3\xbb\xdb\xc1\x18\xb3\x07\xcag\x9a\x09\xf4\xf2\xe9\xc5\xec_\xb2t\xe3M\xca%\x80LB\xe4Zt_\xb4\x0c\x8c\x99\x80\x02\x95\x8bt\xb4\xa2\xb6G\xcc\x1et\x8a\xf8\xde-\xc0G\xeb\x0fHJ^\xa4\x90?R\xa0NT\xe9\xd2k\xd4q\x87j\xd9\x97\xf6\x06\x0c\xffQ9BC\x06\x8b@y=\xfa\xc6\xd3\x88}4&\x8a\x5c\x89I\xdct\xaaK|\x1b\x97\xa1\x00\xe9\xea`\xe4\x8b"
data = data[16:]
XOR_BYTES, data = data[:256], data[256:]
INITIAL_DATA, BITMASKS = array('Q', data[:512]), array('Q', data[512:])
assert len(XOR_BYTES) == 256
assert len(INITIAL_DATA) == 64
assert len(BITMASKS) == 64
# define xored flag as array of bit vectors
xored_flag = [BitVec(f'xored_flag_{i}', 8) for i in range(256)]
# checkFlag logic:
data1 = [BitVecVal(x, 64) for x in INITIAL_DATA]
k = 0
for i in range(64):
for j in range(64):
if (BITMASKS[i] >> (63 - j)) & 1:
bit = 7 - (k & 7)
data1[i] |= ZeroExt(63, Extract(bit, bit, xored_flag[k // 8])) << (63 - j)
k += 1
# unnamed_function_6 logic:
data2 = [simplify(x) for x in data1] + [BitVecVal(0, 64) for _ in range(64)]
for i in range(64):
for j in range(64):
bit = 63 - i
data2[64 + i] = (data2[64 + i] << 1) | ZeroExt(63, Extract(bit, bit, data1[j]))
# unnamed_function_5 logic:
s = Solver()
# for each half
for off in [0, 64]:
# unnamed_function_1 logic: sum of set bits should be equal 32
for i in range(64):
s.add(Sum([ZeroExt(7, Extract(j, j, data2[off+i])) for j in range(64)]) == 32)
# unnamed_function_2 logic: all values should be different
for i in range(64):
for j in range(i + 1, 64):
s.add(data2[off+i] != data2[off+j])
# unnamed_function_4 logic: ~x & (~x >> 1) & (~x >> 2) == 0
for i in range(64):
s.add(~data2[off+i] & LShR(~data2[off+i], 1) & LShR(~data2[off+i], 2) == 0)
# unnamed_function_3 logic: x & (x >> 1) & (x >> 2) == 0
for i in range(64):
s.add(data2[off+i] & LShR(data2[off+i], 1) & LShR(data2[off+i], 2) == 0)
# phew!
while s.check() == sat:
m = s.model()
# xor the result back
enc_flag = bytes([m[x].as_long() ^ y for x, y in zip(xored_flag, XOR_BYTES)])
# try decrypting it
flag = AES.new(KEY, AES.MODE_CBC, IV).decrypt(enc_flag)
if b'HackTM' in flag:
print(flag)
break
s.add(Or([m[x] != x for x in xored_flag]))
else:
print('not found')
```
After running the script, we get the flag.
Also need to note that only first 8 elements of each half are checked in wasm, so it is possible to pass wrong input that validates to be correct. But extending those checks to full 64 elements narrows it down to a single flag value, which is:
```
HackTM{bee3dc52aabec5c1b673d8d2beaeef64fbbf94fbbfe3f7ebcf716e465bd7af2a609a0be0717f6bcbed7c33dcfc95aadaae2f3e046a3b1ee42dbfb7da3687d77fbece4d957b48c3c3fa00d77da8aeffdedbe823bbc89678ded4bfe9f71fdcbf8c9cbd8b84ebffb118eb68b39bee0bfeccd07efbf8cd530b2dadbff4af}
```
Sign in with Wallet
Connect another wallet