Created
June 1, 2015 13:15
-
-
Save volpino/3559c253d785a34d225e to your computer and use it in GitHub Desktop.
klug
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<stdlib.h> | |
| #include<klee/klee.h> | |
| #include "defs.h" | |
| int main(int argc, const char **argv, const char **envp); | |
| void path_fail(); | |
| void count_fail(); | |
| void path_key(); | |
| void path_c(int a1, char *a2, int a3); | |
| void path_a(int a1, char *a2, int a3, int a4); | |
| void path_e(int a1, char *a2, int a3, int a4); | |
| void path_d(unsigned int a1, char *a2, int a3); | |
| void path_f(unsigned int a1, char *a2, int a3, int a4); | |
| //------------------------------------------------------------------------- | |
| // Data declarations | |
| int _JCR_LIST__ = 0; // weak | |
| int _stack_chk_guard; // weak | |
| char completed_6152; // weak | |
| char path_count_3723; // weak | |
| char path_count_3709; // weak | |
| char path_count_3716; // weak | |
| char path_count_3737; // weak | |
| char path_count_3730; // weak | |
| char path_count_3744; // weak | |
| // extern _UNKNOWN __gmon_start__; weak | |
| //----- (000085C8) -------------------------------------------------------- | |
| int main(int argc, const char **argv, const char **envp) | |
| { | |
| int idx; // r5@1 | |
| int len; // r4@1 | |
| int v5; // r3@2 | |
| char v6; // r0@5 | |
| int result; // r0@9 | |
| char v8[4096]; // [sp+0h] [bp-1020h]@6 | |
| int v9; // [sp+1004h] [bp-1Ch]@1 | |
| idx = 0; | |
| len = 0; | |
| setvbuf(stdout, 0, 2, 0); | |
| puts("\nWelcome! Find me the path to your flag and you shall get your reward!"); | |
| do | |
| { | |
| //v6 = getc(stdin); | |
| klee_make_symbolic(&v6, sizeof(v6), "v6"); | |
| if ( v6 == -1 ) | |
| { | |
| v5 = LOBYTE((&v8)[idx]); | |
| } | |
| else | |
| { | |
| v5 = (unsigned __int8)v6; | |
| v8[idx] = v6; | |
| } | |
| ++len; | |
| if ( v5 == 10 ) | |
| break; | |
| idx = len; | |
| v5 = (unsigned int)len <= 0xFFF; | |
| if ( v6 == -1 ) | |
| v5 = 0; | |
| } | |
| while ( v5 ); | |
| //klee_make_symbolic(v8, len, "input"); | |
| path_a(0x6B6C6565, (char *)&v8, len, v5); | |
| result = 0; | |
| return result; | |
| } | |
| // 854C: using guessed type int __fastcall _stack_chk_fail(_DWORD); | |
| // 11050: using guessed type int _stack_chk_guard; | |
| // 11058: using guessed type int stdin; | |
| // 1105C: using guessed type int stdout; | |
| //----- (00008710) -------------------------------------------------------- | |
| void path_fail() | |
| { | |
| puts("Wrong path, try again next time!"); | |
| exit(1); | |
| } | |
| //----- (00008724) -------------------------------------------------------- | |
| void count_fail() | |
| { | |
| puts("You've been down this path too many times!"); | |
| exit(1); | |
| } | |
| //----- (00008738) -------------------------------------------------------- | |
| void path_key() | |
| { | |
| FILE *v0; // r0@1 | |
| FILE *v1; // r4@1 | |
| char s; // [sp+4h] [bp-10Ch]@2 | |
| int v3; // [sp+104h] [bp-Ch]@1 | |
| v3 = _stack_chk_guard; | |
| v0 = fopen("/tmp/flag", "r"); | |
| v1 = v0; | |
| if ( v0 ) | |
| { | |
| if ( fgets(&s, 255, v0) ) | |
| { | |
| fclose(v1); | |
| printf("The flag is: %s\n", &s); | |
| klee_assert(0); //Signal The solution!! | |
| exit(1); | |
| } | |
| puts("Flag file error! Report the error at once!"); | |
| exit(1); | |
| } | |
| puts("Unable to open flag file! Report the error at once!"); | |
| exit(1); | |
| } | |
| // 85A4: using guessed type int _printf_chk(_DWORD, const char *, ...); | |
| // 11050: using guessed type int _stack_chk_guard; | |
| //----- (000087A0) -------------------------------------------------------- | |
| void path_c(int a1, char *a2, int a3) | |
| { | |
| int v3; // r3@3 | |
| int v4; // r0@3 | |
| unsigned int v5; // r5@3 | |
| char *v6; // r1@4 | |
| int v7; // r2@4 | |
| if ( !a3 ) | |
| path_fail(); | |
| if ( (unsigned __int8)path_count_3723 > 1u ) | |
| count_fail(); | |
| v3 = (unsigned __int8)*a2; | |
| v4 = a1 + 17; | |
| ++path_count_3723; | |
| v5 = v3 % 3u; | |
| if ( v5 + ((unsigned int)v4 >> 4) == (v4 & 0xF) && (v4 << (v3 & 7)) % 0x7Bu == 115 ) | |
| { | |
| v3 <<= v4 % 3u; | |
| if ( v4 > (unsigned int)v3 ) | |
| path_key(); | |
| } | |
| v6 = a2 + 1; | |
| v7 = a3 - 1; | |
| if ( v5 ) | |
| path_f(v4, v6, v7, v3); | |
| else | |
| path_d(v4, v6, v7); | |
| } | |
| // 11061: using guessed type char path_count_3723; | |
| //----- (00008848) -------------------------------------------------------- | |
| void path_a(int a1, char *a2, int a3, int a4) | |
| { | |
| unsigned __int8 v4; // r5@3 | |
| int v5; // r0@3 | |
| int v6; // r4@3 | |
| unsigned int v7; // r7@3 | |
| char *v8; // r1@4 | |
| int v9; // r2@4 | |
| char v10; // r5@8 | |
| int v11; // r0@9 | |
| unsigned int v12; // t1@12 | |
| if ( !a3 ) | |
| LABEL_22: | |
| path_fail(); | |
| if ( (unsigned __int8)path_count_3709 > 2u ) | |
| goto LABEL_20; | |
| v4 = *a2; | |
| v5 = 2 * a1; | |
| v6 = (unsigned __int8)(path_count_3709++ + 1); | |
| v7 = v4 % 3u; | |
| if ( (_BYTE)v7 ) | |
| { | |
| LABEL_4: | |
| v8 = a2 + 1; | |
| v9 = a3 - 1; | |
| if ( v7 == 1 ) | |
| path_c(v5, v8, v9); | |
| else | |
| path_d(v5, v8, v9); | |
| } | |
| else | |
| { | |
| if ( a3 == 1 ) | |
| goto LABEL_22; | |
| if ( (unsigned __int8)path_count_3716 > 2u ) | |
| goto LABEL_20; | |
| v10 = path_count_3716 + 1; | |
| while ( 1 ) | |
| { | |
| v11 = v5 + 27; | |
| if ( (unsigned __int8)a2[1] % 0x75u > 0x1E ) | |
| break; | |
| if ( a3 == 2 ) | |
| goto LABEL_21; | |
| if ( v6 == 3 ) | |
| { | |
| LABEL_19: | |
| path_count_3709 = v6; | |
| path_count_3716 = v10; | |
| LABEL_20: | |
| count_fail(); | |
| } | |
| v12 = (unsigned __int8)a2[2]; | |
| a2 += 2; | |
| v5 = 2 * v11; | |
| v6 = (unsigned __int8)(v6 + 1); | |
| v7 = v12 % 3; | |
| if ( v12 % 3 ) | |
| { | |
| path_count_3709 = v6; | |
| a3 -= 2; | |
| path_count_3716 = v10; | |
| goto LABEL_4; | |
| } | |
| if ( a3 == 3 ) | |
| { | |
| LABEL_21: | |
| path_count_3709 = v6; | |
| path_count_3716 = v10; | |
| goto LABEL_22; | |
| } | |
| if ( (unsigned __int8)(v10 + 1) == 4 ) | |
| goto LABEL_19; | |
| ++v10; | |
| a3 -= 2; | |
| } | |
| path_count_3709 = v6; | |
| path_count_3716 = v10; | |
| path_c(v11, a2 + 2, a3 - 2); | |
| } | |
| } | |
| // 11062: using guessed type char path_count_3709; | |
| // 11063: using guessed type char path_count_3716; | |
| //----- (00008988) -------------------------------------------------------- | |
| void path_e(int a1, char *a2, int a3, int a4) | |
| { | |
| unsigned int v4; // r3@3 | |
| unsigned int v5; // r3@6 | |
| int v6; // r0@6 | |
| char *v7; // r1@6 | |
| int v8; // r2@6 | |
| int v9; // [sp+0h] [bp-18h]@1 | |
| v9 = a4; | |
| if ( !a3 ) | |
| goto LABEL_14; | |
| if ( (unsigned __int8)path_count_3737 > 2u ) | |
| goto LABEL_10; | |
| v4 = (unsigned __int8)*a2; | |
| ++path_count_3737; | |
| if ( !(v4 % 0x25 & 0xFF) ) | |
| { | |
| path_a(a1 - v4, a2 + 1, a3 - 1, v9); | |
| return; | |
| } | |
| if ( a3 == 1 ) | |
| LABEL_14: | |
| path_fail(); | |
| if ( (unsigned __int8)path_count_3716 > 2u ) | |
| LABEL_10: | |
| count_fail(); | |
| v5 = (unsigned __int8)a2[1]; | |
| ++path_count_3716; | |
| v6 = a1 + 26; | |
| v7 = a2 + 2; | |
| v8 = a3 - 2; | |
| if ( v5 % 0x75 > 0x1E ) | |
| path_c(v6, v7, v8); | |
| else | |
| path_a(v6, v7, v8, v9); | |
| } | |
| // 11063: using guessed type char path_count_3716; | |
| // 11064: using guessed type char path_count_3737; | |
| //----- (00008A20) -------------------------------------------------------- | |
| void path_d(unsigned int a1, char *a2, int a3) | |
| { | |
| int v3; // r0@3 | |
| int v4; // r5@3 | |
| char *v5; // r1@3 | |
| int v6; // r2@3 | |
| if ( !a3 ) | |
| path_fail(); | |
| if ( (unsigned __int8)path_count_3730 > 1u ) | |
| count_fail(); | |
| v3 = (unsigned __int8)(a1 & 0x80) | (a1 >> 1); | |
| v4 = (unsigned __int8)*a2 + v3; | |
| v5 = a2 + 1; | |
| v6 = a3 - 1; | |
| ++path_count_3730; | |
| if ( (unsigned int)v4 > 0xAA ) | |
| { | |
| path_e(v3, v5, v6, (int)&path_count_3723); | |
| } | |
| else if ( (unsigned int)v3 <= 0x7F ) | |
| { | |
| path_a(v3, v5, v6, (int)&path_count_3723); | |
| } | |
| else | |
| { | |
| path_c(v3, v5, v6); | |
| } | |
| } | |
| // 11061: using guessed type char path_count_3723; | |
| // 11065: using guessed type char path_count_3730; | |
| //----- (00008A70) -------------------------------------------------------- | |
| void path_f(unsigned int a1, char *a2, int a3, int a4) | |
| { | |
| char v4; // r3@2 | |
| int v5; // r6@3 | |
| char v6; // r4@3 | |
| unsigned int v7; // r0@5 | |
| int v8; // r3@5 | |
| int v9; // t1@10 | |
| unsigned int v10; // r4@10 | |
| unsigned int v11; // r0@13 | |
| unsigned int v12; // r3@17 | |
| unsigned int v13; // r3@20 | |
| int v14; // r0@20 | |
| char *v15; // r1@20 | |
| int v16; // r2@20 | |
| int v17; // [sp+0h] [bp-18h]@1 | |
| v17 = a4; | |
| if ( !a3 ) | |
| goto LABEL_26; | |
| v4 = path_count_3744; | |
| if ( (unsigned __int8)path_count_3744 > 1u ) | |
| goto LABEL_30; | |
| v5 = (unsigned __int8)*a2; | |
| v6 = path_count_3744++ + 1; | |
| if ( v5 != 2 ) | |
| { | |
| if ( v5 != 3 ) | |
| goto LABEL_26; | |
| v7 = a1 - a3; | |
| v8 = (unsigned __int8)(v4 + 2); | |
| while ( 1 ) | |
| { | |
| --a3; | |
| if ( !a3 ) | |
| break; | |
| if ( v8 == 3 ) | |
| { | |
| path_count_3744 = v6; | |
| goto LABEL_30; | |
| } | |
| v9 = (unsigned __int8)(a2++)[1]; | |
| v8 = v9; | |
| v10 = v7 + a3; | |
| if ( v9 == 2 ) | |
| { | |
| path_count_3744 = v8; | |
| goto LABEL_12; | |
| } | |
| if ( v8 != 3 ) | |
| { | |
| path_count_3744 = 2; | |
| goto LABEL_26; | |
| } | |
| v6 = 2; | |
| } | |
| path_count_3744 = v6; | |
| LABEL_26: | |
| path_fail(); | |
| } | |
| v10 = a1; | |
| LABEL_12: | |
| if ( v10 <= 0x29 ) | |
| { | |
| v11 = 6 * v10; | |
| } | |
| else | |
| { | |
| v11 = v10 % 0x4C; | |
| if ( v10 % 0x4C ) | |
| v11 = v10 / 7; | |
| } | |
| if ( a3 == 1 ) | |
| goto LABEL_26; | |
| if ( (unsigned __int8)path_count_3737 > 2u ) | |
| goto LABEL_30; | |
| v12 = (unsigned __int8)a2[1]; | |
| ++path_count_3737; | |
| if ( v12 % 0x25 & 0xFF ) | |
| { | |
| if ( a3 == 2 ) | |
| goto LABEL_26; | |
| if ( (unsigned __int8)path_count_3716 > 2u ) | |
| LABEL_30: | |
| count_fail(); | |
| v13 = (unsigned __int8)a2[2]; | |
| ++path_count_3716; | |
| v14 = v11 + 26; | |
| v15 = a2 + 3; | |
| v16 = a3 - 3; | |
| if ( v13 % 0x75 > 0x1E ) | |
| path_c(v14, v15, v16); | |
| else | |
| path_a(v14, v15, v16, v17); | |
| } | |
| else | |
| { | |
| path_a(v11 - v12, a2 + 2, a3 - 2, v17); | |
| } | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment