# SmileyCTF 2025

## Success

<mark style="color:blue;">Rev</mark>&#x20;

> &#x20;avoid it at all costs

```python
from z3 import *

solver = Solver()
chars = [BitVec(f'c_{i}', 32) for i in range(39)]

solver.add(chars[37] * chars[15] == 3366)
solver.add(chars[8] + chars[21] == 197)
solver.add(chars[8] * chars[13] == 9215)
solver.add(chars[0] * chars[3] == 2714)
solver.add(chars[3] + chars[21] == 159)
solver.add(chars[1] * chars[20] == 5723)
solver.add((chars[6] | chars[37]) == 105)
solver.add(chars[11] * chars[7] == 11990)
solver.add((chars[29] & chars[25]) == 100)
solver.add((chars[16] | chars[29]) == 127)
solver.add(chars[20] - chars[6] == -8)
solver.add(chars[21] + chars[20] == 197)
solver.add(chars[2] + chars[36] == 77)
solver.add(chars[35] * chars[11] == 3630)
solver.add(chars[4] * chars[3] == 2714)
solver.add((chars[35] ^ chars[6]) == 72)
solver.add(chars[25] + chars[24] == 221)
solver.add(chars[14] * chars[36] == 3465)
solver.add((chars[15] - chars[11]) - 148 == -156)
solver.add(chars[37] + chars[17] == 138)
solver.add((chars[1] ^ chars[38]) == 70)
solver.add(chars[9] + chars[29] == 212)
solver.add(chars[30] - chars[10] == 7)
solver.add(chars[10] + chars[33] == 206)
solver.add(chars[7] * chars[15] == 11118)
solver.add(chars[28] * chars[14] * 55 == 641025)
solver.add(((chars[7] | chars[4]) | 216) == 255)
solver.add(chars[24] + chars[4] == 151)
solver.add(chars[2] * chars[30] == 4928)
solver.add(chars[5] + chars[22] == 224)
solver.add((chars[18] | chars[36]) == 127)
solver.add(chars[13] + chars[34] == 195)
solver.add((chars[9] | chars[17]) == 111)
solver.add(chars[12] * chars[9] == 10403)
solver.add((chars[25] ^ chars[27]) == 23)
solver.add((chars[13] ^ chars[34]) == 59)
solver.add(chars[18] + chars[31] == 200)
solver.add(chars[17] + chars[32] == 213)
solver.add(chars[2] * chars[12] == 4444)
solver.add(chars[24] * chars[31] == 11025)
solver.add(chars[5] * chars[0] == 5658)
solver.add((chars[10] + chars[32]) + 228 == 441)
solver.add(chars[35] * chars[0] == 1518)
solver.add((chars[30] | chars[8]) == 113)
solver.add(chars[28] - chars[34] == 11)
solver.add(chars[26] * chars[14] == 9975)
solver.add(chars[31] * chars[22] == 10605)
solver.add(chars[26] * chars[32] * 239 == 2452140)
solver.add(chars[28] * chars[38] == 13875)
solver.add(chars[18] + chars[16] == 190)
solver.add((chars[27] + chars[26]) + 96 == 290)
solver.add(chars[22] - chars[38] == -24)
solver.add(chars[33] + chars[5] == 224)
solver.add(chars[19] * chars[16] == 10355)
solver.add(chars[27] + chars[1] == 158)
solver.add(chars[33] + chars[12] == 202)
solver.add(chars[19] * chars[23] == 10355)

result = solver.check()
model = solver.model()
flag = ''.join(chr(model[chars[i]].as_long()) for i in range(39))
print(flag)
```

`└─$ .;,;.{imagine_if_i_made_it_compiled!!!}`

## rorecovery1

<mark style="color:blue;">Forensics</mark>

We were given a corrupted Roblox binary. Upon inspecting the file, both the header and footer contained an unusual `rblx`signature. By referencing the [Roblox Binary Model Format](https://github.com/rojo-rbx/rbx-dom/blob/master/docs/binary.md) and comparing it with a sample file downloaded from Roblox Studio, we are able to reconstruct the original binary structure.

<div data-full-width="true"><figure><img src="https://1163145841-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F4UkbOn8PnZkBCBDx07r4%2Fuploads%2F2CAX8iJl46vRjEFQi5Qu%2Fimage.png?alt=media&#x26;token=150b0cd4-b4e4-401f-952f-cef391aba084" alt="" width="324"><figcaption><p>given rorecovery1</p></figcaption></figure></div>

<figure><img src="https://1163145841-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F4UkbOn8PnZkBCBDx07r4%2Fuploads%2FbOfvxgOZw9HoHAJnyVJA%2Fimage.png?alt=media&#x26;token=5ee1ba9c-c040-492a-8e9c-c7888bd5e66b" alt="" width="325"><figcaption><p>sample.rbxl</p></figcaption></figure>

<figure><img src="https://1163145841-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2F4UkbOn8PnZkBCBDx07r4%2Fuploads%2FIMfDiPP8fmKECiye5nSs%2Fimage.png?alt=media&#x26;token=de659ba4-b87d-4493-b47e-44ad57dc5f71" alt="" width="563"><figcaption><p>fixed_rorecovery1.rbxl</p></figcaption></figure>

