ECSC 2019 - Frankenstein

description: WGRAEHAAAAHAAHAHDAZHDAAHEAZHEHAZEHAZEAHAZ

category: reverse - 288

ecsc_frankenstein.png

An ELF64 file is attached to the description:

Using IDA, you can find the first part of this challenge:

ecsc_frankenstein_check.png

Let’s see the check_constraints function (This is the IDA pseudocode):

__int64 __fastcall check_constraints(__int64 a1)
{
  int i; // [rsp+14h] [rbp-Ch]
  unsigned int v3; // [rsp+18h] [rbp-8h]
  int v4; // [rsp+1Ch] [rbp-4h]

  v3 = 1;
  v4 = strlen((const char *)a1);
  if ( v4 != 11 )
    v3 = 0;
  for ( i = 0; i < v4; ++i )
  {
    if ( *(_BYTE *)(i + a1) <= 64 || *(_BYTE *)(i + a1) > 90 )
    {
      v3 = 0;
      break;
    }
  }
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 2) >> 4) ^ (unsigned __int8)(*(_BYTE *)(a1 + 6) >> 3)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 8) >> 4) ^ (unsigned __int8)(*(_BYTE *)(a1 + 8) >> 3)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 4) >> 4) ^ (unsigned __int8)(*(_BYTE *)(a1 + 6) >> 4)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 4) >> 2) ^ (unsigned __int8)(*(_BYTE *)(a1 + 9) >> 1)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)a1 >> 1) ^ (unsigned __int8)(*(_BYTE *)(a1 + 7) >> 1)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 1) >> 4) ^ (unsigned __int8)(*(_BYTE *)(a1 + 9) >> 3)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 3) >> 2) ^ (unsigned __int8)(*(_BYTE *)(a1 + 10) >> 1)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 3) >> 2) ^ *(_BYTE *)(a1 + 10)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 1) >> 2) ^ (unsigned __int8)(*(_BYTE *)(a1 + 8) >> 2)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 1) >> 1) ^ (unsigned __int8)(*(_BYTE *)(a1 + 5) >> 3)) & 1 )
    v3 = 0;
  if ( (*(_BYTE *)(a1 + 1) ^ (unsigned __int8)(*(_BYTE *)(a1 + 10) >> 3)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 6) >> 4) ^ (unsigned __int8)(*(_BYTE *)(a1 + 10) >> 2)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 6) >> 3) ^ (unsigned __int8)(*(_BYTE *)(a1 + 10) >> 4)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 2) >> 2) ^ *(_BYTE *)(a1 + 8)) & 1 )
    v3 = 0;
  if ( (*(_BYTE *)(a1 + 5) ^ (unsigned __int8)(*(_BYTE *)(a1 + 8) >> 4)) & 1 )
    v3 = 0;
  if ( (*(_BYTE *)(a1 + 5) ^ (unsigned __int8)(*(_BYTE *)(a1 + 9) >> 4)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 3) >> 3) ^ (unsigned __int8)(*(_BYTE *)(a1 + 6) >> 4)) & 1 )
    v3 = 0;
  if ( ((unsigned __int8)(*(_BYTE *)(a1 + 7) >> 2) ^ (unsigned __int8)(*(_BYTE *)(a1 + 10) >> 2)) & 1 )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 8) >> 4) ^ (unsigned __int8)(*(_BYTE *)(a1 + 10) >> 3)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)a1 >> 2) ^ (unsigned __int8)(*(_BYTE *)(a1 + 1) >> 2)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)a1 >> 1) ^ (unsigned __int8)(*(_BYTE *)(a1 + 8) >> 4)) & 1) )
    v3 = 0;
  if ( !((*(_BYTE *)(a1 + 3) ^ (unsigned __int8)(*(_BYTE *)(a1 + 8) >> 4)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 1) >> 4) ^ *(_BYTE *)(a1 + 6)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 1) >> 3) ^ (unsigned __int8)(*(_BYTE *)(a1 + 7) >> 4)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 1) >> 3) ^ *(_BYTE *)(a1 + 3)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 5) >> 2) ^ (unsigned __int8)(*(_BYTE *)(a1 + 7) >> 3)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 1) >> 2) ^ *(_BYTE *)(a1 + 2)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 3) >> 4) ^ (unsigned __int8)(*(_BYTE *)(a1 + 4) >> 3)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 6) >> 2) ^ (unsigned __int8)(*(_BYTE *)(a1 + 9) >> 1)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 2) >> 1) ^ (unsigned __int8)(*(_BYTE *)(a1 + 3) >> 2)) & 1) )
    v3 = 0;
  if ( !((*(_BYTE *)(a1 + 2) ^ (unsigned __int8)(*(_BYTE *)(a1 + 3) >> 4)) & 1) )
    v3 = 0;
  if ( !((*(_BYTE *)(a1 + 1) ^ (unsigned __int8)(*(_BYTE *)(a1 + 2) >> 1)) & 1) )
    v3 = 0;
  if ( !((*(_BYTE *)(a1 + 1) ^ *(_BYTE *)(a1 + 5)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 7) >> 3) ^ (unsigned __int8)(*(_BYTE *)(a1 + 10) >> 1)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 7) >> 2) ^ (unsigned __int8)(*(_BYTE *)(a1 + 7) >> 1)) & 1) )
    v3 = 0;
  if ( !(((unsigned __int8)(*(_BYTE *)(a1 + 4) >> 2) ^ (unsigned __int8)(*(_BYTE *)(a1 + 6) >> 4)) & 1) )
    v3 = 0;
  return v3;
}

Considering the first if condition and the first for loop, we can guess that our entry is 11 uppercase letters. Then our entry has to validate some conditions. We can use z3:

from z3 import *

s = Solver()

param_0 = BitVec('param_0', 8)
param_1 = BitVec('param_1', 8)
param_2 = BitVec('param_2', 8)
param_3 = BitVec('param_3', 8)
param_4 = BitVec('param_4', 8)
param_5 = BitVec('param_5', 8)
param_6 = BitVec('param_6', 8)
param_7 = BitVec('param_7', 8)
param_8 = BitVec('param_8', 8)
param_9 = BitVec('param_9', 8)
param_10 = BitVec('param_10', 8)

s.add(param_0 >= 65)
s.add(param_0 <= 90)
s.add(param_1 >= 65)
s.add(param_1 <= 90)
s.add(param_2 >= 65)
s.add(param_2 <= 90)
s.add(param_3 >= 65)
s.add(param_3 <= 90)
s.add(param_4 >= 65)
s.add(param_4 <= 90)
s.add(param_5 >= 65)
s.add(param_5 <= 90)
s.add(param_6 >= 65)
s.add(param_6 <= 90)
s.add(param_7 >= 65)
s.add(param_7 <= 90)
s.add(param_8 >= 65)
s.add(param_8 <= 90)
s.add(param_9 >= 65)
s.add(param_9 <= 90)
s.add(param_10 >= 65)
s.add(param_10 <= 90)

s.add(((param_6 >> 3 ^ param_2 >> 4) & 1) == 0)
s.add(((param_8 >> 3 ^ param_8 >> 4) & 1) == 0)
s.add(((param_6 ^ param_4) >> 4 & 1) == 0)
s.add(((param_9 >> 1 ^ param_4 >> 2) & 1) == 0)
s.add(((param_7 ^ param_0) >> 1 & 1) == 0)
s.add(((param_9 >> 3 ^ param_1 >> 4) & 1) == 0)
s.add(((param_10 >> 1 ^ param_3 >> 2) & 1) == 0)
s.add(((param_10 ^ param_3 >> 2) & 1) == 0)
s.add(((param_8 ^ param_1) >> 2 & 1) == 0)
s.add(((param_5 >> 3 ^ param_1 >> 1) & 1) == 0)
s.add(((param_10 >> 3 ^ param_1) & 1) == 0)
s.add(((param_10 >> 2 ^ param_6 >> 4) & 1) == 0)
s.add(((param_10 >> 4 ^ param_6 >> 3) & 1) == 0)
s.add(((param_8 ^ param_2 >> 2) & 1) == 0)
s.add(((param_8 >> 4 ^ param_5) & 1) == 0)
s.add(((param_9 >> 4 ^ param_5) & 1) == 0)
s.add(((param_6 >> 4 ^ param_3 >> 3) & 1) == 0)
s.add(((param_10 ^ param_7) >> 2 & 1) == 0)
s.add(((param_10 >> 3 ^ param_8 >> 4) & 1) != 0)
s.add(((param_1 ^ param_0) >> 2 & 1) != 0)
s.add(((param_8 >> 4 ^ param_0 >> 1) & 1) != 0)
s.add(((param_8 >> 4 ^ param_3) & 1) != 0)
s.add(((param_6 ^ param_1 >> 4) & 1) != 0)
s.add(((param_7 >> 4 ^ param_1 >> 3) & 1) != 0)
s.add(((param_3 ^ param_1 >> 3) & 1) != 0)
s.add(((param_7 >> 3 ^ param_5 >> 2) & 1) != 0)
s.add(((param_2 ^ param_1 >> 2) & 1) != 0)
s.add(((param_4 >> 3 ^ param_3 >> 4) & 1) != 0)
s.add(((param_9 >> 1 ^ param_6 >> 2) & 1) != 0)
s.add(((param_3 >> 2 ^ param_2 >> 1) & 1) != 0)
s.add(((param_3 >> 4 ^ param_2) & 1) != 0)
s.add(((param_2 >> 1 ^ param_1) & 1) != 0)
s.add(((param_5 ^ param_1) & 1) != 0)
s.add(((param_10 >> 1 ^ param_7 >> 3) & 1) != 0)
s.add(((param_7 >> 1 ^ param_7 >> 2) & 1) != 0)
s.add(((param_6 >> 4 ^ param_4 >> 2) & 1) != 0)

while s.check() == sat:
	result = str(s.model()) + '\n'

	string = 'param_0 = '
	length = len(string)
	var0 = result[result.find(string) + length: result.find(string) + length + result[result.find(string) + length:].find('\n') - 1]

	string = 'param_1 = '
	length = len(string)
	var1 = result[result.find(string) + length: result.find(string) + length + result[result.find(string) + length:].find('\n') - 1]

	string = 'param_2 = '
	length = len(string)
	var2 = result[result.find(string) + length: result.find(string) + length + result[result.find(string) + length:].find('\n') - 1]

	string = 'param_3 = '
	length = len(string)
	var3 = result[result.find(string) + length: result.find(string) + length + result[result.find(string) + length:].find('\n') - 1]

	string = 'param_4 = '
	length = len(string)
	var4 = result[result.find(string) + length: result.find(string) + length + result[result.find(string) + length:].find('\n') - 1]

	string = 'param_5 = '
	length = len(string)
	var5 = result[result.find(string) + length: result.find(string) + length + result[result.find(string) + length:].find('\n') - 1]

	string = 'param_6 = '
	length = len(string)
	var6 = result[result.find(string) + length: result.find(string) + length + result[result.find(string) + length:].find('\n') - 1]

	string = 'param_7 = '
	length = len(string)
	var7 = result[result.find(string) + length: result.find(string) + length + result[result.find(string) + length:].find('\n') - 1]

	string = 'param_8 = '
	length = len(string)
	var8 = result[result.find(string) + length: result.find(string) + length + result[result.find(string) + length:].find('\n') - 1]

	string = 'param_9 = '
	length = len(string)
	var9 = result[result.find(string) + length: result.find(string) + length + result[result.find(string) + length:].find('\n') - 1]

	string = 'param_10 = '
	length = len(string)
	var10 = result[result.find(string) + length: result.find(string) + length + result[result.find(string) + length:].find('\n') - 1]

	print chr(int(var0)) + chr(int(var1)) + chr(int(var2)) + chr(int(var3)) + chr(int(var4)) + chr(int(var5)) + chr(int(var6)) + chr(int(var7)) + chr(int(var8)) + chr(int(var9)) + chr(int(var10))

	s.add(Or(
		param_0 != s.model()[param_0],
		param_1 != s.model()[param_1],
		param_2 != s.model()[param_2],
		param_3 != s.model()[param_3],
		param_4 != s.model()[param_4],
		param_5 != s.model()[param_5],
		param_6 != s.model()[param_6],
		param_7 != s.model()[param_7],
		param_8 != s.model()[param_8],
		param_9 != s.model()[param_9],
		param_10 != s.model()[param_10]
		))

This is the output:

# python script.py 
DXCHXATLXXD
CGLWGNCSGCK
EZOJZITLYYD
EZOJZYTLYYD
MZOJZYTLYYD
[...]
MZGJZITLYXD
MZGJZIVLYXD
MZGHZITLYXD
EZGHZITLYXD
EZGJZITLYXD
[...]

It seems that there is a lot of solutions…

Well, let’s see the second part of the program:

[...]
draw_input((__int64)v7, (__int64)v8);
print_grid(v8);
for ( j = 0; j <= 4; ++j )
	gol_step((__int64)v8);
ptr = malloc(0x2711uLL);
convert_grid_to_string((__int64)v8, (__int64)ptr);
if ( (unsigned int)validate(ptr) )
{
	puts("WGRAEHAAAAHAAHAHDAZHDAAHEAZHEHAZEHAZEAHAZ");
	printf("GG ! You can validate with ECSC %s :D\n", *(_QWORD *)(v4 + 8));
}
else
{
	puts("Nah it was just an impression...");
}
[...]

I won’t present every function, but in summary, draw_input is creating a grid with our entry (presented later), gol_step is modifying the grid (called 5 times (0 to 4)) and validate is comparing the resulting grid to a stored grid.

We need to see the gol_step and the validate functions:

__int64 __fastcall gol_step(__int64 a1)
{
  unsigned int i; // [rsp+1Ch] [rbp-14h]
  unsigned int j; // [rsp+20h] [rbp-10h]
  int v4; // [rsp+24h] [rbp-Ch]
  __int64 v5; // [rsp+28h] [rbp-8h]

  v5 = copy_grid(a1);
  for ( i = 0; i <= 0x27; ++i )
  {
    for ( j = 0; j <= 0xF9; ++j )
    {
      v4 = get_n_alive_neighbors(v5, i, j);
      if ( v4 == 3 )
      {
        *(_BYTE *)(*(_QWORD *)(8LL * i + a1) + j) = 1;
      }
      else if ( v4 != 2 )
      {
        *(_BYTE *)(*(_QWORD *)(8LL * i + a1) + j) = 0;
      }
    }
  }
  return free_grid(v5);
}


__int64 __fastcall validate(__int64 a1)
{
  signed int i; // [rsp+10h] [rbp-8h]
  unsigned int v3; // [rsp+14h] [rbp-4h]

  v3 = 1;
  for ( i = 0; i <= 9999; ++i )
  {
    if ( *(_BYTE *)(i + a1) != answer[i] )
      return 0;
  }
  return v3;
}

As you can see gol_step looks like a Conway’s Game of Life

Now lets print the answer grid:

"""
Usage: gdb -q -x grid.py
"""

my_efl_file="./frankenstein"
 
gdb.execute("file " + my_efl_file)
gdb.execute("set confirm off")
gdb.execute("set pagination off")
gdb.execute("set non-stop on")
gdb.execute("set breakpoint pending on")
gdb.execute("set print pretty off")

i = 0
res = ""

gdb.Breakpoint("* validate+0x39")

try:
	gdb.execute("run UJCHXIWMXUD")
	frame = gdb.selected_frame()
	"""
	if str(frame.unwind_stop_reason()) == "0":
		gdb.execute("d")
		gdb.execute("watch $rdx == 0xf0b")
		gdb.execute("c")
	if str(frame.unwind_stop_reason()) == "0":
		gdb.execute("d")
		gdb.Breakpoint("* validate+0x39")
		gdb.execute("c")
	"""
	while True:
		if i%250 == 0:
			print(str(i))
			res += "\n" 
		if str(frame.unwind_stop_reason()) == "0":
			cl = str(frame.read_register("cl"))
			al = str(frame.read_register("al"))
			gdb.execute("set $al=" + cl)
			if al == "0x1":
				res += "#"
			else:
				res += "-"
			i += 1
			gdb.execute("c")
except:
	pass

print(res)

This is our grid (I deleted empty lines and for beauty):

----------------------------------------------------------------------------
---------------------##-------------------------------#---------------------
----##-----##------##-##---------#------------##------#----###-----##-------
---#-#---#---#-----##--#-----------------##---##----------####-----##-------
----#---#-----#-----#----#---#-#--------#-#---------------#-#--#-------##---
-------#------#---#----------#-#-------#-##-------###------#----##----##----
------#-------#-----#-------------------#-#--------##----#--#-#--#---#-##---
-----#-##----#-----##-#------------------##---##----###--##-#-#---##-##-----
-----##----##------##-#---###-----------------##-----##----##-#---#--#------
---------------------#----##--------------------------#-----###----###------
--------------------------#-------------------------------------------------
----------------------------------------------------------------------------

I decided to code the algorithm in python and try to bruteforce the entry by pattern recognition. For example, I’ll try to test all possibilities of the first 2 chars and compare it to the answer grid (we want the fish):

import copy
from itertools import product

charset = "ABCDEFGHIJKLMNOPQRSTUVWXYZ"

loads = product(charset, repeat=2)

letter = []
letter.append("0111001100011100110001110011100111001010011100111001010010000101001001011100111001110011100111001110010100101010001010100101001110")
letter.append("0101001010010000101001000010000100001010001000010001010010000111001101010100101001010010100100000100010100101010001010100101000010")
letter.append("0111001100010000101001110011100101001110001000010001100010000101001011010100111001010011100111000100010100101010101001000111000100")
letter.append("0101001010010000101001000010000101001010001000010001010010000101001001010100100001010010100001000100010100101011011010100010001000")
letter.append("0101001100011100110001110010000111001010011100110001010011100101001001011100100001111010010111000100011100010010001010100010001010")

for payload in loads:
	#payload = "SE" + "".join(pay)
	print payload

	tab = []

	for i in range(40*250):
		tab.append(0)

	number = 0

	v7 = 90
	for myId in range(len(payload)):
		v7 += 2
		for i in range(5):
			for j in range(5):
				tab[(17*250) + i*250 + v7 + j] = int(letter[i][j + (ord(payload[myId])-65)*5])
		v7 += 5

	for i in range(5):
		tmp = copy.deepcopy(tab)

		for i in range(30*250):
			val = tab[i-251] + tab[i-250] + tab[i-249] + tab[i-1] + tab[i+1] + tab[i+249] + tab[i+250] + tab[i+251]
			if val == 3:
				tmp[i] = 1
			elif val != 2:
				tmp[i] = 0

		for i in range(40*250):
			tab[i] = tmp[i]

	draw = ""
	for i in range(10*250,25*250):
		if i%250 == 0:
			draw += '\n'
		if tab[i]:
			draw += '#'
		else:
			draw += '-'

	print draw
	raw_input(payload)

And the output:

-----------------
-----------------
-----------------
-----------------
-----------------
-----#------#----
-----#------#----
-----------------
-----------------
-----------------
--------##-------
--------##-------
-----------------
-----------------
-----------------
('A', 'A')

-----------------
-----------------
-----------------
-----------------
-----------------
-----#-----------
-----#-----------
------------##---
------------###--
-------#-##---##-
--------#---###--
------------##---
-----------------
-----------------
-----------------
('A', 'B')
[...]
-----------------
-----------------
-----------------
-----------------
-----------------
-----------------
----##-----##----
---#-#---#---#---
----#---#-----#--
-------#------#--
------#-------#--
-----#-##----#---
-----##----##----
-----------------
-----------------
('S', 'E')

Okay seems like the first letters are ‘SE’.

We can now modify our z3 script and add these conditions:

[...]
s.add(param_0 == 83)
s.add(param_1 == 69)
[...]

Then you can bruteforce the 3rd and the 4th char. You can select every couple of 3rd and 4th char from the z3 script (should not have lots of possibilities).

Keeping doing this, we finally find the good entry:

# ./frankenstein SEDWFDCRGGK
Wait !? Is it moving !?
-------------------------------------------------------------------------------
---###----###----##----#---#---###----##-----###----###----###----###----#-#---
---#------#------#-#---#---#---#------#-#----#------#-#----#------#------#-#---
---###----###----#-#---#-#-#---###----#-#----#------###----#-#----#-#----##----
-----#----#------#-#---##-##---#------#-#----#------#-#----#-#----#-#----#-#---
---###----###----##----#---#---#------##-----###----#--#---###----###----#-#---
-------------------------------------------------------------------------------
WGRAEHAAAAHAAHAHDAZHDAAHEAZHEHAZEHAZEAHAZ
GG ! You can validate with ECSC{SEDWFDCRGGK} :D

Yeah ! the flag is ECSC{SEDWFDCRGGK}