problem

https://twitter.com/tayandyou

$ ./tayy
=============================================================
Welcome to the future of AI, developed by NIA Research, Tayy!
=============================================================
1. Talk to Tayy.
2. Flag?
0. Exit.
> 1
=============================================================
1. Ayy lmao, Tayy lmao.
2. You are very cruel.
3. Memes are lyf.
4. Go away!.
5. zzzz
6. Cats > Dogs.
7. Dogs > Cats.
8. AI is overrated?.
9. I dont like you.
0. <exit to menu>
> 8
Tayy: Die, human!

=============================================================
1. Talk to Tayy.
2. Flag?
0. Exit.
> 2
Flag: EMhd?^\67cTC<y^D=?SLCSL]AVUS#Yo?l-4^_s
=============================================================
1. Talk to Tayy.
2. Flag?
0. Exit.
> 0

Tay has a flag string. It is modified depending on your choice at 1. Talk to Tayy., and readable via 2. Flag?.

solution

The program is like below. The original % is C’s one, so below example sometimes returns wrong results if the argument has negative integer.

#!/usr/bin/env python2
def tayy(key):
    flag = map(ord, "4545584c831918231c404e35265b03672c713248373f30393a473e34214f5d694a28270a56".decode("hex"))
    for i in range(len(key)):
        for k in range(len(flag)):
            if i % 2 == 0:
                flag[k] += k * key[i] % 37
            else:
                flag[k] -= k * key[i] % 37
            flag[k] %= 256
    return ''.join(map(chr, flag))
print tayy([1, 2, 3])

You can get flag using z3. You should not forget that it accepts arbitrary integer, not only $1, 2, \dots, 9, 0$.

ECTF{41_1S_D3f1n1t3lY_N0T_TH3_FuTUR3}.

implementation

This implementation has appearent bug around the %. But I got the flag luckily, so it is not fixed.

#!/usr/bin/env python2
from z3 import *

s = Solver()
flag = [Int('flag_%d' % i) for i in range(37)]
key  = [Int('key_%d'  % i) for i in range(7) ]

# flag constraint
initial_flag = "4545584c831918231c404e35265b03672c713248373f30393a473e34214f5d694a28270a56".decode('hex')
for k in range(len(initial_flag)):
    s.add(flag[k] == ord(initial_flag[k]))

# key constraint
for i in range(len(key)):
    s.add(0 <= key[i])
    s.add(key[i] < 37)
for i in range(0, len(key)-2):
    s.add(key[i] <= key[i+2])

# relation constraint
for k in range(len(flag)):
    for i in range(len(key)):
        if i % 2 == 0:
            flag[k] += k * key[i] % 37
        else:
            flag[k] -= k * key[i] % 37
    flag[k] %= 256

# result constraint
for k, c in list(enumerate('ECTF{')) + [(len(flag)-1, '}')]:
    s.add(flag[k]  == ord(c))
for k in range(len(flag)):
    s.add(0x20 <= flag[k])
    s.add(flag[k] <= 0x7e)

r = s.check()
if r == sat:
    m = s.model()
else:
    print 'unsat'
    exit(1)

print ','.join([str(m[n].as_long()) for n in key])