[prev in list] [next in list] [prev in thread] [next in thread]
List: klee-dev
Subject: [klee-dev] Sorry, may i ask a question?
From: "=?utf-8?B?5pu+5p2w?=" <zyj183247166 () qq ! com>
Date: 2017-04-12 2:21:55
Message-ID: tencent_06F40DC9271277262CCA15CC () qq ! com
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
[Attachment #4 (text/plain)]
Hi,all
I am very sorry to disturb you. Really thanks for the work Of Prof. Cristian \
Cadar. KLEE is one strong tool for testing softwares and symbolic execution is very \
promising. When i use klee to run the follow program, which is a similar example \
about the Vulnerability in the dissertation of Prof. Cristian Cadar for the degree of \
doctor of philosophy.
the code of vulnerability existing in the function safe_addptr in the 32-bit \
version of HISTAR kernel : uintptr_t safe_addptr(int *of , uint64_t a, uint64_t b){
uintptr_t r=a+b;
if(r < a )
return r;
}
i rewrite a similar program as bellow.
#include<stdio.h> #include<malloc.h> #include <klee/klee.h> int main() { \
unsigned long long int a; unsigned long long int b; unsigned int c; \
klee_make_symbolic(&a,sizeof(a),"a"); klee_make_symbolic(&b,sizeof(b),"b"); \
c=a+b; if(c<a) { printf("yes \n"); } else if(c<b) { printf("xiaojie \n"); } else \
printf("no \n"); return 0; }
when using klee to run it. there are three paths.
My question is about the generated test case which i cannot understand.
root@sucof-virtual-machine:~/桌面/xiaojiework/klee_work# ktest-tool \
./klee-last/test000002.ktest ktest file : './klee-last/test000002.ktest'
args : ['overflowdetect_klee.bc']
num objects: 2
object 0: name: 'a'
object 0: size: 8
object 0: data: '\x01\x00FA\x00\x00\x00\x80'
object 1: name: 'b'
object 1: size: 8
object 1: data: '}_9~\x00\x00\x00\x00'
I understand "\x" is to express hexadecimal number. then what does \
the "}_9~" means in the red circle in the above picture ? I would very much \
appreciate your help.
[Attachment #5 (text/html)]
<div>Hi,all</div><div><div yne-bulb-block="paragraph" style="white-space: pre-wrap; \
font-size: 14px;"><span style=" font-size: 12px ; ; ; ; "> I am very sorry to \
disturb you. Really thanks for the work Of Prof. Cristian Cadar. KLEE is one strong \
tool for testing softwares and symbolic execution is very promising. When i use klee \
to run the follow program, which is a similar example about the </span><span style=" \
color: rgb(67, 67, 67); ; font-size: 12px; font-weight: bold; line-height: \
19.1875px; white-space: normal; background-color: rgb(242, 242, 242); ">Vulnerability \
</span><span style=" font-size: 12px ; ; ; ; ">in the dissertation of </span><span \
style=" color: rgb(102, 102, 102) ; ; ; ; ">Prof. Cristian Cadar for the degree of \
doctor of philosophy.</span></div></div><div yne-bulb-block="paragraph" \
style="white-space: pre-wrap; font-size: 14px;"><span style=" color: rgb(102, 102, \
102) ; ; ; ; "> the code of vulnerability existing in the </span><span style=" \
color: rgb(102, 102, 102) ; ; ; ; ">function </span><span style=" color: rgb(102, \
102, 102) ; ; ; ; "> safe_addptr in the 32-bit version of HISTAR kernel \
:</span></div><div yne-bulb-block="paragraph" style="white-space: pre-wrap; \
font-size: 14px;"><div style=" font-size: 14px; white-space: normal; color: rgb(70, \
70, 70) ; ; ; ; ; ; ">uintptr_t safe_addptr(int *of , uint64_t a, uint64_t \
b){</div><div style=" font-size: 14px; white-space: normal; color: rgb(70, 70, 70) ; \
; ; ; ; ; ">uintptr_t <wbr>r=a+b;</div><div style=" font-size: 14px; white-space: \
normal; color: rgb(70, 70, 70) ; ; ; ; ; ; ">if(r < a )</div><div style=" \
font-size: 14px; white-space: normal; color: rgb(70, 70, 70) ; ; ; ; ; ; ">return \
r;</div><div style=" font-size: 14px; white-space: normal; color: rgb(70, 70, 70) ; ; \
; ; ; ; ">}</div></div><div yne-bulb-block="paragraph" style="white-space: pre-wrap; \
font-size: 14px;"><span style=" color: rgb(102, 102, 102) ; ; ; ; "> i rewrite a \
similar program as bellow.<font editorwarp__="1" style=" display: inline; font-size: \
14px ; ; ; ; ; ; ; "><font editorwarp__="1" style="display: inline; \
background-color: rgb(188, 211, 229);"></font></font></span></div><font \
editorwarp__="1" style="display: inline; background-color: rgb(188, 211, 229);"><div \
yne-bulb-block="paragraph" style="display: block; background-color: rgb(188, 211, \
229);"><span style=" color: rgb(102, 102, 102) ; ; ; ; ; ; ; ; "><font \
editorwarp__="1" style=" display: inline; font-size: 14px ; ; ; ; ; ; ; \
"></font></span><font color="#464646" face="Microsoft YaHei, Helvetica Neue, \
SimSun"><span style="white-space: pre-wrap;">#include<stdio.h> \
#include<malloc.h> #include <klee/klee.h>
int main()
{
unsigned long long int a;
unsigned long long int b;
unsigned int c;</span></font><font color="#464646" face="Microsoft YaHei, \
Helvetica Neue, SimSun"><span style="white-space: pre-wrap;"> \
klee_make_symbolic(&a,sizeof(a),"a"); klee_make_symbolic(&b,sizeof(b),"b");
c=a+b;</span></font><font color="#464646" face="Microsoft YaHei, Helvetica Neue, \
SimSun"><span style="white-space: pre-wrap;"> if(c<a)
{
printf("yes \n");
}
else if(c<b)
{
printf("xiaojie \n");
}
else
printf("no \n");
return 0;
}</span></font></div><div yne-bulb-block="paragraph" style="display: block; \
background-color: rgb(188, 211, 229);"><font editorwarp__="1" style=" display: \
inline; font-size: 12px ; ; ; ; ; ; ; "><br></font></div><font editorwarp__="1" \
style=" display: inline; font-size: 12px ; ; ; ; ; ; ; "><div \
yne-bulb-block="paragraph" style=" display: block; background-color: rgba(0, 0, 0, \
0); font-size: 12px ; ; ; ; ; ; "><font editorwarp__="1" style="display: \
inline;"><font editorwarp__="1" style="display: inline;"> when \
using klee to run it. there are three paths.<font editorwarp__="1" style="display: \
inline;"></font></font></font><br></div><div yne-bulb-block="paragraph" style=" \
display: block; background-color: rgba(0, 0, 0, 0); font-size: 12px ; ; ; ; ; ; \
"><font editorwarp__="1" style="display: inline;"><font editorwarp__="1" \
style="display: inline;"> My question is about the generated test case \
which i cannot understand.</font></font></div><div yne-bulb-block="paragraph" style=" \
display: block; background-color: rgba(0, 0, 0, 0); font-size: 12px ; ; ; ; ; ; \
"><font editorwarp__="1" style="display: inline;"><font editorwarp__="1" \
style="display: inline;"><br></font></font></div><div yne-bulb-block="paragraph" \
style=" display: block; background-color: rgba(0, 0, 0, 0); font-size: 12px ; ; ; ; ; \
; "></div><div yne-bulb-block="paragraph" style=" display: block; background-color: \
rgba(0, 0, 0, 0); font-size: 12px ; ; ; ; ; ; "><div yne-bulb-block="paragraph" \
style="background-color: rgba(0, 0, 0, \
0);">root@sucof-virtual-machine:~/桌面/xiaojiework/klee_work# ktest-tool \
./klee-last/test000002.ktest</div><div yne-bulb-block="paragraph" \
style="background-color: rgba(0, 0, 0, 0);">ktest file : \
'./klee-last/test000002.ktest'</div><div yne-bulb-block="paragraph" \
style="background-color: rgba(0, 0, 0, 0);">args : \
['overflowdetect_klee.bc']</div><div yne-bulb-block="paragraph" \
style="background-color: rgba(0, 0, 0, 0);">num objects: 2</div><div \
yne-bulb-block="paragraph" style="background-color: rgba(0, 0, 0, 0);">object \
0: name: 'a'</div><div yne-bulb-block="paragraph" style="background-color: \
rgba(0, 0, 0, 0);">object 0: size: 8</div><div \
yne-bulb-block="paragraph" style="background-color: rgba(0, 0, 0, 0);">object \
0: data: '\x01\x00FA\x00\x00\x00\x80'</div><div yne-bulb-block="paragraph" \
style="background-color: rgba(0, 0, 0, 0);">object 1: name: \
'b'</div><div yne-bulb-block="paragraph" style="background-color: rgba(0, 0, 0, \
0);">object 1: size: 8</div><div yne-bulb-block="paragraph" \
style="background-color: rgba(0, 0, 0, 0);">object 1: data: \
'}_9~\x00\x00\x00\x00'</div><div><br></div></div><div yne-bulb-block="paragraph" \
style=" display: block; background-color: rgba(0, 0, 0, 0); font-size: 12px ; ; ; ; ; \
; "><font editorwarp__="1" style="display: inline;"> <font editorwarp__="1" \
style="display: inline;"></font> <font editorwarp__="1" style="display: \
inline;"> I</font> understand "\x" is to <font editorwarp__="1" \
style="display: inline;"><font editorwarp__="1" style="display: \
inline;">express hexadecimal number. then what does the "}_9~" means in the red \
circle in the above picture ?</font></font></font></div></font></font><div \
yne-bulb-block="paragraph" style=" display: block; background-color: rgba(0, 0, 0, \
0); font-size: 12px ; ; ; ; ; ; "><font editorwarp__="1" style="display: inline; \
background-color: rgb(188, 211, 229);"><font editorwarp__="1" style=" display: \
inline; font-size: 12px ; ; ; ; ; ; ; "><font editorwarp__="1" style="display: \
inline;"><font editorwarp__="1" style="display: inline;"><font editorwarp__="1" \
style="display: inline;"><font editorwarp__="1" style="display: inline;"><font \
editorwarp__="1" style="display: inline;"> \
</font></font></font></font></font></font></font><span style="white-space: \
pre-wrap; background-color: rgb(255, 255, 255);">I would very much appreciate your \
help.<font editorwarp__="1" style="display: inline;"></font></span></div><h2 \
style=" margin: 0px; padding: 0px; border: 0px; outline: 0px; font-size: 1.16em; \
color: rgb(67, 67, 67); ; line-height: 24px; background-color: rgb(242, 242, 242); \
"><span class="keyword" style="margin: 0px 1.5em 0px 0px; padding: 0px; border: 0px; \
outline: 0px; font-size: 1.4258em; max-width: 70%; overflow: hidden; text-overflow: \
ellipsis; white-space: nowrap; display: inline-block; height: \
1.2em;"></span></h2><div yne-bulb-block="paragraph"><div style=" color: rgb(70, 70, \
70) ; ; ; ; ; ; ; "></div></div>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic