Skip to content

Instantly share code, notes, and snippets.

@ianklatzco
Created April 22, 2019 09:28
Show Gist options
  • Save ianklatzco/5b1e6589371ff29852f0737749139fcc to your computer and use it in GitHub Desktop.
Save ianklatzco/5b1e6589371ff29852f0737749139fcc to your computer and use it in GitHub Desktop.
crappy dbi for asisctf
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;
}
#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");
}
}
}
# 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)
#!/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))
; 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