實驗二：klee處理未建模函數和處理error的方式

本文轉載自查看原文 2017-05-10 16:51 1489 軟件分析技術

首先，能夠分析klee源碼固然重要。但是目前尚未到那個地步。我按照我的過程，記錄和分析我所做的實驗。

結論性內容是：

1、klee處理printf傳入符號值的情形時，報為error，不會將符號值具體化以后再調用printf進行具體執行。

2、klee處理error的時候，如果多條路徑覆蓋該error，則只報一次該error，並且只生成一個測試用例。

3、klee符號執行時的posix-runtime選項為命令行建模提供支持，uclibc則對atoi等c標准庫的函數進行建模。

（如果使用了Posix-rutime選項，但是沒有對命令行建模（--sym-args和--sym-arg選項），則會報錯；如果沒有使用uclibc選項，那么klee符號執行過程會提示atoi等函數是external，無法處理。）

示例代碼1:

#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <assert.h>
#include <klee/klee.h>
int main(int argc, char* argv[]) {
    int result = argc > 1 ? atoi(argv[1]) : 0;
    printf("result：%d\n",result);
    if (result == 42)
    {
    printf("yes\n");
    klee_assert(0);
    }
   // printf("result：%d\n",result);
}

示例代碼2：

#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <assert.h>
#include <klee/klee.h>
int main(int argc, char* argv[]) {
    int result = argc > 1 ? atoi(argv[1]) : 0;
    //printf("result：%d\n",result);
    if (result == 42)
    {
    printf("yes\n");
    klee_assert(0);
    }
    printf("result：%d\n",result);
}

運行腳本：

clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c
klee --optimize --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3

運行結果：

修改前

klee@ubuntu:~/kleeexperiment/modeltest$ clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c
klee@ubuntu:~/kleeexperiment/modeltest$ klee --optimize --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3
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/modeltest/klee-out-12"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 62967648)
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: printf(51779744, 0)
result：0
result：0
result：0
result：0
result：0
result：0
result：0
result：0
KLEE: ERROR: /home/klee/kleeexperiment/modeltest/test2.c:19: external call with symbolic argument: printf
KLEE: NOTE: now ignoring this error at this location
result：0
result：0
result：0
result：0
result：0
result：0
result：0
result：-9
result：-9
result：0
result：0
result：-9
result：0
result：9
result：-99
result：9
result：9
result：9
result：9
result：9
result：9
result：9
result：99
result：99
result：99
result：99
result：999

KLEE: done: total instructions = 6238
KLEE: done: completed paths = 68
KLEE: done: generated tests = 36

修改后：

klee@ubuntu:~/kleeexperiment/modeltest$ clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c
klee@ubuntu:~/kleeexperiment/modeltest$ klee --optimize --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3
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/modeltest/klee-out-11"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 58818256)
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: printf(55045792, 0)
result：0
result：0
result：0
result：0
result：0
result：0
result：0
KLEE: ERROR: /home/klee/kleeexperiment/modeltest/test2.c:25: external call with symbolic argument: printf
KLEE: NOTE: now ignoring this error at this location
result：0
result：0
result：0
result：0
result：0
result：0
result：0
result：0
KLEE: WARNING ONCE: calling external: puts(60211056)
yes
KLEE: ERROR: /home/klee/kleeexperiment/modeltest/test2.c:23: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location
result：9
result：0
result：-9
result：9
result：0
result：9
result：0
result：99
result：9
result：-9
result：9
yes
yes
yes
result：9
result：9
result：-9
result：9
result：-99
yes
result：99
result：99
result：99
result：999

KLEE: done: total instructions = 6381
KLEE: done: completed paths = 73
KLEE: done: generated tests = 37

可以看到結果不一樣：后面比前面多生成了一個測試用例（36到37），並且新增匯報了一個error，就是assertion。為什么會多一個呢？因為：

printf放在了if(result==42)的前面。當符號值傳遞給printf的時候，klee可能有兩種做法，一種是放棄分析，另外一種是將符號值具體化（目前我的猜測，繼續往下看）。

如果是放棄分析，klee就不可能沿着該路徑往后面走了；

如果是符號值具體化，klee也不可能考慮到后續有if(result==42)的語句，而故意將其具體化為42。因此，無論如何就無法檢測到klee_assert的錯誤，即klee都不可能再對符號result添加==42的約束，從而跳入到后面的if語句中，繼續符號執行。

針對該現象繼續進行解釋：即klee處理printf傳入符號值的時候，是符號值具體化呢，還是放棄分析呢？我們就結合這個實例來探討一下：

一，修改前和修改后的測試用例情況和路徑覆蓋情況對比：（說明針對一個error只產生一個測試用例）

KLEE: done: completed paths = 68

KLEE: done: generated tests = 36

KLEE: done: completed paths = 73

KLEE: done: generated tests = 37

此外，在符號執行過程中，輸出了五次yes，說明有五條路徑覆蓋了if（result==42）。printf（“yes”）的參數不是符號值，因此可以直接執行。

現象說明：將printf從if(result==42)之前移動到之后以后，原有的68條路徑中，有五條路徑的約束還能夠滿足result==42，因此新增了五條路徑（從68變為73）。

但是為什么測試用例只增加了一個呢？這是因為，五條路徑都報錯的話，klee只匯報一次error，同時只從產生一個覆蓋該error的測試用例。

你若不信的話，我預言，你把klee_assert去掉，那么路徑肯定是從68增加到73，然后測試用例也增加五個。我們試一試。

驗證代碼是：

修改前：

int main(int argc, char* argv[]) {

int result = argc > 1 ? atoi(argv[1]) : 0;

printf("result：%d\n",result);

if (result == 42)

{

printf("yes\n");

//klee_assert(0);

}

//printf("result：%d\n",result);

}

修改后：

int main(int argc, char* argv[]) {

int result = argc > 1 ? atoi(argv[1]) : 0;

//printf("result：%d\n",result);

if (result == 42)

{

printf("yes\n");

//klee_assert(0);

}

printf("result：%d\n",result);

}

輸出信息：

修改前：

klee@ubuntu:~/kleeexperiment/modeltest$ clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c

klee@ubuntu:~/kleeexperiment/modeltest$ klee --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3

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/modeltest/klee-out-17"

KLEE: Using STP solver backend

KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 47881104)

KLEE: WARNING ONCE: calling __user_main with extra arguments.

KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.

KLEE: WARNING ONCE: calling external: printf(65297728, 0)

result：0

KLEE: ERROR: /home/klee/kleeexperiment/modeltest/test2.c:19: external call with symbolic argument: printf

KLEE: NOTE: now ignoring this error at this location

result：0

result：-9

result：0

result：-9

result：9

result：-99

result：9

result：99

result：9

result：99

result：999

KLEE: done: total instructions = 11514

KLEE: done: completed paths = 68

KLEE: done: generated tests = 36

修改后：

klee@ubuntu:~/kleeexperiment/modeltest$ clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c

klee@ubuntu:~/kleeexperiment/modeltest$ klee --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3

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/modeltest/klee-out-16"

KLEE: Using STP solver backend

KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 31737040)

KLEE: WARNING ONCE: calling __user_main with extra arguments.

KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.

KLEE: WARNING ONCE: calling external: printf(44028960, 0)

result：0

KLEE: ERROR: /home/klee/kleeexperiment/modeltest/test2.c:25: external call with symbolic argument: printf

KLEE: NOTE: now ignoring this error at this location

result：0

result：-9

result：0

result：9

result：-9

result：0

result：9

result：-99

result：-9

result：9

yes

result：42

result：9

yes

result：42

result：9

yes

result：42

result：9

result：99

yes

result：42

result：99

yes

result：42

result：99

result：999

KLEE: done: total instructions = 11648

KLEE: done: completed paths = 73

KLEE: done: generated tests = 41

驗證了我的推斷。

問題：為什么路徑數目和測試用例不一致呢？可能是由於求解器的原因，一些路徑的約束無法計算出來（繼續下面看，會發現該程序不是因為這個原因。）

二、為什么路徑數目和測試用例不一致呢？klee處理printf傳入符號值，究竟是具體化符號值，還是直接放棄分析，報出error？

進一步修改程序：

int main(int argc, char* argv[]) {
    int result = argc > 1 ? atoi(argv[1]) : 0;
    //printf("result：%d\n",result);
    if (result == 42)
    {
    printf("yes,");//修改的地方是，加了一個逗號。
    klee_assert(0);
    }
    printf("result：%d\n",result);
}

klee符號執行結果：

klee@ubuntu:~/kleeexperiment/modeltest$ clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c
klee@ubuntu:~/kleeexperiment/modeltest$ klee --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3
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/modeltest/klee-out-18"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 75566416)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: printf(66063584, 0)
result：0
result：0
result：0
result：0
result：0
KLEE: ERROR: /home/klee/kleeexperiment/modeltest/test2.c:25: external call with symbolic argument: printf
KLEE: NOTE: now ignoring this error at this location
result：0
result：0
result：0
result：0
result：0
result：0
result：0
result：0
result：0
result：0
result：0
result：-9
result：0
result：9
result：0
result：-9
result：9
result：-99
result：-9
result：9
KLEE: ERROR: /home/klee/kleeexperiment/modeltest/test2.c:23: ASSERTION FAIL: 0
KLEE: NOTE: now ignoring this error at this location
yes,result：9
result：9
result：9
yes,yes,result：9
result：9
result：99
result：99
yes,yes,result：99
result：99
result：999

KLEE: done: total instructions = 11623
KLEE: done: completed paths = 73
KLEE: done: generated tests = 37

首先，輸出的信息都是符號執行的過程中輸出的。產生的測試用例都是符號執行結束以后產生的。根據我前面的論證，當覆蓋同一個錯誤的時候，只報一次error，只產生一個測試用例。所以，五個yes，也就說明實際能夠產生測試用例的路徑是41條。那么也就說明，符號執行過程中應該輸出41組值。我們數一下。一共是40組值（注意，yes,單獨算一組）。為什么？？？

這個時候我進一步摸索和修改（也是誤打誤撞出來）

版本一程序

版本二程序

版本三程序

int main(int argc, char* argv[]) {
    int result = argc > 1 ? atoi(argv[1]) : 0;
    //printf("result：%d\n",result);
    if (result == 42)
    {
    printf("yes,");
    //klee_assert(0);
    }
    //printf("result：%d\n",result);
}

int main(int argc, char* argv[]) {
    int result = argc > 1 ? atoi(argv[1]) : 0;
    //printf("result：%d\n",result);
    if (result == 42)
    {
    printf("yes,");
    klee_assert(0);
    }
    //printf("result：%d\n",result);
}

int main(int argc, char* argv[]) {
    int result = argc > 1 ? atoi(argv[1]) : 0;
    printf("result：%d\n",result);
    if (result == 42)
    {
    printf("yes,");
    //klee_assert(0);
    }
    //printf("result：%d\n",result);
}

輸出結果：

版本一	版本二

版本三：

klee@ubuntu:~/kleeexperiment/modeltest$ clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test2.c
klee@ubuntu:~/kleeexperiment/modeltest$ klee --libc=uclibc --posix-runtime test2.bc --sym-args 0 1 3
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/modeltest/klee-out-21"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 60923696)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: calling external: printf(76818928, 0)
result：0
result：0
result：0
result：0
result：0
result：0
result：0
KLEE: ERROR: /home/klee/kleeexperiment/modeltest/test2.c:19: external call with symbolic argument: printf
KLEE: NOTE: now ignoring this error at this location
result：0
result：0
result：0
result：0
result：0
result：0
result：0
result：0
result：0
result：-9
result：9
result：0
result：0
result：-9
result：9
result：9
result：9
result：9
result：99
result：-9
result：9
result：9
result：9
result：-99
result：99
result：99
result：99
result：999

KLEE: done: total instructions = 11514
KLEE: done: completed paths = 68
KLEE: done: generated tests = 36

比較一下版本一和版本二，可以看出，版本二由於assert原因，73條路徑中五條覆蓋assert，所以只生成69個測試用例，匯報一次error，error對應一個測試用例。

比較一下版本二和版本三，可以看出，版本三由於printf放在了if(result==42)的前面，無論是printf傳入具體值，還是printf傳入符號值（符號值具體化或者klee放棄分析，見前述分析），后續覆蓋if(result==42)的路徑都不會被滿足和分析，沒有yes被輸出。同時，覆蓋的路徑條數為68。這也說明，if點前一共有68條路徑，如果沒有printf影響，其中只有五條的約束在添加(result==42)以后，還能夠滿足，從而覆蓋到if(result==42)分支內部內容。

比較一下版本一和版本三，可以看出，符號執行過程中的輸出為35組數據（數一數輸出的result信息的個數），但是生成了36個測試用例，報了一個error，我們看了一下，error的具體內容是：

同時配套生成了一個error的測試用例。但是符號執行過程中輸出為35組數據，這也就說明了，klee處理printf傳入符號值的時候，沒有將其具體化以后再調用printf，而是直接報error，並且放棄分析。

這也說明了：版本三程序的一共68條路徑中，有（68-35）條路徑因為執行printf時傳入符號值，均為error，但是只報出一個error，最后也只產生一個測試用例覆蓋該條路徑。這也是前述41個測試用例和40組輸出數據的原因。

我們查看一下測試用例的內容和用該測試用例重新運行程序，可以看出，由於printf傳入符號值的這種error類型，是klee自身不能處理的情況，而不是我們一般程序運行時的內存錯誤等，所以該測試用例下重新運行該程序，不會報錯。result輸出值為0。那為什么還要生成該測試用例呢，因為需要覆蓋該error所在路徑。

klee@ubuntu:~/kleeexperiment/modeltest$ export LD_LIBRARY_PATH=/home/klee/xiaojiework/klee-xiaojie/build/debug/lib/:$LD_LIBRARY_PATH
klee@ubuntu:~/kleeexperiment/modeltest$ gcc -L /home/klee/xiaojiework/klee-xiaojie/build/debug/lib/ test2.c -lkleeRuntest
klee@ubuntu:~/kleeexperiment/modeltest$ ktest-tool klee-last/test000010.ktestktest file : 'klee-last/test000010.ktest'
args       : ['test2.bc', '--sym-args', '0', '1', '3']
num objects: 3
object    0: name: 'n_args'
object    0: size: 4
object    0: data: '\x01\x00\x00\x00'
object    1: name: 'arg0'
object    1: size: 4
object    1: data: '+0\x00\x00'
object    2: name: 'model_version'
object    2: size: 4
object    2: data: '\x01\x00\x00\x00'
klee@ubuntu:~/kleeexperiment/modeltest$ KTEST_FILE=klee-last/test000010.ktest ./a.out
result：0

結論性的東西往往不容易獲得。分析完畢！

免責聲明！

本站轉載的文章為個人學習借鑒使用，本站對版權不負任何法律責任。如果侵犯了您的隱私權益，請聯系本站郵箱yoyou2525@163.com刪除。

猜您在找 以全局監聽的方式處理img的error事件 Golang 中處理 error 的幾種方式數據建模（1）-數據預處理超時未支付訂單處理 [PHP]日志處理error_log()函數和配置使用實驗一：使用符號執行工具klee對軟件進行破解（來自於klee官網） PHP錯誤處理函數set_error_handler()的用法數據處理以及建模完整流程數學建模教程（六）——用Excel處理lingo數據 VBS中對Error的處理