# Ekoparty pre-challenges 2k16 - backdoor (50)

$ cat solver.py
from z3 import *

## Defining and initializing

flag = []
for i in range(18):
 flag.append(Int('v%.2d' % i))

s = Solver()

# Constraints

s.add(flag[0] == 69)
s.add(flag[1] == 75)
s.add(flag[1] + flag[2] == 154)
s.add(flag[2] + flag[3] == 202)
s.add(flag[3] + flag[4] == 241)
s.add(flag[4] + flag[5] == 233)
s.add(flag[5] + flag[6] == 217)
s.add(flag[6] + flag[7] == 218)
s.add(flag[7] + flag[8] == 228)
s.add(flag[8] + flag[9] == 212)
s.add(flag[9] + flag[10] == 195)
s.add(flag[10] + flag[11] == 195)
s.add(flag[11] + flag[12] == 201)
s.add(flag[12] + flag[13] == 207)
s.add(flag[13] + flag[14] == 203)
s.add(flag[14] + flag[15] == 215)
s.add(flag[15] + flag[16] == 235)
s.add(flag[16] + flag[17] == 242)

# Checking and printing

if s.check() == sat:
 m = s.model()
 #print m
 for v in m:
  print v, m[v]
  p = int(str(v)[1:])
  v = chr(int(str(m[v])))
  flag[p] = v

 print flag
 print ''.join(flag)

$ python solver.py
v17 125
v16 117
v15 118
v14 97
v13 106
v12 101
v11 100
v10 95
v09 100
v08 112
v07 116
v06 102
v05 115
v04 118
v03 123
v02 79
v01 75
v00 69
['E', 'K', 'O', '{', 'v', 's', 'f', 't', 'p', 'd', '_', 'd', 'e', 'j', 'a', 'v', 'u', '}']
EKO{vsftpd_dejavu}

Reference

http://jolmos.blogspot.com.es/2016/10/vsftpd-backdoor-ekoparty-prectf.html