[Writeup] Solution to the CTF Challenge in Readme

## Final Result

```
a = 2057944750
b = -1256157214
c = 411975585
```

The four magic numbers recovered from the challenge are: `0x166f05f`, `0xccedffde`, `0xdeadbeef`, `0x9337fe4f`

## Write Up

### Initial Idea

I noticed that the core mechanism of the obfuscation involves splitting a single `i32` into a vector `<32 x i32>`.
Within this vector, each `i32` represents a single bit of the original integer. Using a "Mod3" representation:
- A `1` in the original integer is represented as `i32 2`.
- A `0` in the original integer is represented as `i32 1`.

Below is the source code for the challenge (I used `K1-4` to represent the original magic numbers):
```c
#include
int main() {
int a, b, c;
printf("Please input a, b, c:\n");
scanf("%d%d%d", &a, &b, &c);
if (((b + K1) & (c + K2)) == (a ^ K3)) {
if (a + c == K4) {
printf("%d %d %d\n", a, b, c);
puts("Win!");
}
}
return 0;
}
```

I compiled this with `clang` to inspect the structure of the LLVM IR.
In the code below, I used `123, 456, 789, 101112` for `K1-K4`.

```llvm
define dso_local noundef i32 @main() local_unnamed_addr #0 {
%1 = alloca i32, align 4
%2 = alloca i32, align 4
%3 = alloca i32, align 4
call void @llvm.lifetime.start.p0(i64 4, ptr nonnull %1) #3
call void @llvm.lifetime.start.p0(i64 4, ptr nonnull %2) #3
call void @llvm.lifetime.start.p0(i64 4, ptr nonnull %3) #3
%4 = tail call i32 @puts(ptr nonnull dereferenceable(1) @str)
%5 = call i32 (ptr, ...) @__isoc99_scanf(ptr noundef nonnull @.str.1, ptr noundef nonnull %1, ptr noundef nonnull %2, ptr noundef nonnull %3)
%6 = load i32, ptr %2, align 4, !tbaa !5
%7 = add nsw i32 %6, 123
%8 = load i32, ptr %3, align 4, !tbaa !5
%9 = add nsw i32 %8, 456
%10 = and i32 %9, %7
%11 = load i32, ptr %1, align 4, !tbaa !5
%12 = xor i32 %10, %11
%13 = icmp eq i32 %12, 789
%14 = add nsw i32 %11, %8
%15 = icmp eq i32 %14, 101112
%16 = select i1 %13, i1 %15, i1 false
br i1 %16, label %17, label %20

17: ; preds = %0
%18 = call i32 (ptr, ...) @printf(ptr noundef nonnull dereferenceable(1) @.str.2, i32 noundef %11, i32 noundef %6, i32 noundef %8)
%19 = call i32 @puts(ptr noundef nonnull dereferenceable(1) @.str.3)
br label %20

20: ; preds = %17, %0
call void @llvm.lifetime.end.p0(i64 4, ptr nonnull %3) #3
call void @llvm.lifetime.end.p0(i64 4, ptr nonnull %2) #3
call void @llvm.lifetime.end.p0(i64 4, ptr nonnull %1) #3
ret i32 0
}
```

The goal is to locate these `K`s.

I noticed that `BitFuscatorImpl` relies heavily on `addWithOverflow`. Therefore, analyzing `add` or `sub` directly is difficult. However, the patterns for `and` and `icmp` are quite distinct.

More importantly, if we provide the input `a = 0, b = 0, c = 0`:
- The operands of the `and` instruction become exactly **K1** and **K2**.
- The RHS of the two `icmp` instructions become **K3** and **K4**.

Now let's look at the obfuscation for `and` and `icmp`:

### `And` Instruction

```c++
Value *visitAnd(BinaryOperator &I) {
if (I.getType()->isVectorTy())
return nullptr;
auto *Op0 = convertToBit(I.getOperand(0));
auto *Op1 = convertToBit(I.getOperand(1));
auto *Res = BitRep->bitAnd(Op0, Op1);
return convertFromBit(Res, I.getType());
}
```

To locate the obfuscated `and` and `icmp`, I modified `visitAnd` and `visitICmp` in the obfuscator to insert a `InlineAsm` before and after the instructions. The obfuscated IR for `and` looked like this:

```llvm
call void asm sideeffect "# [FSubFuscator] Start: Obfuscated And.", ""() #3
%678 = add nsw <32 x i32> %361, splat (i32 -1)
%679 = add nsw <32 x i32> %677, splat (i32 -1)
%680 = mul <32 x i32> %679, %678
%681 = add <32 x i32> %680, splat (i32 1)
call void asm sideeffect "# [FSubFuscator] End: Obfuscated And.", ""() #3
```

Here, `%361` and `%677` correspond to `K1` and `K2` (when inputs are 0).

Now let's look at the disassembly.

I found that this `and` appears before this `load` in the original LLVM IR:
```llvm
%11 = load i32, ptr %1, align 4, !tbaa !5
```

In the final assembly, it also appears right before a load.

```asm
328b: 8b 84 24 1c 02 00 00 mov 0x21c(%rsp),%eax
```

The assembly pattern for the `and` looked like this:

```asm
3017: 66 45 0f 76 ff pcmpeqd %xmm15,%xmm15
301c: 66 0f 6f ac 24 30 01 movdqa 0x130(%rsp),%xmm5
3023: 00 00
3025: 66 41 0f ef ef pxor %xmm15,%xmm5
302a: 66 0f fe ac 24 40 01 paddd 0x140(%rsp),%xmm5
3031: 00 00
3033: 66 44 0f 6f 9c 24 c0 movdqa 0xc0(%rsp),%xmm11
303a: 00 00 00
303d: 66 45 0f ef df pxor %xmm15,%xmm11
3042: 66 44 0f fe 9c 24 a0 paddd 0xa0(%rsp),%xmm11
3049: 00 00 00
304c: 66 0f 6f 3c 24 movdqa (%rsp),%xmm7
3051: 66 41 0f ef ff pxor %xmm15,%xmm7
3056: 66 0f fe bc 24 d0 00 paddd 0xd0(%rsp),%xmm7
305d: 00 00
305f: 66 0f 7f 3c 24 movdqa %xmm7,(%rsp)
3064: 66 0f 6f bc 24 50 01 movdqa 0x150(%rsp),%xmm7
306b: 00 00
306d: 66 41 0f ef ff pxor %xmm15,%xmm7
3072: 66 0f fe 7c 24 70 paddd 0x70(%rsp),%xmm7
3078: 66 44 0f 6f b4 24 b0 movdqa 0xb0(%rsp),%xmm14
```

`pcmpeqd %xmm15,%xmm15` generates `splat -1`. Then, XORing with it acts as a bitwise NOT.

I noticed that in the obfuscation of `and A B`, there is a pattern of `(A-1)*(B-1)`.
At first, I thought this might be: `(A-1)*(B-1) ---> (-A+1)*(-B+1) ---> (~A)*(~B) ---> (-1 ^ A)*(-1 ^ B)`. So, it seemed like the other operand of `pxor` would be A and B.

However, I found this was not the case. The other operand of `pxor` is `0` in runtime, so the result of the `pxor` is also `splat -1`. The result of `pxor` is the operand for `paddd`. Consequently, `paddd` is the instruction performing `A-1`. This means the operand of `paddd` is the original value we are seeking.

(I haven't figured out exactly why this is happening. If the result of `pxor` is `splat -1`, why not use the `xmm15` generated earlier?)

There are 16 `paddd` instructions in total. By stepping through GDB and finding that operand, I obtained `K1` and `K2`.

But it wasn't done yet! The bit order of `K1` and `K2` was scrambled. I kept adjusting the inputs `a`, `b`, and `c` and discovered the layout is as follows:

```
1111 0000 0000 | K1 8
2111 1000 0001 | K1 7
1221 0110 0110 | K1 6
1221 0110 0110 | K1 5
2222 1111 1111 | K1 4
1111 0000 0000 | K1 3
2121 1010 0101 | K1 2
1122 0011 1100 | K2 8
1122 0011 1100 | K2 7
1222 0111 1110 | K2 6
2122 1011 1101 | K2 5
2222 1111 1111 | K2 4
2222 1111 1111 | K2 3
2122 1011 1101 | K2 2
1222 0111 1110 | K2 1
2222 1111 1111 | K1 1
```

The first column is extracted from the 16 `paddd` instructions in order. The second column is the conversion to the original binary representation. A tricky part was that the bit order was reversed, so I had to reverse it to get the third column. The third column contains the actual content of K1 and K2. Also, they are not arranged from MSB to LSB.

Initially, I noticed in the disassembly that there was a big gap between the first 15 `paddd` instructions and the 16th one. This suggested they might not be in MSB->LSB order. I tested with some inputs and found that the LSB of K1 was placed at the very end. The final organized result is shown above.

Finally, arranging them gives:

- K1 = 0x166f05f
- K2 = 0xccedffde

### `ICmp` Instruction

```c++
Value *visitICmp(ICmpInst &I) {
if (!I.getOperand(0)->getType()->isIntegerTy())
return nullptr;

auto *Op0 = I.getOperand(0);
auto *Op1 = I.getOperand(1);
if (I.isRelational()) {
Op0 = Builder.CreateFreeze(Op0);
Op1 = Builder.CreateFreeze(Op1);
}
auto Pred = I.getPredicate();
if (ICmpInst::getStrictPredicate(I.getUnsignedPredicate()) ==
ICmpInst::ICMP_UGT) {
std::swap(Op0, Op1);
Pred = ICmpInst::getSwappedPredicate(Pred);
}

auto [Res, Carry] = addWithOverflow(
Op0, Op1,
/*Sub=*/true, /*Unsigned=*/I.isEquality() || I.isUnsigned());
// TODO: use Bits?
switch (Pred) {
case ICmpInst::ICMP_EQ:
return Builder.CreateICmpEQ(Res, Constant::getNullValue(Res->getType()));
case ICmpInst::ICMP_NE:
return Builder.CreateICmpNE(Res, Constant::getNullValue(Res->getType()));
case ICmpInst::ICMP_ULT:
return Carry;
case ICmpInst::ICMP_ULE:
return Builder.CreateOr(
Carry,
Builder.CreateICmpEQ(Res, Constant::getNullValue(Res->getType())));
case ICmpInst::ICMP_SLT:
return Builder.CreateXor(
Carry,
Builder.CreateICmpSLT(Res, Constant::getNullValue(Res->getType())));
case ICmpInst::ICMP_SLE:
return Builder.CreateXor(
Carry,
Builder.CreateICmpSLE(Res, Constant::getNullValue(Res->getType())));
default:
llvm_unreachable("Unexpected ICmp predicate");
}
}
```

Next, let's look at `icmp`. The obfuscated IR is too long to include here. However, from the code above, the obfuscation strategy is to subtract and check if the result is 0 (`icmp eq`).

At the end of the subtraction, `Res` needs to be converted back to its original form (`convertFromBit`). The `convertFromBit` for Mod3 looks like this:

```c++
Value *convertFromBit(Value *V) override {
return Builder.CreateICmpSGT(V, ConstantInt::get(V->getType(), 1));
}
```

This means there will be many `sgt`. I searched and found exactly 16 `pcmpgtd` instructions in the disassembly, which corresponds perfectly to two `convertFromBit` of `i32`.

To find `K3` and `K4`, note that when `a=b=c=0`:
- The first icmp subtraction result is `(K1 & K2) - K3`.
- The second icmp subtraction result is `0 - K4`.

Since we already know `K1` and `K2`, we simply need to recover these subtraction results.

Let's look at the second `icmp` first. The last 8 `pcmpgtd` instructions:
```asm
643d: 66 44 0f 66 cc pcmpgtd %xmm4,%xmm9
6442: 66 0f 66 f4 pcmpgtd %xmm4,%xmm6
6446: 66 41 0f eb f1 por %xmm9,%xmm6
644b: 66 0f 66 dc pcmpgtd %xmm4,%xmm3
644f: 66 0f 66 d4 pcmpgtd %xmm4,%xmm2
6453: 66 0f eb d3 por %xmm3,%xmm2
6457: 66 0f 6b d6 packssdw %xmm6,%xmm2
645b: 66 44 0f 66 c4 pcmpgtd %xmm4,%xmm8
6460: 66 0f 66 c4 pcmpgtd %xmm4,%xmm0
6464: 66 41 0f eb c0 por %xmm8,%xmm0
6469: 66 0f 66 ec pcmpgtd %xmm4,%xmm5
646d: 66 0f 66 cc pcmpgtd %xmm4,%xmm1
6471: 66 0f eb cd por %xmm5,%xmm1
6475: 66 0f 6b c8 packssdw %xmm0,%xmm1
6479: 66 0f 63 ca packsswb %xmm2,%xmm1
647d: 66 0f d7 c1 pmovmskb %xmm1,%eax
6481: 31 d2 xor %edx,%edx
```

Using GDB, I found that one operand is `splat 1`, so the other operand must be the result of the subtraction.
Finally, I got the following data:

```
1221 0110 0110 | -K4 8
1111 0000 0000 | -K4 4
1122 0011 1100 | -K4 7
2111 1000 0001 | -K4 3
1122 0011 1100 | -K4 6
2212 1101 1011 | -K4 2
1112 0001 1000 | -K4 5
2111 1000 0001 | -K4 1
```

The first column is the extracted operand, and the second is the binary representation. Similarly, I had to reverse them to get the third column. Also, they are not in MSB->LSB order. I tested with more inputs and found the order is interleaved: 8 -> 4 -> 7 -> 3 -> 6 -> 2 -> 5 -> 1.

Arranging them gives `0-K4` as `0x6cc801b1`. Using a similar method on the first 8 `pcmpgtd` instructions, I found `(K1&K2)-K3` to be `0x21b7316f`. Finally, I got:

- K3 = 0xdeadbeef
- K4 = 0x9337fe4f

### Solving the Equation

Finally, a small script to solve the equation:

```python
from z3 import *

def solve_challenge():
s = Solver()

a = BitVec('a', 32)
b = BitVec('b', 32)
c = BitVec('c', 32)

K1 = 0x166f05f
K2 = 0xccedffde
K3 = 0xdeadbeef
K4 = 0x9337fe4f

s.add(((b + K1) & (c + K2)) == (a ^ K3))

s.add(a + c == K4)

if s.check() == sat:
print("Solution found!")
m = s.model()

val_a = m[a].as_signed_long()
val_b = m[b].as_signed_long()
val_c = m[c].as_signed_long()

print(f"Input: {val_a} {val_b} {val_c}")
else:
print("No solution found.")

if __name__ == "__main__":
solve_challenge()
```

Output:

```
Solution found!
Input: 2057944750 -1256157214 411975585
```

Many thanks to the author for this interesting project and CTF challenge!