原文地址：https://gitlab.com/Manouchehri/Matryoshka-Stage-2/blob/master/stage2.md
實驗用代碼下載地址：https://gitlab.com/Manouchehri/Matryoshka-Stage-2/blob/master/stage2.md
下面是我自己的實驗進程：
2017-05-09 16:18:09
1. linux 64位提權並執行stage2.bin文件
可以看到，輸入錯誤的密碼時，會提示Try again...
2. 對stage2.bin文件利用IDA拍攝6.6版本定位出main函數
程序入口點start看到：
查詢一下__libc_start_main函數的功能：
int __libc_start_main(int *(main) (int, char * *, char * *), int argc, char * * ubp_av, void (*init) (void), void (*fini) (void), void (*rtld_fini) (void), void (* stack_end));
第一個函數參數是main，也就是二進制程序中的mov rdi, offset sub_4006F2。
查看sub_4006F2的函數調用流程圖，可以確定這個是main函數。因為調用流程里為false的時候，會輸出Try again；沒有輸入的時候，輸出pass等等。圖比較大，這里不粘貼了。
3.反匯編出C代碼。
可以按F5，使用Hex-Rays Decompiler反匯編出main函數的代碼。也可以點擊IDA的File>produce file>create C File。我們使用后者，生成的C文件的內容如下：、
/* This file has been generated by the Hex-Rays decompiler. Copyright (c) 2007-2014 Hex-Rays <info@hex-rays.com> Detected compiler: GNU C++ */ #include <defs.h> //------------------------------------------------------------------------- // Function declarations int init_proc(); // ssize_t write(int fd, const void *buf, size_t n); // size_t strlen(const char *s); // int fprintf(FILE *stream, const char *format, ...); // int __gmon_start__(void); weak // size_t fwrite(const void *ptr, size_t size, size_t n, FILE *s); signed int sub_400590(); int sub_4005C0(); signed int sub_400600(); int sub_400620(); __int64 __fastcall sub_40064D(const char *a1); int __fastcall sub_4006F2(int a1, __int64 a2); void term_proc(); //------------------------------------------------------------------------- // Data declarations char byte_400A60[] = { '6' }; // weak FILE *stdout; // idb char byte_608068; // weak // extern _UNKNOWN _gmon_start__; weak //----- (00000000004004C8) ---------------------------------------------------- int init_proc() { _UNKNOWN *v0; // rax@1 v0 = &_gmon_start__; if ( &_gmon_start__ ) LODWORD(v0) = __gmon_start__(); return (signed int)v0; } // 400540: using guessed type int __gmon_start__(void); //----- (0000000000400560) ---------------------------------------------------- #error "400566: positive sp value has been found (funcsize=3)" //----- (0000000000400590) ---------------------------------------------------- signed int sub_400590() { return 7; } //----- (00000000004005C0) ---------------------------------------------------- int sub_4005C0() { return 0; } //----- (0000000000400600) ---------------------------------------------------- signed int sub_400600() { signed int result; // eax@2 if ( !byte_608068 ) { result = sub_400590(); byte_608068 = 1; } return result; } // 608068: using guessed type char byte_608068; //----- (0000000000400620) ---------------------------------------------------- int sub_400620() { return sub_4005C0(); } // 400620: could not find valid save-restore pair for rbp //----- (000000000040064D) ---------------------------------------------------- __int64 __fastcall sub_40064D(const char *a1) { char buf; // [sp+13h] [bp-Dh]@2 int v3; // [sp+14h] [bp-Ch]@1 int v4; // [sp+18h] [bp-8h]@1 int v5; // [sp+1Ch] [bp-4h]@1 fwrite("Good good!\n", 1uLL, 0xBuLL, stdout); v3 = 0; v4 = 0; v5 = strlen(a1); while ( v3 <= 25183 ) { buf = byte_400A60[(signed __int64)v3] ^ a1[v4 % v5]; write(2, &buf, 1uLL); ++v3; ++v4; } return 0LL; } //----- (00000000004006F2) ---------------------------------------------------- int __fastcall sub_4006F2(int a1, __int64 a2) { int result; // eax@2 __int64 v3; // rbx@10 signed int v4; // [sp+1Ch] [bp-14h]@4 if ( a1 == 2 ) { if ( 42 * (strlen(*(const char **)(a2 + 8)) + 1) != 504 ) goto LABEL_31; v4 = 1; if ( **(_BYTE **)(a2 + 8) != 80 ) v4 = 0; if ( 2 * *(_BYTE *)(*(_QWORD *)(a2 + 8) + 3LL) != 200 ) v4 = 0; if ( **(_BYTE **)(a2 + 8) + 16 != *(_BYTE *)(*(_QWORD *)(a2 + 8) + 6LL) - 16 ) v4 = 0; v3 = *(_BYTE *)(*(_QWORD *)(a2 + 8) + 5LL); if ( v3 != 9 * strlen(*(const char **)(a2 + 8)) - 4 ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 1LL) != *(_BYTE *)(*(_QWORD *)(a2 + 8) + 7LL) ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 1LL) != *(_BYTE *)(*(_QWORD *)(a2 + 8) + 10LL) ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 1LL) - 17 != **(_BYTE **)(a2 + 8) ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 3LL) != *(_BYTE *)(*(_QWORD *)(a2 + 8) + 9LL) ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 4LL) != 105 ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 2LL) - *(_BYTE *)(*(_QWORD *)(a2 + 8) + 1LL) != 13 ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 8LL) - *(_BYTE *)(*(_QWORD *)(a2 + 8) + 7LL) != 13 ) v4 = 0; if ( v4 ) result = sub_40064D(*(const char **)(a2 + 8)); else LABEL_31: result = fprintf(stdout, "Try again...\n", a2); } else { result = fprintf(stdout, "Usage: %s <pass>\n", *(_QWORD *)a2, a2); } return result; } //----- (0000000000400A34) ---------------------------------------------------- void term_proc() { ; } #error "There were 1 decompilation failure(s) on 9 function(s)"
4. 既然是破解，我們只需要在通過驗證的地方，做一些改動。所以，圍繞main函數（這里是sub_4006F2函數）我們去除所有不想干的代碼，提取出主要流程，比如，sub_40064D實現的功能是在驗證通過的時候，輸出密碼驗證通過的信息，那么我就直接用printf("good!")進行代替，以簡化破解難度。改動后的代碼是：
#include <defs.h> int __fastcall sub_4006F2(int a1, __int64 a2) { int result; // eax@2 __int64 v3; // rbx@10 signed int v4; // [sp+1Ch] [bp-14h]@4 if ( a1 == 2 ) { if ( 42 * (strlen(*(const char **)(a2 + 8)) + 1) != 504 ) goto LABEL_31; v4 = 1; if ( **(_BYTE **)(a2 + 8) != 80 ) v4 = 0; if ( 2 * *(_BYTE *)(*(_QWORD *)(a2 + 8) + 3LL) != 200 ) v4 = 0; if ( **(_BYTE **)(a2 + 8) + 16 != *(_BYTE *)(*(_QWORD *)(a2 + 8) + 6LL) - 16 ) v4 = 0; v3 = *(_BYTE *)(*(_QWORD *)(a2 + 8) + 5LL); if ( v3 != 9 * strlen(*(const char **)(a2 + 8)) - 4 ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 1LL) != *(_BYTE *)(*(_QWORD *)(a2 + 8) + 7LL) ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 1LL) != *(_BYTE *)(*(_QWORD *)(a2 + 8) + 10LL) ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 1LL) - 17 != **(_BYTE **)(a2 + 8) ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 3LL) != *(_BYTE *)(*(_QWORD *)(a2 + 8) + 9LL) ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 4LL) != 105 ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 2LL) - *(_BYTE *)(*(_QWORD *)(a2 + 8) + 1LL) != 13 ) v4 = 0; if ( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 8LL) - *(_BYTE *)(*(_QWORD *)(a2 + 8) + 7LL) != 13 ) v4 = 0; if ( v4 ) printf("good\n"); else LABEL_31: result = fprintf(stdout, "Try again...\n", a2); } else { result = fprintf(stdout, "Usage: %s <pass>\n", *(_QWORD *)a2, a2); } return result; }
5. 當然，這離可執行還差很遠。我們還要改動為KLEE能夠分析的形式。但是在滿足klee能夠分析之前，我們要先將其改動為可以編譯執行的C文件。
我們一邊用經驗去改，一邊用編譯器同時編譯，根據編譯不通過所提示的錯誤進行改動。
主要改動如下：
- 第一處
將defs.h文件從IDA的目錄中復制到test.c（改動代碼放置位置）的相同目錄中去。Defs.h文件中保存的是IDA生成的C文件中相關類型的定義。
- 第二處：
../src/test.c:35:5: warning: second argument of ‘main’ should be ‘char **’ [-Wmain]
int main(int a1, __int64 a2)
將__int64改為char**（這是經驗）
- 第三處：
../src/test.c:71:7: warning: implicit declaration of function ‘sub_40064D’ [-Wimplicit-function-declaration]
result = sub_40064D(*(const char **)(a2 + 8));
^
../src/test.c:74:7: warning: too many arguments for format [-Wformat-extra-args]
result = fprintf(stdout, "Try again...\n", a2);
^
../src/test.c:78:5: warning: format ‘%s’ expects argument of type ‘char *’, but argument 3 has type ‘uint64’ [-Wformat=]
result = fprintf(stdout, "Usage: %s <pass>\n", *(_QWORD *)a2, a2);
所以將fprintf改為printf。並且去掉return result。
- 第四處
代碼中有大量的類型轉換，我們在IDA對sub_4006F2按F5彈出的反匯編后C代碼的窗口中，右鍵選擇Hiden casts.
可以看到，之前的QWORD *和BYTE *等IDA中的類型，都去除了。所以，再次改動后的代碼是：
#include <stdio.h> #include <string.h> #include <stdlib.h> #include "defs.h" int main(int a1, char ** a2) { __int64 v3; // rbx@10 signed int v4; // [sp+1Ch] [bp-14h]@4 if ( a1 == 2 ) { if ( 42 * (strlen(*(a2 + 8)) + 1) != 504 ) goto LABEL_31; v4 = 1; if ( **(a2 + 8) != 80 ) v4 = 0; if ( 2 * *(*(a2 + 8) + 3LL) != 200 ) v4 = 0; if ( **(a2 + 8) + 16 != *(*(a2 + 8) + 6LL) - 16 ) v4 = 0; v3 = *(*(a2 + 8) + 5LL); if ( v3 != 9 * strlen(*(a2 + 8)) - 4 ) v4 = 0; if ( *(*(a2 + 8) + 1LL) != *(*(a2 + 8) + 7LL) ) v4 = 0; if ( *(*(a2 + 8) + 1LL) != *(*(a2 + 8) + 10LL) ) v4 = 0; if ( *(*(a2 + 8) + 1LL) - 17 != **(a2 + 8) ) v4 = 0; if ( *(*(a2 + 8) + 3LL) != *(*(a2 + 8) + 9LL) ) v4 = 0; if ( *(*(a2 + 8) + 4LL) != 105 ) v4 = 0; if ( *(*(a2 + 8) + 2LL) - *(*(a2 + 8) + 1LL) != 13 ) v4 = 0; if ( *(*(a2 + 8) + 8LL) - *(*(a2 + 8) + 7LL) != 13 ) v4 = 0; if ( v4 ) printf("good\n"); else LABEL_31: printf("Try again...\n"); } else { printf("Usage: %s <pass>\n", *a2); } return 0; }
6. 使用KLEE進行分析
改動
if ( v4 ) printf("good\n");
為：
if ( v4 ){ printf("good\n"); klee_assert(0); }
並且添加兩個頭文件：
#include <assert.h>
#include <klee/klee.h>
下一步使用KLEE進行符號執行：KLEE官網見（http://klee.github.io/）
需要大家自行准備一下KLEE的知識。這里不再贅述。
執行下面的腳本。test.c為可以編譯通過的c文件。test-klee.c為添加klee_assert等內容以后的文件
clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test-klee.c klee --optimize --libc=uclibc --posix-runtime test-klee.bc --sym-arg 100
結果是：
出現了問題，沒有像官網那樣，報assertion的錯誤，而且探尋的路徑只有一條。究竟是怎么回事？？？
7. 問題所在。
經過一系列研究，才發現問題的所在。
首先，int a1,char **a2是main函數中用於接收命令行信息的參數。a1是命令行輸入的字符串的個數。a2[0]就是程序名稱。a2[1]是程序后的第一個參數。
比如，你輸入stage2.bin “123”，那么傳入test.c中main函數的，就是a1為2，a2為char**類型，包含兩個字符串，分別是“stage2.bin”和“123”。
所以，a2[1]存儲的是密碼字符串。但是我們反匯編出的程序反復處理的是*(a2+8)位置的字符串。這也是klee發現out of bound pointer的原因。
8.問題是如何導致的？又如何解決？
首先，明確一個問題。
如果a2是char **類型，那么*(a2+1)和a2[1]是一樣的。因為char **是char *的指針，a2+1會自動解釋為真正a2的地址值加上8（也就是8個字節）。
如果a2是__int64類型，那么*(a2+8)和a2[1]的值是相等的。當然，要對a2+8先cast為char **類型以后，才能用*取值。
這是因為C編譯器對a2+n計算的處理是這樣做的。
如果a2是int類型，那么就是簡單+n。
如果a2是指針類型，則加上a2指向的對象大小*n。比如,a2是char**類型的時候，a2+1，就是a2+1*(sizeof(char*))。由於64位程序下指針類型都是64位，即8個字節。所以a2+1的真正計算值是a2值+8。
C語言的cast特別多。對cast機制，可以自行補課。這里不再贅述。
我的錯誤是：
一開始反匯編出的代碼，將a2作為__int64類型處理，所以代碼中用
( *(_BYTE *)(*(_QWORD *)(a2 + 8) + 1LL)
表示a2[1][1]。也就是將__int64類型的地址a2，將其作為char**類型的時候，計算a2[1][1]的正確過程。
我在后續將反匯編出的C代碼立求編譯通過的時候，簡單的在main函數括號內，將a2的類型改正為cahr**了，但是后面計算a2[1][1]的方式還沒有變。
這就是錯誤的原因。
正確的做法：在IDA F5反匯編出的代碼窗口，右鍵main函數括號內的a2，選擇set lvar type為char **a2。可以看到main函數的代碼為：
int __fastcall sub_4006F2(int a1, char **a2) { int result; // eax@2 __int64 v3; // rbx@10 signed int v4; // [sp+1Ch] [bp-14h]@4 if ( a1 == 2 ) { if ( 42 * (strlen(a2[1]) + 1) != 504 ) goto LABEL_31; v4 = 1; if ( *a2[1] != 80 ) v4 = 0; if ( 2 * a2[1][3] != 200 ) v4 = 0; if ( *a2[1] + 16 != a2[1][6] - 16 ) v4 = 0; v3 = a2[1][5]; if ( v3 != 9 * strlen(a2[1]) - 4 ) v4 = 0; if ( a2[1][1] != a2[1][7] ) v4 = 0; if ( a2[1][1] != a2[1][10] ) v4 = 0; if ( a2[1][1] - 17 != *a2[1] ) v4 = 0; if ( a2[1][3] != a2[1][9] ) v4 = 0; if ( a2[1][4] != 105 ) v4 = 0; if ( a2[1][2] - a2[1][1] != 13 ) v4 = 0; if ( a2[1][8] - a2[1][7] != 13 ) v4 = 0; if ( v4 ) result = sub_40064D(a2[1]); else LABEL_31: result = fprintf(stdout, "Try again...\n", a2); } else { result = fprintf(stdout, "Usage: %s <pass>\n", *a2, a2); } return result; }
可以看到，這才是正確的代碼。之前對a2的類型改動以后，沒有在代碼中對計算a2[1]的方式進行改動。還是按照a2為__int64類型時的計算方式。
9. 計算出軟件密鑰。
執行前述的腳本：
klee@ubuntu:~/kleeexperiment/Keygenningwithklee/stage2$ sh ./xiaojie.sh KLEE: NOTE: Using klee-uclibc : /usr/local/lib/x86_64-linux-gnu/klee/runtime/klee-uclibc.bca KLEE: NOTE: Using model: /usr/local/lib/x86_64-linux-gnu/klee/runtime/libkleeRuntimePOSIX.bca KLEE: output directory is "/home/klee/kleeexperiment/Keygenningwithklee/stage2/klee-out-0" KLEE: Using STP solver backend KLEE: WARNING: undefined reference to function: puts KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 35075632) KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8. KLEE: WARNING ONCE: calling external: puts(46355200) Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Good good! Try again... KLEE: ERROR: /home/klee/kleeexperiment/Keygenningwithklee/stage2/main.c:42: ASSERTION FAIL: 0 KLEE: NOTE: now ignoring this error at this location Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... Try again... KLEE: done: total instructions = 5619 KLEE: done: completed paths = 102 KLEE: done: generated tests = 102 klee@ubuntu:~/kleeexperiment/Keygenningwithklee/stage2$
生成的文件中，test000027.assert.err是klee_assert報錯的位置。其實也就是密碼驗證通過的位置。查看第27個測試用例的詳細內容：
可以看到Pandi_panda為密鑰。
我們驗證一下，可以看到通過驗證了。
