diff --git a/examples/linux/Makefile b/examples/linux/Makefile index db1d375..d023235 100644 --- a/examples/linux/Makefile +++ b/examples/linux/Makefile @@ -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 diff --git a/examples/linux/arguments.c b/examples/linux/arguments.c index 61e01ee..b7ef3d3 100644 --- a/examples/linux/arguments.c +++ b/examples/linux/arguments.c @@ -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 -#include #include diff --git a/examples/linux/baby-re.c b/examples/linux/baby-re.c index f2cff1f..0ea4de1 100644 --- a/examples/linux/baby-re.c +++ b/examples/linux/baby-re.c @@ -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" */ diff --git a/examples/linux/basic.c b/examples/linux/basic.c index 989dde6..fb48c1e 100644 --- a/examples/linux/basic.c +++ b/examples/linux/basic.c @@ -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 diff --git a/examples/linux/cbahacks.py b/examples/linux/cbahacks.py deleted file mode 100644 index 1eb735e..0000000 --- a/examples/linux/cbahacks.py +++ /dev/null @@ -1,116 +0,0 @@ -import random, string, random -chars = string.ascii_uppercase + string.digits - -antitrace = False -password = 'CBAHACKS#2016#01' - - -PROGRAM = '' -PROGRAM += ''' - -#include -#include -#include -#include -''' - -if antitrace: - PROGRAM += ''' - -#include -#include -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 - diff --git a/examples/linux/crackme.py b/examples/linux/crackme.py new file mode 100644 index 0000000..6d544d6 --- /dev/null +++ b/examples/linux/crackme.py @@ -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 <== + * �CMM + * ==> test_00000002.stdin <== + * �C�� + * ==> test_00000003.stdin <== + * ��SS + * ==> test_00000004.stdin <== + * ���� + * ==> test_00000005.stdin <== + * SCR + * ==> test_00000006.stdin <== + * S�TT + * ==> test_00000007.stdin <== + * SCRT + * ==> test_00000008.stdin <== + * S��� + * ==> test_00000009.stdin <== + * SC�@ + * ==> test_0000000a.stdin <== + * SC�8 + * +*/ +#include +#include +#include +#include +''' + +if antitrace: + PROGRAM += ''' + +#include +#include +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 + diff --git a/examples/linux/ibranch.c b/examples/linux/ibranch.c index 3f48509..92f89e7 100644 --- a/examples/linux/ibranch.c +++ b/examples/linux/ibranch.c @@ -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 + * 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 diff --git a/examples/linux/indexhell.c b/examples/linux/indexhell.c index 67eb413..842767c 100644 --- a/examples/linux/indexhell.c +++ b/examples/linux/indexhell.c @@ -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 + * 2017-04-24 12:46:54,093: [15934][0] MEMORY:INFO: Reading 1 bytes from symbolic address + * 2017-04-24 12:46:54,944: [15934][0] MEMORY:INFO: Reading 1 bytes from symbolic address + * 2017-04-24 12:46:55,907: [15934][0] MEMORY:INFO: Reading 1 bytes from symbolic address + * 2017-04-24 12:46:56,678: [15934][0] MEMORY:INFO: Reading 1 bytes from symbolic address + * 2017-04-24 12:46:57,497: [15934][0] MEMORY:INFO: Reading 1 bytes from symbolic address + * 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 +#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 -#include -#include -#include - -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; -} diff --git a/examples/linux/sindex.c b/examples/linux/sindex.c index a79a88f..0d6f631 100644 --- a/examples/linux/sindex.c +++ b/examples/linux/sindex.c @@ -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 + * 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 diff --git a/examples/linux/strncmp.c b/examples/linux/strncmp.c index 59af752..0abc0d5 100644 --- a/examples/linux/strncmp.c +++ b/examples/linux/strncmp.c @@ -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 diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index 91f8218..bb189f0 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -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(.*))\ #x(?P([0-9a-fA-F]*))\)\)'), 16)