Clean and document some example/linux (#176)
* Clean arguments.c * Increase query timeout from 30 to 120 seconds * Example documentation updated * Add ibranch comments * crackme.py, ibranch, sindex and typos * indexhell * visitad typo * typo * strncmp example * Typos
This commit is contained in:
feliam
Dan Guido
@@ -3,13 +3,13 @@ CFLAGS=-O3 -static
|
||||
|
||||
all: CFLAGS=-O3 -static
|
||||
all: NOSTDLIBFLAGS=-m32 -fno-builtin -static -nostdlib -fomit-frame-pointer
|
||||
all: nostdlib basic sindex strncmp arguments ibranch sendmail cbahacks indexhell baby-re helloworld
|
||||
all: nostdlib basic sindex strncmp arguments ibranch sendmail crackme indexhell baby-re helloworld
|
||||
|
||||
arm: CC=arm-linux-gnueabi-gcc
|
||||
arm: basic sindex strncmp arguments ibranch sendmail cbahacks indexhell helloworld simple_copy
|
||||
arm: basic sindex strncmp arguments ibranch sendmail crackme indexhell helloworld simple_copy
|
||||
|
||||
clean:
|
||||
rm -rf nostdlib basic sindex strncmp arguments sendmail server ibranch cbahacks indexhell cbahacks.c simple_copy helloworld
|
||||
rm -rf nostdlib basic sindex strncmp arguments sendmail server ibranch crackme indexhell crackme.c simple_copy helloworld nostdlib32 nostdlib64
|
||||
|
||||
nostdlib: nostdlib.c
|
||||
$(CC) -m32 -fno-builtin -static -nostdlib -fomit-frame-pointer nostdlib.c -o nostdlib32
|
||||
@@ -25,6 +25,7 @@ basic: basic.c
|
||||
|
||||
sindex: sindex.c
|
||||
$(CC) $(CFLAGS) sindex.c -o sindex
|
||||
|
||||
ibranch: ibranch.c
|
||||
$(CC) $(CFLAGS) ibranch.c -o ibranch
|
||||
|
||||
@@ -40,13 +41,12 @@ sendmail: sendmail.c
|
||||
server: server.c
|
||||
gcc -static server.c -o server
|
||||
|
||||
|
||||
cbahacks: cbahacks.py
|
||||
python cbahacks.py >cbahacks.c
|
||||
gcc -static cbahacks.c -o cbahacks
|
||||
crackme: crackme.py
|
||||
python crackme.py >crackme.c
|
||||
gcc -static -Os crackme.c -o crackme
|
||||
|
||||
indexhell: indexhell.c
|
||||
gcc -static indexhell.c -o indexhell
|
||||
gcc -static indexhell.c -o indexhell
|
||||
|
||||
baby-re: baby-re.c
|
||||
$(CC) $(CFLAGS) -o $@ $< -Wno-unused-result
|
||||
|
||||
@@ -1,16 +1,57 @@
|
||||
/* Minimal toy example with input from argv
|
||||
*
|
||||
* The "special" character '+' marks symbolic bytes on the argyuments to the program.
|
||||
/* This program parses a commandline argument.
|
||||
*
|
||||
* Compile with :
|
||||
* $ gcc toy005-arguments.c -o toy005-arguments
|
||||
* $ gcc -static -Os arguments.c -o arguments
|
||||
*
|
||||
* Analyze it with:
|
||||
* $ manticore arguments ++++++++++
|
||||
*
|
||||
* - Note that the character + will be replaced by a symbolic byte
|
||||
* representing all possible bytes (except \x00)
|
||||
* The length of the argument is important as it wont allow \x00
|
||||
* in the middle of the argument
|
||||
*
|
||||
* Expected output:
|
||||
* $ manticore arguments +++++++++
|
||||
* 2017-04-21 17:12:01,241: [4783] MAIN:INFO: Loading program: ['arguments', '+++++++++']
|
||||
* 2017-04-21 17:12:01,242: [4783] MAIN:INFO: Workspace: ./mcore_dG3b5O
|
||||
* 2017-04-21 17:12:34,130: [4835][3] EXECUTOR:INFO: Generating testcase No. 1 for state No.3 - Program finished correctly
|
||||
* 2017-04-21 17:12:48,745: [4840][11] EXECUTOR:INFO: Generating testcase No. 2 for state No.11 - Program finished correctly
|
||||
* 2017-04-21 17:13:00,509: [4840][17] EXECUTOR:INFO: Generating testcase No. 3 for state No.17 - Program finished correctly
|
||||
* 2017-04-21 17:13:10,748: [4833][21] EXECUTOR:INFO: Generating testcase No. 4 for state No.21 - Program finished correctly
|
||||
* 2017-04-21 17:13:20,580: [4833][29] EXECUTOR:INFO: Generating testcase No. 5 for state No.29 - Program finished correctly
|
||||
* 2017-04-21 17:13:28,560: [4834][33] EXECUTOR:INFO: Generating testcase No. 6 for state No.33 - Program finished correctly
|
||||
* 2017-04-21 17:13:38,583: [4838][41] EXECUTOR:INFO: Generating testcase No. 7 for state No.41 - Program finished correctly
|
||||
* 2017-04-21 17:13:47,878: [4840][47] EXECUTOR:INFO: Generating testcase No. 8 for state No.47 - Program finished correctly
|
||||
* 2017-04-21 17:13:52,500: [4835][53] EXECUTOR:INFO: Generating testcase No. 9 for state No.53 - Program finished correctly
|
||||
* 2017-04-21 17:13:52,988: [4840][51] EXECUTOR:INFO: Generating testcase No. 10 for state No.51 - Program finished correctly
|
||||
*
|
||||
* Look at ./mcore_dG3b5O for results, you will find something like this:
|
||||
* command.sh #The original command line
|
||||
* test_00000001.messages #A txt file with cpu and memory state
|
||||
* test_00000001.smt #The smtlib description of the path constraint leading here
|
||||
* test_00000001.stderr #stderr output of the program
|
||||
* test_00000001.stdin #stdin an example stdin input
|
||||
* test_00000001.stdout #stdout output of the program
|
||||
* test_00000001.syscalls #The trace of IO syscalls
|
||||
* test_00000001.trace #The list of visited instructions
|
||||
* test_00000001.txt #A solution to all symbolic variables used. (Includes ARGV/ENVP)
|
||||
*
|
||||
* $ cat t*txt |grep ARGV
|
||||
* ARGV1_1: '\x01\x01\x01\x01\x01\x01\x01\x01\x01'
|
||||
* ARGV1_1: '-\x01\x01\x01\x01\x01\x01\x01\x01'
|
||||
* ARGV1_1: '--\x01\x01\x01\x01\x01\x01\x01'
|
||||
* ARGV1_1: '--d\x01\x01\x01\x01\x01\x01'
|
||||
* ARGV1_1: '--do\x01\x01\x01\x01\x01'
|
||||
* ARGV1_1: '--dos\x01\x01\x01\x01'
|
||||
* ARGV1_1: '--dost\x01\x01\x01'
|
||||
* ARGV1_1: '--dostu\x01\x01'
|
||||
* ARGV1_1: '--dostuff'
|
||||
* ARGV1_1: '--dostuf\x01'
|
||||
*
|
||||
* Analize it with:
|
||||
* $ python system.py example/toy005-arguments ++++++++++
|
||||
*/
|
||||
|
||||
#include <stdio.h>
|
||||
#include <stdlib.h>
|
||||
#include <string.h>
|
||||
|
||||
|
||||
|
||||
@@ -4,7 +4,7 @@
|
||||
* Note: Challenge was ported to use read(2) instead of scanf(3)
|
||||
*
|
||||
* To run:
|
||||
* $ python main.py baby-re
|
||||
* $ manticore baby-re
|
||||
*
|
||||
* Look in the output directory for a .stdout file containing "The flag"
|
||||
*/
|
||||
|
||||
@@ -1,11 +1,36 @@
|
||||
/* Minimal toy example with input/output using libc
|
||||
* Symbolic values are read from stdin using standard libc calls.
|
||||
*
|
||||
/**
|
||||
* Symbolic values are read from stdin using standard libc calls.
|
||||
* Program checks if a binary packed integer at the input is 0x41 or less.
|
||||
*
|
||||
* Compile with :
|
||||
* $ gcc toy002-libc.c -o toy002-libc
|
||||
*
|
||||
* Analize it with:
|
||||
* $ python system.py --sym stdin examples/toy002-libc
|
||||
* $ gcc -static -Os basic.c -o basic
|
||||
*
|
||||
* Analyze it with:
|
||||
* $ manticore basic
|
||||
*
|
||||
* - By default manticore will consider all input of stdin symbolic
|
||||
*
|
||||
* Expected output:
|
||||
* $ manticore basic
|
||||
* 2017-04-22 10:35:52,789: [9309] MAIN:INFO: Loading program: ['basic']
|
||||
* 2017-04-22 10:35:52,792: [9309] MAIN:INFO: Workspace: ./mcore_IJ2sPb
|
||||
* 2017-04-22 10:36:24,386: [9359][3] EXECUTOR:INFO: Generating testcase No. 1 for state No.3 - Program finished correctly
|
||||
* 2017-04-22 10:36:28,452: [9359][5] EXECUTOR:INFO: Generating testcase No. 2 for state No.5 - Program finished correctly
|
||||
*
|
||||
* Look at ./mcore_IJ2sPb for results, you will find something like this:
|
||||
* $ hexdump -C test_00000001.stdin
|
||||
* 00000000 00 80 00 20 |... |
|
||||
*
|
||||
* $ hexdump -C test_00000002.stdin
|
||||
* 00000000 41 00 00 00 |A...|
|
||||
*
|
||||
* You can try out the values like this:
|
||||
*
|
||||
* $ printf "\x00\x80\x00\x20" | ./basic
|
||||
* Message: It is greater than 0x41
|
||||
*
|
||||
* $ printf "\x41\x00\x00\x00" | ../basic
|
||||
* Message: It is smaller or equal than 0x41
|
||||
*/
|
||||
|
||||
#include <stdio.h>
|
||||
|
||||
@@ -1,116 +0,0 @@
|
||||
import random, string, random
|
||||
chars = string.ascii_uppercase + string.digits
|
||||
|
||||
antitrace = False
|
||||
password = 'CBAHACKS#2016#01'
|
||||
|
||||
|
||||
PROGRAM = ''
|
||||
PROGRAM += '''
|
||||
|
||||
#include <stdio.h>
|
||||
#include <stdlib.h>
|
||||
#include <unistd.h>
|
||||
#include <sys/types.h>
|
||||
'''
|
||||
|
||||
if antitrace:
|
||||
PROGRAM += '''
|
||||
|
||||
#include <sys/ptrace.h>
|
||||
#include <sys/wait.h>
|
||||
char brand[] = "http://www.julioauto.com/rants/anti_ptrace.htm";
|
||||
void anti_ptrace(void)
|
||||
{
|
||||
pid_t child;
|
||||
|
||||
if(getenv("LD_PRELOAD"))
|
||||
while(1);
|
||||
|
||||
|
||||
child = fork();
|
||||
if (child){
|
||||
wait(NULL);
|
||||
}else {
|
||||
if (ptrace(PTRACE_TRACEME, 0, 1, 0) == -1)
|
||||
while(1);
|
||||
exit(0);
|
||||
}
|
||||
|
||||
if (ptrace(PTRACE_TRACEME, 0, 0, 0) == -1)
|
||||
while(1);
|
||||
|
||||
}
|
||||
'''
|
||||
|
||||
PROGRAM += '''
|
||||
int
|
||||
main(int argc, char* argv[]){'''
|
||||
|
||||
if antitrace:
|
||||
PROGRAM += '''
|
||||
sleep(10);
|
||||
anti_ptrace();
|
||||
'''
|
||||
|
||||
|
||||
pad = ''.join(random.choice(chars) for _ in range(len(password)))
|
||||
|
||||
banner = '''
|
||||
This computer system is for authorized use only. All activity is logged and
|
||||
regularly checked by system administrators. Individuals attempting to connect
|
||||
to, port-scan, deface, hack, or otherwise interfere with any services on this
|
||||
system will be reported.
|
||||
_____ _
|
||||
| __ \ | |
|
||||
| |__) |_ _ ___ _____ _____ _ __ __| |
|
||||
| ___/ _` / __/ __\ \ /\ / / _ \| '__/ _` |
|
||||
| | | (_| \__ \__ \\\\ V V / (_) | | | (_|
|
||||
|_| \__,_|___/___/ \_/\_/ \___/|_| \__,_|
|
||||
Authorized use only!
|
||||
|
||||
Please enter your password:
|
||||
'''
|
||||
import json
|
||||
|
||||
PROGRAM += '''printf ("%s");'''%json.dumps(banner).strip('"')
|
||||
PROGRAM += '''char xor(char a, char b){
|
||||
return a^b;
|
||||
}
|
||||
'''
|
||||
PROGRAM += '''int c;\n'''
|
||||
|
||||
def func(password, pad, flag=True):
|
||||
if len(password) == 1:
|
||||
#SUBPROGRAMTRUE = '''if ( getchar() == 0x10 )\n'''
|
||||
if flag:
|
||||
SUBPROGRAMTRUE = ''' printf("You are in!\\n");\n'''
|
||||
else:
|
||||
SUBPROGRAMTRUE = ''' printf("You are NOT in!\\n");\n'''
|
||||
else:
|
||||
SUBPROGRAMTRUE = func(password[1:], pad[1:], flag)
|
||||
|
||||
if len(password) == 1:
|
||||
SUBPROGRAMFALSE = ''' printf("You are NOT in!\\n");\n'''
|
||||
else:
|
||||
SUBPROGRAMFALSE = func(''.join(random.choice(chars) for _ in range(len(password)/2)), pad[1:], False)
|
||||
|
||||
config = random.choice([ (True, SUBPROGRAMTRUE, SUBPROGRAMFALSE), (False, SUBPROGRAMFALSE, SUBPROGRAMTRUE)])
|
||||
|
||||
SUBPROGRAM = ''
|
||||
if config[0]:
|
||||
SUBPROGRAM += '''if ( ((c = getchar(), (c >= 0)) && xor(c, '%c') == ('%c' ^ '%c')) ){\n'''%(pad[0], password[0], pad[0])
|
||||
else:
|
||||
SUBPROGRAM += '''if ( ((c = getchar(), (c < 0)) || xor(c, '%c') != ('%c' ^ '%c')) ){\n'''%(pad[0], password[0], pad[0])
|
||||
|
||||
SUBPROGRAM += config[1]
|
||||
SUBPROGRAM += '''}else {\n'''
|
||||
SUBPROGRAM += config[2]
|
||||
SUBPROGRAM += '''}'''
|
||||
SUBPROGRAM = ('\n'+(' ')).join(SUBPROGRAM.split('\n'))
|
||||
return (' ')+SUBPROGRAM+'\n'
|
||||
|
||||
PROGRAM += func(password, pad)
|
||||
PROGRAM += '''return 0;\n}'''
|
||||
print PROGRAM
|
||||
|
||||
153
examples/linux/crackme.py
Normal file
153
examples/linux/crackme.py
Normal file
@@ -0,0 +1,153 @@
|
||||
import random, string, random
|
||||
chars = string.ascii_uppercase + string.digits
|
||||
|
||||
antitrace = False
|
||||
password = 'SCRT'
|
||||
|
||||
|
||||
PROGRAM = ''
|
||||
PROGRAM += '''
|
||||
/* This program parses a commandline argument.
|
||||
*
|
||||
* Compile with :
|
||||
* $ gcc -static -Os crackme.c -o crackme
|
||||
*
|
||||
* Analyze it with:
|
||||
* $ manticore crackme
|
||||
*
|
||||
* - By default manticore will consider all input of stdin symbolic
|
||||
* It will explore all possible paths, eventually finding the SCRT key
|
||||
*
|
||||
* Expected output:
|
||||
* $ manticore --proc 5 crackme
|
||||
* 2017-04-22 10:57:07,913: [11918] MAIN:INFO: Loading program: ['crackme']
|
||||
* 2017-04-22 10:57:07,918: [11918] MAIN:INFO: Workspace: ./mcore_fZKdZ8
|
||||
* 2017-04-22 10:57:56,068: [11969][23] EXECUTOR:INFO: Generating testcase No. 1 for state No.23 - Program finished correctly
|
||||
* 2017-04-22 10:57:56,461: [11975][21] EXECUTOR:INFO: Generating testcase No. 2 for state No.21 - Program finished correctly
|
||||
* 2017-04-22 10:57:56,877: [11978][31] EXECUTOR:INFO: Generating testcase No. 3 for state No.31 - Program finished correctly
|
||||
* 2017-04-22 10:57:57,053: [11971][35] EXECUTOR:INFO: Generating testcase No. 4 for state No.35 - Program finished correctly
|
||||
* 2017-04-22 10:57:57,817: [11970][42] EXECUTOR:INFO: Generating testcase No. 5 for state No.42 - Program finished correctly
|
||||
* 2017-04-22 10:58:26,874: [11975][30] EXECUTOR:INFO: Generating testcase No. 6 for state No.30 - Program finished correctly
|
||||
* 2017-04-22 10:58:27,187: [11969][44] EXECUTOR:INFO: Generating testcase No. 7 for state No.44 - Program finished correctly
|
||||
* 2017-04-22 10:58:27,571: [11971][27] EXECUTOR:INFO: Generating testcase No. 8 for state No.27 - Program finished correctly
|
||||
* 2017-04-22 10:58:28,567: [11978][53] EXECUTOR:INFO: Generating testcase No. 9 for state No.53 - Program finished correctly
|
||||
* 2017-04-22 10:58:33,148: [11970][51] EXECUTOR:INFO: Generating testcase No. 10 for state No.51 - Program finished correctly
|
||||
*
|
||||
* Look at ./mcore_IJ2sPb for results, you will find something like this:
|
||||
*
|
||||
* $ head -c 4 *.stdin
|
||||
* ==> test_00000001.stdin <==
|
||||
* <20>CMM
|
||||
* ==> test_00000002.stdin <==
|
||||
* <20>C<EFBFBD><43>
|
||||
* ==> test_00000003.stdin <==
|
||||
* <20><>SS
|
||||
* ==> test_00000004.stdin <==
|
||||
* <20><><EFBFBD><EFBFBD>
|
||||
* ==> test_00000005.stdin <==
|
||||
* SCR
|
||||
* ==> test_00000006.stdin <==
|
||||
* S<>TT
|
||||
* ==> test_00000007.stdin <==
|
||||
* SCRT
|
||||
* ==> test_00000008.stdin <==
|
||||
* S<><53><EFBFBD>
|
||||
* ==> test_00000009.stdin <==
|
||||
* SC<53>@
|
||||
* ==> test_0000000a.stdin <==
|
||||
* SC<53>8
|
||||
*
|
||||
*/
|
||||
#include <stdio.h>
|
||||
#include <stdlib.h>
|
||||
#include <unistd.h>
|
||||
#include <sys/types.h>
|
||||
'''
|
||||
|
||||
if antitrace:
|
||||
PROGRAM += '''
|
||||
|
||||
#include <sys/ptrace.h>
|
||||
#include <sys/wait.h>
|
||||
char brand[] = "http://www.julioauto.com/rants/anti_ptrace.htm";
|
||||
void anti_ptrace(void)
|
||||
{
|
||||
pid_t child;
|
||||
|
||||
if(getenv("LD_PRELOAD"))
|
||||
while(1);
|
||||
|
||||
|
||||
child = fork();
|
||||
if (child){
|
||||
wait(NULL);
|
||||
}else {
|
||||
if (ptrace(PTRACE_TRACEME, 0, 1, 0) == -1)
|
||||
while(1);
|
||||
exit(0);
|
||||
}
|
||||
|
||||
if (ptrace(PTRACE_TRACEME, 0, 0, 0) == -1)
|
||||
while(1);
|
||||
|
||||
}
|
||||
'''
|
||||
|
||||
PROGRAM += '''
|
||||
int
|
||||
main(int argc, char* argv[]){'''
|
||||
|
||||
if antitrace:
|
||||
PROGRAM += '''
|
||||
sleep(10);
|
||||
anti_ptrace();
|
||||
'''
|
||||
|
||||
|
||||
pad = ''.join(random.choice(chars) for _ in range(len(password)))
|
||||
|
||||
banner = '''Please enter your password:
|
||||
'''
|
||||
import json
|
||||
|
||||
PROGRAM += '''printf ("%s");'''%json.dumps(banner).strip('"')
|
||||
PROGRAM += '''char xor(char a, char b){
|
||||
return a^b;
|
||||
}
|
||||
'''
|
||||
PROGRAM += '''int c;\n'''
|
||||
|
||||
def func(password, pad, flag=True):
|
||||
if len(password) == 1:
|
||||
#SUBPROGRAMTRUE = '''if ( getchar() == 0x10 )\n'''
|
||||
if flag:
|
||||
SUBPROGRAMTRUE = ''' printf("You are in!\\n");\n'''
|
||||
else:
|
||||
SUBPROGRAMTRUE = ''' printf("You are NOT in!\\n");\n'''
|
||||
else:
|
||||
SUBPROGRAMTRUE = func(password[1:], pad[1:], flag)
|
||||
|
||||
if len(password) == 1:
|
||||
SUBPROGRAMFALSE = ''' printf("You are NOT in!\\n");\n'''
|
||||
else:
|
||||
SUBPROGRAMFALSE = func(''.join(random.choice(chars) for _ in range(len(password)/2)), pad[1:], False)
|
||||
|
||||
config = random.choice([ (True, SUBPROGRAMTRUE, SUBPROGRAMFALSE), (False, SUBPROGRAMFALSE, SUBPROGRAMTRUE)])
|
||||
|
||||
SUBPROGRAM = ''
|
||||
if config[0]:
|
||||
SUBPROGRAM += '''if ( ((c = getchar(), (c >= 0)) && xor(c, '%c') == ('%c' ^ '%c')) ){\n'''%(pad[0], password[0], pad[0])
|
||||
else:
|
||||
SUBPROGRAM += '''if ( ((c = getchar(), (c < 0)) || xor(c, '%c') != ('%c' ^ '%c')) ){\n'''%(pad[0], password[0], pad[0])
|
||||
|
||||
SUBPROGRAM += config[1]
|
||||
SUBPROGRAM += '''}else {\n'''
|
||||
SUBPROGRAM += config[2]
|
||||
SUBPROGRAM += '''}'''
|
||||
SUBPROGRAM = ('\n'+(' ')).join(SUBPROGRAM.split('\n'))
|
||||
return (' ')+SUBPROGRAM+'\n'
|
||||
|
||||
PROGRAM += func(password, pad)
|
||||
PROGRAM += '''return 0;\n}'''
|
||||
print PROGRAM
|
||||
|
||||
@@ -1,13 +1,29 @@
|
||||
/* Minimal toy example with input output
|
||||
/* The symbolic input is taken from command line argument and it is
|
||||
* used as an index in a function pointer table. Analysis should explore
|
||||
* both functions.
|
||||
*
|
||||
* The symbolic input is taken from command line argumets passed to the interpreted program
|
||||
* Will use the argv input to select a pointer from a lit and call it.
|
||||
* Compile with :
|
||||
* $ gcc -static -Os ibranch.c -o ibranch
|
||||
*
|
||||
* Compile with :
|
||||
* $ gcc toy006-ibranch.c -o toy006-ibranch
|
||||
* Analyze it with:
|
||||
* $ manticore ibranch +
|
||||
*
|
||||
* Analize it with:
|
||||
* $ python system.py example/toy006-ibranch +
|
||||
* - The character + at the argument will be replaced by a free symbolic byte
|
||||
*
|
||||
* Expected output:
|
||||
* $ manticore ibranch +
|
||||
* 2017-04-24 12:05:09,089: [13266] MAIN:INFO: Loading program: ['ibranch', '+']
|
||||
* 2017-04-24 12:05:09,090: [13266] MAIN:INFO: Workspace: ./mcore_1DLM6g
|
||||
* 2017-04-24 12:05:19,750: [13316][0] MEMORY:INFO: Reading 8 bytes from symbolic address <manticore.core.smtlib.expression.BitVecAnd object at 0x7f629e40b590>
|
||||
* 2017-04-24 12:05:27,061: [13316][3] EXECUTOR:INFO: Generating testcase No. 1 for state No.3 - Program finished correctly
|
||||
* 2017-04-24 12:05:28,577: [13316][5] EXECUTOR:INFO: Generating testcase No. 2 for state No.5 - Program finished correctly
|
||||
*
|
||||
* Look at ./mcore_1DLM6g for results, you will find something like this:
|
||||
* $ cat *.stdout
|
||||
* Function g
|
||||
* Function f
|
||||
* - It found two finishing paths and explore both functions. -
|
||||
*
|
||||
*/
|
||||
|
||||
#include <stdio.h>
|
||||
|
||||
@@ -1,20 +1,50 @@
|
||||
/* This programs reads a M bytes from stdin, scrambles them, and sums them all.
|
||||
* Only some buffers make the program print "You won!".
|
||||
* Increasing the number of symbolic bytes can generate path constraints too hard to solve.
|
||||
*
|
||||
* Compile with :
|
||||
* $ gcc -static -Os indexhell.c -o indexhell
|
||||
*
|
||||
* Analyze it with:
|
||||
* $ manticore indexhell
|
||||
*
|
||||
* - By default manticore will consider all input of stdin symbolic
|
||||
*
|
||||
* 2017-04-24 12:46:46,227: [15880] MAIN:INFO: Loading program: ['indexhell']
|
||||
* 2017-04-24 12:46:46,228: [15880] MAIN:INFO: Workspace: ./mcore_72BTxZ
|
||||
* 2017-04-24 12:46:53,302: [15934][0] MEMORY:INFO: Reading 1 bytes from symbolic address <manticore.core.smtlib.expression.BitVecAnd object at 0x7f0ad114c4d0>
|
||||
* 2017-04-24 12:46:54,093: [15934][0] MEMORY:INFO: Reading 1 bytes from symbolic address <manticore.core.smtlib.expression.BitVecAnd object at 0x7f0ad177acd0>
|
||||
* 2017-04-24 12:46:54,944: [15934][0] MEMORY:INFO: Reading 1 bytes from symbolic address <manticore.core.smtlib.expression.BitVecAnd object at 0x7f0ad1051110>
|
||||
* 2017-04-24 12:46:55,907: [15934][0] MEMORY:INFO: Reading 1 bytes from symbolic address <manticore.core.smtlib.expression.BitVecAnd object at 0x7f0ad115f9d0>
|
||||
* 2017-04-24 12:46:56,678: [15934][0] MEMORY:INFO: Reading 1 bytes from symbolic address <manticore.core.smtlib.expression.BitVecAnd object at 0x7f0ad1009150>
|
||||
* 2017-04-24 12:46:57,497: [15934][0] MEMORY:INFO: Reading 1 bytes from symbolic address <manticore.core.smtlib.expression.BitVecAnd object at 0x7f0ad1016550>
|
||||
* 2017-04-24 12:47:06,520: [15934][3] EXECUTOR:INFO: Generating testcase No. 1 for state No.3 - Program finished correctly
|
||||
* 2017-04-24 12:47:09,693: [15934][5] EXECUTOR:INFO: Generating testcase No. 2 for state No.5 - Program finished correctly
|
||||
*
|
||||
* Look at ./mcore_72BTxZ for results, you will find something like this:
|
||||
* hexdump -C test_00000001.stdin
|
||||
* 00000000 23 80 26 ff 4f 56 |#.&.OV|
|
||||
*
|
||||
* cat mcore_72BTxZ/test_00000001 | ./indexhell
|
||||
* You won!
|
||||
*/
|
||||
|
||||
|
||||
#include<stdio.h>
|
||||
#define M 6
|
||||
|
||||
main(){
|
||||
int i,count;
|
||||
unsigned char buffer[256];
|
||||
read(0, buffer, 256);
|
||||
unsigned char buffer[M];
|
||||
read(0, buffer, M);
|
||||
|
||||
|
||||
for (i=0;i <256;i++)
|
||||
buffer[i] = buffer[buffer[i]] ^ buffer[i];
|
||||
for (i=0; i<M; i++)
|
||||
buffer[i] = buffer[buffer[i]%M] ^ buffer[i];
|
||||
|
||||
count = 0;
|
||||
for (i=0;i <256;i++)
|
||||
for (i=0; i < M; i++)
|
||||
count += buffer[i];
|
||||
|
||||
if (count == 0x414243)
|
||||
if (count == 0x123)
|
||||
printf("You won!");
|
||||
|
||||
return 0;
|
||||
|
||||
@@ -4,7 +4,7 @@
|
||||
* Compile with :
|
||||
* $ gcc -fno-builtin -static -nostdlib -m32 -fomit-frame-pointer toy001.c -o toy001
|
||||
*
|
||||
* Analize it with:
|
||||
* Analyze it with:
|
||||
* $ python system.py --sym stdin examples/toy001-nostdlib
|
||||
*/
|
||||
|
||||
|
||||
@@ -1,47 +0,0 @@
|
||||
/* A simple server in the internet domain using TCP
|
||||
The port number is passed as an argument */
|
||||
#include <stdio.h>
|
||||
#include <sys/types.h>
|
||||
#include <sys/socket.h>
|
||||
#include <netinet/in.h>
|
||||
|
||||
void error(char *msg)
|
||||
{
|
||||
perror(msg);
|
||||
exit(1);
|
||||
}
|
||||
|
||||
int main(int argc, char *argv[])
|
||||
{
|
||||
int sockfd, newsockfd, portno, clilen;
|
||||
char buffer[256];
|
||||
struct sockaddr_in serv_addr, cli_addr;
|
||||
int n;
|
||||
if (argc < 2) {
|
||||
fprintf(stderr,"ERROR, no port provided\n");
|
||||
exit(1);
|
||||
}
|
||||
sockfd = socket(AF_INET, SOCK_STREAM, 0);
|
||||
if (sockfd < 0)
|
||||
error("ERROR opening socket");
|
||||
bzero((char *) &serv_addr, sizeof(serv_addr));
|
||||
portno = atoi(argv[1]);
|
||||
serv_addr.sin_family = AF_INET;
|
||||
serv_addr.sin_addr.s_addr = INADDR_ANY;
|
||||
serv_addr.sin_port = htons(portno);
|
||||
if (bind(sockfd, (struct sockaddr *) &serv_addr,
|
||||
sizeof(serv_addr)) < 0)
|
||||
error("ERROR on binding");
|
||||
listen(sockfd,5);
|
||||
clilen = sizeof(cli_addr);
|
||||
newsockfd = accept(sockfd, (struct sockaddr *) &cli_addr, &clilen);
|
||||
if (newsockfd < 0)
|
||||
error("ERROR on accept");
|
||||
bzero(buffer,256);
|
||||
n = read(newsockfd,buffer,255);
|
||||
if (n < 0) error("ERROR reading from socket");
|
||||
printf("Here is the message: %s\n",buffer);
|
||||
n = write(newsockfd,"I got your message",18);
|
||||
if (n < 0) error("ERROR writing to socket");
|
||||
return 0;
|
||||
}
|
||||
@@ -1,14 +1,61 @@
|
||||
/* Minimal toy example with input outputA
|
||||
*
|
||||
* This program will use the input from stdin as an index into a 256 bytes long array of bools (bytes)
|
||||
* If input is considered symbolic this will exercise a read on a symbolic input.
|
||||
/* This program uses the input from stdin as an index into a 256 bytes long
|
||||
* array of booleans (bytes). Only 3 indexes of the array are set to *true*.
|
||||
* All remaining array values are false.
|
||||
* Only indexes in the set { 0xfe, 0xfc, 0xfd } may branch to the "Found" part.
|
||||
*
|
||||
* Compile with :
|
||||
* $ gcc toy003-sindex.c -o toy003-sindex
|
||||
*
|
||||
* Analize it with:
|
||||
* $ python system.py --sym stdin example/toy003-sindex
|
||||
*
|
||||
* Compile with :
|
||||
* $ gcc -static -Os sindex.c -o sindex
|
||||
*
|
||||
* Analyze it with:
|
||||
* $ manticore sindex
|
||||
*
|
||||
* - By default manticore will consider` all input of stdin symbolic
|
||||
*
|
||||
* Expected output:
|
||||
* $ manticore sindex
|
||||
* 2017-04-24 12:16:53,413: [13490] MAIN:INFO: Loading program: ['sindex']
|
||||
* 2017-04-24 12:16:53,414: [13490] MAIN:INFO: Workspace: ./mcore_wZWmf_
|
||||
* 2017-04-24 12:17:00,455: [13540][0] MEMORY:INFO: Reading 1 bytes from symbolic address <manticore.core.smtlib.expression.BitVecAnd object at 0x7fe811910150>
|
||||
* 2017-04-24 12:17:03,303: [13540][3] EXECUTOR:INFO: Generating testcase No. 1 for state No.3 - Program finished correctly
|
||||
* 2017-04-24 12:17:04,883: [13540][5] EXECUTOR:INFO: Generating testcase No. 2 for state No.5 - Program finished correctly
|
||||
*
|
||||
* Look at ./mcore_IJ2sPb for results.
|
||||
* $ ls -1
|
||||
* command.sh
|
||||
* test_00000001.messages
|
||||
* test_00000001.pkl
|
||||
* test_00000001.smt
|
||||
* test_00000001.stderr
|
||||
* test_00000001.stdin
|
||||
* test_00000001.stdout
|
||||
* test_00000001.syscalls
|
||||
* test_00000001.trace
|
||||
* test_00000001.txt
|
||||
* test_00000002.messages
|
||||
* test_00000002.pkl
|
||||
* test_00000002.smt
|
||||
* test_00000002.stderr
|
||||
* test_00000002.stdin
|
||||
* test_00000002.stdout
|
||||
* test_00000002.syscalls
|
||||
* test_00000002.trace
|
||||
* test_00000002.txt
|
||||
*
|
||||
* Note it generated only 2 finishing traces.
|
||||
* One for the index selecting a false boolean
|
||||
* $ cat test_00000002.stdout
|
||||
* Message: Not Found!
|
||||
*
|
||||
* and one for the index selecting a true value
|
||||
* $ cat test_00000001.stdout
|
||||
* Message: Found!
|
||||
*
|
||||
* test_00000001.stdin contains a single solution for it.
|
||||
* $ hexdump test_00000001.stdin
|
||||
* But there were 3 possible indexes! { 0xfe, 0xfc, 0xfd } !!
|
||||
* The path constraint describing the full set of solutions can
|
||||
* be found at test_00000001.smt
|
||||
*/
|
||||
|
||||
#include <stdio.h>
|
||||
|
||||
@@ -1,13 +1,52 @@
|
||||
/* Minimal toy example with input output
|
||||
/* This program will read data from stdin and compare it with a constant string
|
||||
* using standard strcmp function as provided by libc.
|
||||
*
|
||||
* This program will read data from stdin and compare it with a constant string
|
||||
* using standard strcmp function.
|
||||
*
|
||||
* Compile with :
|
||||
* $ gcc toy004-strcmp.c -o toy004-strcmp
|
||||
* $ gcc -static -Os strncmp.c -o strncmp
|
||||
*
|
||||
* Analyze it with:
|
||||
* $ manticore strncmp
|
||||
* - By default manticore will consider` all input of stdin symbolic
|
||||
*
|
||||
* Expected output:
|
||||
* 2017-04-24 16:04:22,261: [30182] MAIN:INFO: Loading program: ['strncmp']
|
||||
* 2017-04-24 16:04:22,262: [30182] MAIN:INFO: Workspace: ./mcore__dZkhU
|
||||
* 2017-04-24 16:04:30,642: [30232][5] EXECUTOR:INFO: Generating testcase No. 1 for state No.5 - Program finished correctly
|
||||
* 2017-04-24 16:04:32,880: [30232][21] EXECUTOR:INFO: Generating testcase No. 2 for state No.21 - Program finished correctly
|
||||
* 2017-04-24 16:04:36,698: [30232][27] EXECUTOR:INFO: Generating testcase No. 3 for state No.27 - Program finished correctly
|
||||
* 2017-04-24 16:04:41,033: [30232][32] EXECUTOR:INFO: Generating testcase No. 4 for state No.32 - Program finished correctly
|
||||
* 2017-04-24 16:04:46,186: [30232][37] EXECUTOR:INFO: Generating testcase No. 5 for state No.37 - Program finished correctly
|
||||
* 2017-04-24 16:04:52,103: [30232][39] EXECUTOR:INFO: Generating testcase No. 6 for state No.39 - Program finished correctly
|
||||
* 2017-04-24 16:04:59,245: [30232][10] EXECUTOR:INFO: Generating testcase No. 7 for state No.10 - Program finished correctly
|
||||
* 2017-04-24 16:05:05,608: [30232][13] EXECUTOR:INFO: Generating testcase No. 8 for state No.13 - Program finished correctly
|
||||
*
|
||||
* Look at ./mcore__dZkhU for results.
|
||||
* $ head *.stdout
|
||||
* ==> test_00000001.stdout <==
|
||||
* Message: Not Found!
|
||||
*
|
||||
* ==> test_00000002.stdout <==
|
||||
* Message: Not Found!
|
||||
*
|
||||
* ==> test_00000003.stdout <==
|
||||
* Message: Not Found!
|
||||
*
|
||||
* ==> test_00000004.stdout <==
|
||||
* Message: Not Found!
|
||||
*
|
||||
* ==> test_00000005.stdout <==
|
||||
* Message: ZARAZA!
|
||||
*
|
||||
* ==> test_00000006.stdout <==
|
||||
* Message: Not Found!
|
||||
*
|
||||
* ==> test_00000007.stdout <==
|
||||
* Message: Not Found!
|
||||
*
|
||||
* ==> test_00000008.stdout <==
|
||||
* Message: Not Found!
|
||||
*
|
||||
* Analize it with:
|
||||
* $ python system.py --sym stdin example/toy004-strcmp
|
||||
*/
|
||||
|
||||
#include <stdio.h>
|
||||
|
||||
@@ -132,7 +132,7 @@ class Z3Solver(Solver):
|
||||
else:
|
||||
logger.debug(' Please install Z3 4.4.1 or newer to get optimization support')
|
||||
|
||||
self._command = 'z3 -t:30000 -smt2 -in'
|
||||
self._command = 'z3 -t:120000 -smt2 -in'
|
||||
self._init = ['(set-logic QF_AUFBV)', '(set-option :global-decls false)']
|
||||
self._get_value_fmt = (re.compile('\(\((?P<expr>(.*))\ #x(?P<value>([0-9a-fA-F]*))\)\)'), 16)
|
||||
|
||||
|
||||
Reference in New Issue
Block a user