Rating:
ELF crackme with 5 checks, it will immediately segfault if any check fails.
**check**
- check flag format, first 4 characters should be ENO{.
**cccheck**
- check 8 characters after flag format.
- the character range should be in one of this ranges A-Z 0-9 and \-\`.
- flag[i] xored with flag[i+14] and the sum of all 8 characters after xor should be 0x1F4.
- flag[i] xored with flag[i+14] and the multiplication of all characters after xor should be 0x3A49D503C4C0.
**ccheck**
- each flag characters from index-12 to index-23 xored with 0x13 and the result should be R]WL^aA|q#g
**ccccheck**
- check the last character of flag, should be }.
**cccccheck**
- crc32b(flag) should be 0x67123A46.
```
from z3 import *
LEN = 8
s = Solver()
v1 = [BitVec(i, 32) for i in range(LEN)]
MUL = 64088780817600
ADD = 500
CUR = 'ENO{!!!!!!!!AND_MrRob0t}'
add = 0
mul = 1
for i in range(LEN):
x = CUR[i + 15]
add += v1[i] ^ ord(x)
mul *= v1[i] ^ ord(x)
s.add(v1[0] >= ord('A'))
s.add(v1[0] <= ord('Z'))
s.add(v1[1] >= ord('0'))
s.add(v1[1] <= ord('9'))
s.add(v1[2] >= ord('A'))
s.add(v1[2] <= ord('Z'))
s.add(v1[3] >= ord('A'))
s.add(v1[3] <= ord('Z'))
s.add(v1[4] >= ord('0'))
s.add(v1[4] <= ord('9'))
s.add(v1[5] >= ord('A'))
s.add(v1[5] <= ord('Z'))
s.add(v1[6] >= ord('A'))
s.add(v1[6] <= ord('Z'))
s.add(v1[LEN -1] == 95)
s.add(add == ADD)
s.add(mul == MUL)
if s.check() == sat:
model = s.model()
flag = ''
for i in range(LEN):
flag += chr(model[v1[i]].as_long())
print(flag)
# found H4XL3NY_, with a little bit help from chat gpt by searching "hacker movie like mr robot" which pop hackers as one of the movie, after correction it become H4CK3RS_
```
