mokhdzanifaeq

from z3 import *
from struct import pack

# define vars
LENGTH = 8
DEBUG = 0
Buf = [BitVec("%i" % i, 16) for i in range(LENGTH)]
solver = Solver()

solver.add(

mokhdzanifaeq

import requests

tmp = '0x'
flag = ''
length = 1

# get flag length
while True:
	r = requests.get('http://localhost/post.php?id=length(@bounty)-{}'.format(length - 1))
	if '1337' in r.content: break

mokhdzanifaeq

# pip install pycryptodome
from Crypto.Protocol.KDF import PBKDF2
from Crypto.Cipher import AES
from hashlib import sha256
from datetime import datetime
from ctypes import *
import multiprocessing as mp

# http://referencesource.microsoft.com/#mscorlib/system/random.cs
class Random(object):

mokhdzanifaeq

import os,sys
import requests
import re
import ast
import json
import time
from numpy.random import choice

loop = 102

mokhdzanifaeq

import re
import sys
import string
from z3 import *

# hackish way to generate string that satisfy simple regex
# what's not supported: group reference & look behind
# usage: python regex.py PATTERN LENGTH

pattern = sys.argv[1]

mokhdzanifaeq

from PIL import Image
import argparse
from collections import OrderedDict

def parseMask(string):
	mask = []
	for val in string.split(","):
		if "-" in val: 
			min, max = val.split("-")
			mask += [1 << (i - 1) for i in range(int(min), int(max) + 1)]

mokhdzanifaeq

// extracted from metasploit source code
// need to get hex stream of the buffer

VirtualKeyCodes = {
  1 => %W{ LClick },
  2 => %W{ RClick },
  3 => %W{ Cancel },
  4 => %W{ MClick },
  8 => %W{ Back  },
  9 => %W{ Tab  },

mokhdzanifaeq

# challenge4_ok.exe - https://drive.google.com/open?id=0B_bQeUUGe4uLcXNqRnBBand5Yk0

from z3 import *
import sys

# argv[1] == key length
length = int(sys.argv[1])
if length < 5:
    print "length must be more than 4!"
    exit()

mokhdzanifaeq

# challenge3 - https://drive.google.com/file/d/0B_bQeUUGe4uLM3BWd1dqTVF4TVE/view?usp=sharing

from z3 import *
import sys

# define the variables
chars = IntVector("", 7)
solver = Solver()
constraint = []

mokhdzanifaeq

from z3 import *
from random import shuffle

# define the variables
chars = IntVector("", 16)

solver = Solver()

# all values are printable chararacters (33 - 126)
for i in range(16):