Desc : Do equations embarrass you? Well, nothing can stop you if you've got the z3al! File : https://shorturl.at/lCOU9

z3al-writeup-ISFCR.py

from z3 import *
st = [BitVec(f'{i}', 8) for i in range(0x27)]
s = Solver()

s.add(st[0x00]^st[0x02]^st[0x04]==0x60)
s.add(st[0x04]^st[0x06]^st[0x08]==0x36)
s.add(st[0x08]^st[0x0a]^st[0x0c]==0x71)
s.add(st[0x0c]^st[0x0e]^st[0x10]==0x32)
s.add(st[0x10]^st[0x12]^st[0x14]==0x3f)
s.add(st[0x14]^st[0x16]^st[0x18]==0x01)
s.add(st[0x18]^st[0x1a]^st[0x1c]==0x2a)
s.add(st[0x1c]^st[0x1e]^st[0x20]==0x3f)
s.add(st[0x20]^st[0x22]^st[0x24]==0x7a)
s.add(st[0x01]^st[0x03]^st[0x05]==0x64)
s.add(st[0x05]^st[0x07]^st[0x09]==0x7e)
s.add(st[0x09]^st[0x0b]^st[0x0d]==0x74)
s.add(st[0x0d]^st[0x0f]^st[0x11]==0x00)
s.add(st[0x11]^st[0x13]^st[0x15]==0x58)
s.add(st[0x15]^st[0x17]^st[0x19]==0x62)
s.add(st[0x19]^st[0x1b]^st[0x1d]==0x5b)
s.add(st[0x1d]^st[0x1f]^st[0x21]==0x5c)
s.add(st[0x21]^st[0x23]^st[0x25]==0x62)
s.add(st[0x00]^st[0x01]^st[0x03]==0x60)
s.add(st[0x03]^st[0x04]^st[0x06]==0x70)
s.add(st[0x06]^st[0x07]^st[0x09]==0x6c)
s.add(st[0x09]^st[0x0a]^st[0x0c]==0x33)
s.add(st[0x0c]^st[0x0d]^st[0x0f]==0x68)
s.add(st[0x0f]^st[0x10]^st[0x12]==0x3f)
s.add(st[0x12]^st[0x13]^st[0x15]==0x63)
s.add(st[0x15]^st[0x16]^st[0x18]==0x58)
s.add(st[0x18]^st[0x19]^st[0x1b]==0x34)
s.add(st[0x1b]^st[0x1c]^st[0x1e]==0x75)
s.add(st[0x1e]^st[0x1f]^st[0x21]==0x37)
s.add(st[0x21]^st[0x22]^st[0x24]==0x6e)
s.add(st[0x01]^st[0x02]^st[0x04]==0x75)
s.add(st[0x04]^st[0x05]^st[0x07]==0x6c)
s.add(st[0x07]^st[0x08]^st[0x0a]==0x3d)
s.add(st[0x0a]^st[0x0b]^st[0x0d]==0x70)
s.add(st[0x0d]^st[0x0e]^st[0x10]==0x34)
s.add(st[0x10]^st[0x11]^st[0x13]==0x5a)
s.add(st[0x13]^st[0x14]^st[0x16]==0x01)
s.add(st[0x16]^st[0x17]^st[0x19]==0x0a)
s.add(st[0x19]^st[0x1a]^st[0x1c]==0x2d)
s.add(st[0x1c]^st[0x1d]^st[0x1f]==0x43)
s.add(st[0x1f]^st[0x20]^st[0x22]==0x27)
s.add(st[0x22]^st[0x23]^st[0x25]==0x3f)
s.add(st[0x00]^st[0x04]^st[0x06]==0x75)
s.add(st[0x04]^st[0x08]^st[0x0a]==0x25)
s.add(st[0x08]^st[0x0c]^st[0x0e]==0x34)
s.add(st[0x0c]^st[0x10]^st[0x12]==0x66)
s.add(st[0x10]^st[0x14]^st[0x16]==0x04)
s.add(st[0x14]^st[0x18]^st[0x1a]==0x36)
s.add(st[0x18]^st[0x1c]^st[0x1e]==0x76)
s.add(st[0x1c]^st[0x20]^st[0x22]==0x3b)
s.add(st[0x01]^st[0x05]^st[0x07]==0x6a)
s.add(st[0x05]^st[0x09]^st[0x0b]==0x31)
s.add(st[0x09]^st[0x0d]^st[0x0f]==0x2e)
s.add(st[0x0d]^st[0x11]^st[0x13]==0x5e)
s.add(st[0x11]^st[0x15]^st[0x17]==0x0a)
s.add(st[0x15]^st[0x19]^st[0x1b]==0x33)
s.add(st[0x19]^st[0x1d]^st[0x1f]==0x06)
s.add(st[0x1d]^st[0x21]^st[0x23]==0x40)

print(s.check())
model = s.model()
flag = ''.join([chr(int(str(model[st[i]]))) for i in range(len(model))])
print(flag)