Rating: 4.3

# Just Rust (41 solves)

> Clam really enjoys writing in C, but he realizes that he'll have to learn another language eventually. After all, he's grown pretty rusty after only programming in C for a year. So, he decided to write a program to create some ASCII art from user input. He also provided a sample output!
>
> Author: aplet123

*output.txt*:


What do you want to encode?
[REDACTED]
CCHJEHMK
CFKJCEOL
FOJLMOJJ
BDN@H@BA
ODMJHFCJ
MOOKMOOO
OOAOFOGI
@@@@@@@@


The binary is written in rust but has very simple encoding algorithm.

Our job is to find initial input.

The encoding algorithm:

python
def algo(inp):
out = [0x40 for i in range(72)]

for i in range(len(inp)):
t = i
x = i >> 3
for j in range(8):
out[8 * j + (t & 7)] |= ((1 << (j & 7)) & inp[i]) >> (j & 7) << (x & 7)
t += 1
print(''.join(map(chr, out)))


Solution:

python
from z3 import *
import sys

def find_all_possible(s):
while s.check() == sat:
model = s.model()
block = []
out = ''
for i in range(32):
c = globals()['b%i' % i]
out += chr(model[c].as_long())
block.append(c != model[c])
s.add(Or(block))
print(out)

def main():
flag = "CCHJEHMKCFKJCEOLFOJLMOJJBDN@H@BAODMJHFCJMOOKMOOOOOAOFOGI@@@@@@@@"
s = Solver()
out = [0x40 for i in range(72)]
for i in range(32):
globals()['b%d' % i] = BitVec('b%d' % i, 8)
t = i
x = i >> 3
for j in range(8):
out[8 * j + (t & 7)] |= ((1 << (j & 7)) & globals()['b%d' % i]) >> (j & 7) << (x & 7)
t += 1

s.add(globals()['b0'] == ord('a'))
s.add(globals()['b1'] == ord('c'))
s.add(globals()['b2'] == ord('t'))
s.add(globals()['b3'] == ord('f'))
s.add(globals()['b4'] == ord('{'))

for i in range(64):
s.add(out[i] == ord(flag[i]))

find_all_possible(s)

if __name__ == "__main__":
sys.exit(main())


yields the flag

bash
actf{b1gg3r_4nd_b4dd3r_l4ngu4g3}


Original writeup (https://github.com/archercreat/CTF-Writeups/blob/master/angstromctf/rev/Just%20Rust/README.md).