Created
April 22, 2019 09:28
-
-
Save ianklatzco/5b1e6589371ff29852f0737749139fcc to your computer and use it in GitHub Desktop.
crappy dbi for asisctf
This file contains 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
undefined8 check_secret_id(char *user_input) | |
{ | |
int iVar1; | |
int iVar2; | |
int user_input_(int); | |
long lVar3; | |
size_t sVar4; | |
size_t sVar5; | |
size_t sVar6; | |
int bottom_four_numbers; | |
int all_but_the_bottom_five_numbers; | |
lVar3 = strtol(user_input,(char **)0x0,10); | |
user_input_(int) = (int)lVar3; | |
sVar4 = strlen(user_input); | |
if ((SUB168((ZEXT816(0) << 0x40 | ZEXT816((ulong)(long)user_input_(int))) % ZEXT816(sVar4 + 2),0) | |
== 0) && (user_input[4] == '1')) { | |
all_but_the_bottom_five_numbers = user_input_(int) / 100000; | |
// aka user_input[n]:user_input[5] | |
bottom_four_numbers = user_input_(int) % 10000; | |
if (((user_input[1] + user_input[3] * 10) - (( user_input[n:8] ) * 10 + user_input[5]) == 1 ) | |
// u[3] u[1] - 85 == 1 | |
// 12345678 | |
// 90618006 | |
// 69 68 | |
&& | |
(((user_input[7])) * 10 + user_input[6] + (user_input[2] + (user_input[1] * 10) * -2 == 8)) | |
( | |
76 + | |
( 2 + (1 * 10) * -2 == 8)) | |
// 7 + 8 == 8 // if == is higher prec, should return 8 | |
// if == is lower prec, should return 0 | |
(((all_but_the_bottom_five_numbers / 100) % 10) * 10 + | |
(all_but_the_bottom_five_numbers / 10) % 10 + | |
((bottom_four_numbers % 1000) / 100 + ((bottom_four_numbers % 100) / 10) * 10) * -2 == | |
8) | |
// 76 - 12*2 == 8 | |
{ | |
iVar1 = (all_but_the_bottom_five_numbers % 10) * 10 + (all_but_the_bottom_five_numbers / 100) % 10; | |
iVar2 = ((bottom_four_numbers / 100) % 10) * 10 + bottom_four_numbers % 10; | |
if ((iVar1 / iVar2 == 3) && (iVar1 % iVar2 == 0)) { | |
sVar4 = strlen(user_input); | |
sVar5 = strlen(user_input); | |
sVar6 = strlen(user_input); | |
if ((long)(user_input_(int) % (all_but_the_bottom_five_numbers * bottom_four_numbers)) == | |
(sVar6 + 2) * (sVar4 + 2) * (sVar5 + 2) + 6) { | |
return 1; | |
} | |
} | |
} | |
} | |
return 0; | |
} | |
This file contains 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
#include <stdio.h> | |
#include <stdint.h> | |
#include <sys/mman.h> | |
#include <errno.h> | |
#include <sys/types.h> | |
#include <sys/stat.h> | |
#include <fcntl.h> | |
#include <string.h> | |
#include <stdlib.h> | |
#include <signal.h> | |
// This is a C harness that runs a patched ASM function that was taken from the | |
// binary, `silkroad.elf`. | |
// The patched function accepts a string of integers (max len 9) via rdi. | |
// It runs against a few constraints (roughly, each basic block in `bin`). | |
// If it fails any check, it returns back to the C handler. | |
// If it passes (reaches the call to puts), it exits, printing the correct | |
// number. | |
// I pulled it out of r2 using one of the pc? | |
// I have provided a statically compiled binary, `iterate`. | |
// This harness has an underlying challenge: every recompile, you'll need to | |
// update addresses to lib functions in the file `bin`. | |
// Specifically, the first 0x200 bytes have a few jmps to required lib functions. | |
// I wonder if I could've just inline asm'd the whole thing instead of mmap'ing | |
// a bin.... would've probably required a syntax transfer. | |
// Load some functions we'll want easy access to. | |
// I grabbed their addresses by disas'ing whatever in gdb, then using r2 to | |
// write the addresses to jmp to. | |
int whatever() | |
{ | |
char h[] = "hello\0"; | |
strtol((char *)-1, 0, 10); | |
int c = strcmp(h,h); | |
puts(h); | |
return strlen(h) + c; | |
} | |
int main() | |
{ | |
signal(SIGFPE, SIG_IGN); // Attempt to suppress divide by 0 exceptions. | |
// This worked for the first one, but I think ran into issues after there was | |
// more than one. | |
char arr[10] = {0}; | |
// File containing the "borrowed" function that we want to instrument. | |
int f = open("bin", O_RDONLY); | |
// mmap it into memory. It won't get loaded at 0x401000 (staticly compiled). | |
void* new_region = mmap((int*)0x00401000, 1000, PROT_READ | PROT_WRITE | | |
PROT_EXEC, MAP_PRIVATE, f, 0); | |
if (new_region == (int*)-1) | |
{ | |
printf("%d", errno); | |
exit(69); | |
} | |
int ret; | |
// Mark it as writeable/executable. Not necessary. | |
ret = mprotect((int*)0x00400000, 0x1000, PROT_READ | PROT_WRITE | PROT_EXEC); | |
if (ret == -1) | |
{ | |
printf("mprotect 2 failed: errno %d", errno); | |
exit(69); | |
} | |
// Iterate through possible values, including with variable amounts of | |
// leading zeroes. Obtained by reversing the function w/ Ghidra. | |
// Thanks, Kyle. | |
// The most significant number is at the higher index of the string. | |
// 0 1 2 3 4 5 6 7 8 9 | |
// totlen: [5,9]. Used to 0 pad the front of the string. | |
for (int totlen=5; totlen <10; totlen++) { | |
// Fill string w 0s. | |
for (int j = 0; j < totlen; j++) { | |
arr[j] = 0x30; | |
} | |
int ind_non_nine = -1; | |
while (1) { | |
// From the highest index to the lowest, find the first non-nine. | |
ind_non_nine = -1; | |
for (int i = totlen-1; i>=0; i--) | |
{ | |
if (arr[i] != 0x39) | |
{ | |
ind_non_nine = i; | |
break; | |
} | |
} | |
// If all nines, break to add a digit on the left. | |
if (ind_non_nine == -1) {break;} | |
// If you need to carry, carry. | |
// 00009 -> 00000 | |
for (int i = totlen-1; i > ind_non_nine; i--) { | |
arr[i] = 0x30; | |
} | |
arr[ind_non_nine]++; | |
// At this point you have a new number. | |
// Time to throw it into the instrumented code. | |
// avoid div by 0 cases. | |
if ( arr[totlen-3] == '0' && arr[totlen-1] == '0') | |
{ | |
continue; | |
} | |
// nops to make it easier to find the address of this in gdb. | |
asm("nop"); asm("nop"); asm("nop"); | |
// Transfer control flow to the ASM. | |
// RDI needs to contain the buffer | |
asm( | |
"lea %0, %%rdi \n\t" | |
"call %1" | |
:"=m"(arr) // hm, it's =m instead of =r. | |
:"r"(new_region+0x40a) | |
); | |
asm("nop"); asm("nop"); asm("nop"); | |
} | |
} | |
} | |
This file contains 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
# first attempt at using z3 to just get to a partic address. | |
# result: angr says it can't find the thing. | |
# next: try expressing everything in z3's SMT language. basically what we did with python, but use a constraint solver instead of brute force. | |
import angr | |
import sys | |
def main(argv): | |
# Create an Angr project. | |
path_to_binary = 'silkroad.elf' # :string | |
project = angr.Project(path_to_binary, auto_load_libs=False) | |
# Tell Angr where to start executing (should it start from the main() | |
# function or somewhere else?) For now, use the entry_state function | |
# to instruct Angr to start from the main() function. | |
initial_state = project.factory.entry_state() # entry_state means main | |
# Create a simulation manager initialized with the starting state. It provides | |
# a number of useful tools to search and execute the binary. | |
simulation = project.factory.simgr(initial_state) | |
# addr of code that prints the thing we want | |
print_good_address = 0x401aaf | |
simulation.explore(find=print_good_address) | |
# this will return a list of states that might be correct that get us to that eip | |
# Check that we have found a solution. The simulation.explore() method will | |
# set simulation.found to a list of the states that it could find that reach | |
# the instruction we asked it to search for. Remember, in Python, if a list | |
# is empty, it will be evaluated as false, otherwise true. | |
if simulation.found: | |
# The explore method stops after it finds a single state that arrives at the | |
# target address. | |
solution_state = simulation.found[0] | |
# Print the string that Angr wrote to stdin to follow solution_state. This | |
# is our solution. | |
print solution_state.posix.dumps(sys.stdin.fileno()) | |
else: | |
# If Angr could not find a path that reaches print_good_address, throw an | |
# error. Perhaps you mistyped the print_good_address? | |
raise Exception('Could not find the solution') | |
if __name__ == '__main__': | |
main(sys.argv) |
This file contains 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
#!/usr/bin/python3 | |
import random, sys, signal | |
import logging | |
from logging import * | |
import multiprocessing | |
basicConfig(level=DEBUG) | |
# I wrote this first, but got really confused with accessing various base10 digits of an int. | |
# So I wrote a C harness instead, iterate.c. | |
# this script doesn't test cases where there's leading 0s. | |
# as it turns out, that dousn't matter; tho i did find an interesting case that segfaults the binary. | |
# all of the checks that index, index from the rightmost side. | |
# eg: 790317143: check_2 asks for u[31]. | |
# that is, ^ ^ | |
# in: [Int] | |
# out: Bool | |
def check_1( int_list = None, int_repr = None, strlen = None): | |
a = int_repr % (strlen + 2) | |
return a == 0 | |
def check_2(int_repr=None, int_list=None, strlen = None, str_repr=None): | |
# the fifth digit of the int from the right is '1'. (x0000) | |
# u[4] == 1. | |
# xxxx1xxxx | |
return int_list[4] == 1 | |
def check_3( int_list = None, int_repr = None, strlen = None, str_repr=None): | |
# u[31] - u[85] == 1. | |
l = int_list | |
a = l[3]*10 + l[1] # 31 | |
b = l[8]*10 + l[5] # 85 | |
c = a-b # 31 - 85 | |
return c == 1 | |
def check_4( int_list = None, int_repr = None, strlen = None ): | |
# u[76] + u[12] * -2 == 8 | |
a = int_list[7] * 10 + int_list[6] # 76 | |
b = int_list[1] * 10 + int_list[2] # 12 | |
b = b * 2 | |
c = a - b | |
return c == 8 | |
def check_5( int_list = None, int_repr = None, strlen = None ): | |
a = int_list[5] * 10 + int_list[7] # 57 | |
b = int_list[2] * 10 + int_list[0] # 20 | |
if b == 0: return False | |
return (a / b == 3) and (a % b == 0) | |
def check_6( int_list = None, int_repr = None, strlen = None): | |
top_numbers = int_repr // 100000 # // != / in py3. sigh. this caught me. | |
bottom_nums = int_repr % 10000 | |
a = int_repr % (top_numbers * bottom_nums) | |
b = strlen+2 | |
b = b*b*b +6 | |
return a == b | |
def worker(j): | |
# 0, 1 000 000 000 | |
# 1 000 000 001, 2 000 000 000 | |
# 2 000 000 001, 3 000 000 000 | |
# 3 000 000 001, 4 000 000 000 | |
# 4 000 000 001, 4 294 967 295 | |
li = [0,0,0,0,0,0,0,0,0,0] | |
# 9th position | |
for i9 in range(0,5): | |
for i7 in range(0,10): | |
for i6 in range(0,10): | |
for i3 in range(0,10): | |
for i2 in range(0,10): | |
for i1 in range(0,10): | |
for i0 in range(0,10): | |
if ( i3 == 0 and i1 == 0 ): | |
# catch an edge case where u[31] < u[85] results in a div by 0 | |
continue | |
li[9] = i9 | |
# i8 | |
li[7] = i7 | |
li[6] = i6 | |
# i5 | |
li[4] = 1 # check_2 | |
li[3] = i3 | |
li[2] = i2 | |
li[1] = i1 | |
li[0] = i0 | |
# li = [0 1 2 3 x * 6 7 * 9] < MSD | |
# encode check_3 to get factor of ~100 speedup | |
# 31 - 1 = 85 | |
eighty_five = (i3 * 10 + i1 - 1) | |
li[8] = eighty_five // 10 | |
li[5] = eighty_five % 10 | |
# li = li[::-1] | |
# 98765 4 3210 < c | |
# 01234 5 6789 < python | |
int_repr = li[9] * 1000000000 + \ | |
li[8] * 100000000 + \ | |
li[7] * 10000000 + \ | |
li[6] * 1000000 + \ | |
li[5] * 100000 + \ | |
li[4] * 10000 + \ | |
li[3] * 1000 + \ | |
li[2] * 100+ \ | |
li[1] * 10+ \ | |
li[0] | |
str_repr = str(int_repr) | |
strlen = len(str(int_repr)) | |
int_list = [ x for x in map(int, str(int_repr).zfill(9)[::-1] ) ] | |
if ( \ | |
check_1(int_repr=int_repr, strlen = strlen, int_list=int_list) and\ | |
check_4(int_repr=int_repr, strlen = strlen, int_list=int_list) and \ | |
check_5(int_repr=int_repr, strlen = strlen, int_list=int_list) and \ | |
check_6(int_repr=int_repr, strlen = strlen, int_list=int_list) \ | |
): | |
# check_3(int_repr=int_repr, strlen = strlen, int_list=int_list) and \ | |
# check_2(int_repr=int_repr, strlen = strlen, int_list=int_list) and \ | |
# Can be totally omitted because of how we wrote our loop. | |
print(li) | |
print(int_repr) | |
if __name__ == '__main__': | |
if (sys.version_info < (3,0)): | |
print("wrong python version, use 3") | |
sys.exit() | |
# jobs = [] | |
# for x in range(0,4): | |
# print("Starting process " + str(x)) | |
# p = multiprocessing.Process(target=worker, args=(x,)) | |
# jobs.append(p) | |
# p.start() | |
worker(0) # no need for multiprocess, optimized it well enough that it only takes a minute. | |
# 790317143 | |
# also found this one that is NOT a right answer: 08901000 but will SIGFPE the binary | |
def check_answer(int_repr): | |
str_repr = str(int_repr) | |
strlen = len(str(int_repr)) | |
int_list = [ x for x in map(int, str(int_repr)[::-1] ) ] | |
one = check_1(int_repr=int_repr, strlen = strlen, int_list=int_list) | |
print("check 1: " + str(one)) | |
two = check_2(int_repr=int_repr, strlen = strlen, int_list=int_list, str_repr=str_repr) | |
print("check 2: " + str(two)) | |
three = check_3(int_repr=int_repr, strlen = strlen, int_list=int_list, str_repr=str_repr) | |
print("check 3: " + str(three)) | |
four = check_4(int_repr=int_repr, strlen = strlen, int_list=int_list) | |
print("check 4: " + str(four)) | |
five = check_5(int_repr=int_repr, strlen = strlen, int_list=int_list) | |
print("check 5: " + str(five)) | |
six = check_6(int_repr=int_repr, strlen = strlen, int_list=int_list) | |
print("check 6: " + str(six)) | |
This file contains 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
; first attempt at z3 to solve this problem. | |
; this script does not work. | |
(declare-const a String) ; "1234" | |
(declare-const b Int) ; 1234 == 0x4d2 | |
; b must be positive | |
(assert (>= b 0)) | |
; b is int(a) | |
(assert (= (str.to.int a) b)) | |
; a must be <=10 | |
(assert (<= (str.len a) 10)) | |
; len(a) + 2 | |
(assert (= (+ (str.len a) 2) 12 )) | |
; a = i % (len(str(i)) + 2) # remainder | |
; return a == 0 | |
(assert | |
(= (mod b (+ (str.len a) 2)) 0) | |
) | |
; upon adding this check, z3 runs pretty much forever. | |
(check-sat) | |
(get-model) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment