Last active
August 27, 2017 09:18
-
-
Save techvoltage/e9bed41fad937d156383449cd6bbdd45 to your computer and use it in GitHub Desktop.
50 point reversing challenge from HackCon-2017(https://ctftime.org/task/4476). Uses Python z3.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import string | |
| import random | |
| from z3 import * | |
| import socket | |
| def netcat(hostname, port, content): | |
| s = socket.socket(socket.AF_INET, socket.SOCK_STREAM) | |
| s.connect((hostname, port)) | |
| s.sendall(content) | |
| s.shutdown(socket.SHUT_WR) | |
| while 1: | |
| data = s.recv(1024) | |
| if data == "": | |
| break | |
| print "Received:", repr(data) | |
| print "Connection closed." | |
| s.close() | |
| # Return the first "M" models of formula list of formulas F | |
| # https://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation | |
| def get_models(s, M,password): | |
| result = [] | |
| #s = Solver() | |
| #s.add(F) | |
| p=[] | |
| while len(result) < M and s.check() == sat: | |
| m = s.model() | |
| k=''.join(hex(m[i].as_long()) for i in password if m[i] is not None) | |
| q = k.replace("0x", "") | |
| print q | |
| p.append(q+"\n") | |
| result.append(m) | |
| # Create a new constraint the blocks the current model | |
| block = [] | |
| for d in m: | |
| # d is a declaration | |
| if d.arity() > 0: | |
| raise Z3Exception("uninterpreted functions are not supported") | |
| # create a constant from declaration | |
| c = d() | |
| if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT: | |
| raise Z3Exception("arrays and uninterpreted sorts are not supported") | |
| block.append(c != m[d]) | |
| s.add(Or(block)) | |
| #return result | |
| p=''.join(p) | |
| return p | |
| def verify(l,s): | |
| str_="firhfgferfibbqlkdfhh" | |
| for x in xrange(0,len(l)): | |
| rcx=l[x] | |
| #print l[x],"-0x54 = ",hex(rcx-0x54) | |
| diff=rcx-0x54 | |
| #s.add(diff==0x5) | |
| p_bar=((diff * 0x4ec4ec4f)/0xffffffff) | |
| #p_bar=((diff * 79)/255) | |
| #s.add(p_bar==9) | |
| q_bar=diff | |
| #s.add(Or(p_bar<=20)) | |
| #print "(",diff," * 0x4ec4ec4f)/0xffffffff)",p_bar | |
| #print "(",diff," * 79)/255)",p_bar | |
| p=p_bar>>0x3 | |
| q=q_bar>>0x1f | |
| res=diff-((p-q) * 0x1a) +0x61 | |
| s.add(res==ord(str_[x])) | |
| s.add(l[x]<0xff) | |
| s = Solver() | |
| str_="firhfgferfibbqlkdfhh" | |
| password = [BitVec('b%d' % i, 40) for i in range(20)] | |
| verify(password,s) | |
| #print str(s) | |
| #print f.sexpr() | |
| #print s.check() | |
| p=get_models(s, 10,password) | |
| #result=get_models(s, 10,password) | |
| #print p | |
| netcat("defcon.org.in",8083,p) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment