[prev in list] [next in list] [prev in thread] [next in thread]
List: klee-dev
Subject: [klee-dev] =?utf-8?b?562U5aSNOiAgU29ycnksIG1heSBpIGFzayBhIHF1ZXN0?= =?utf-8?q?ion=3F?=
From: Xuzhijian <xuzhijian () huawei ! com>
Date: 2017-04-13 1:15:52
Message-ID: FF8ACB314915C940AFE69F0DDD9A901C01251EC159 () dggeml512-mbs ! china ! huawei ! com
[Download RAW message or body]
[Attachment #2 (text/plain)]
If the character is visible, then klee will show it directly, otherwise, it will show \
it as a hexadecimal number, so I think "}_9~\x00\x00\x00\x00", means \
"\x7d\x5f\x39\x7e\x00\x00\x00\x00" in hexadecimal
发件人: klee-dev-bounces@imperial.ac.uk [mailto:klee-dev-bounces@imperial.ac.uk] \
代表 曾杰 发送时间: 2017年4月12日 10:22
收件人: klee-dev
主题: [klee-dev] Sorry, may i ask a question?
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 #3 (text/html)]
<html xmlns:v="urn:schemas-microsoft-com:vml" \
xmlns:o="urn:schemas-microsoft-com:office:office" \
xmlns:w="urn:schemas-microsoft-com:office:word" \
xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" \
xmlns="http://www.w3.org/TR/REC-html40"> <head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 12 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"MS Mincho";
panose-1:2 2 6 9 4 2 5 8 3 4;}
@font-face
{font-family:宋体;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@宋体";
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:微软雅黑;
panose-1:2 11 5 3 2 2 4 2 2 4;}
@font-face
{font-family:"\@微软雅黑";
panose-1:2 11 5 3 2 2 4 2 2 4;}
@font-face
{font-family:"\@MS Mincho";
panose-1:2 2 6 9 4 2 5 8 3 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:宋体;}
h2
{mso-style-priority:9;
mso-style-link:" 题 2 Char";
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:18.0pt;
font-family:宋体;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
span.2Char
{mso-style-name:" 题 2 Char";
mso-style-priority:9;
mso-style-link:" 题 2";
font-family:"Cambria","serif";
font-weight:bold;}
span.keyword
{mso-style-name:keyword;}
span.EmailStyle19
{mso-style-type:personal-reply;
font-family:"Calibri","sans-serif";
color:#1F497D;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 90.0pt 72.0pt 90.0pt;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="ZH-CN" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span lang="EN-US" \
style="font-size:10.5pt;font-family:"Calibri","sans-serif";color:#1F497D">If \
the character is visible, then klee will show it directly, otherwise, it will show it \
as a hexadecimal number, so I think "}_9~\x00\x00\x00\x00", means \
"\x7d\x5f\x39\x7e\x00\x00\x00\x00" in hexadecimal<o:p></o:p></span></p> <p \
class="MsoNormal"><span lang="EN-US" \
style="font-size:10.5pt;font-family:"Calibri","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:10.0pt">发件人<span \
lang="EN-US">:</span></span></b><span lang="EN-US" style="font-size:10.0pt"> \
klee-dev-bounces@imperial.ac.uk [mailto:klee-dev-bounces@imperial.ac.uk] \
</span><b><span style="font-size:10.0pt">代表 </span></b><span \
style="font-size:10.0pt">曾杰<span lang="EN-US"><br> </span><b>发送时间<span \
lang="EN-US">:</span></b><span lang="EN-US"> 2017</span>年<span \
lang="EN-US">4</span>月<span lang="EN-US">12</span>日<span lang="EN-US"> 10:22<br> \
</span><b>收件人<span lang="EN-US">:</span></b><span lang="EN-US"> klee-dev<br> \
</span><b>主题<span lang="EN-US">:</span></b><span lang="EN-US"> [klee-dev] Sorry, \
may i ask a question?<o:p></o:p></span></span></p> </div>
<p class="MsoNormal"><span lang="EN-US"><o:p> </o:p></span></p>
<div>
<p class="MsoNormal"><span lang="EN-US">Hi,all<o:p></o:p></span></p>
</div>
<div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.5pt">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><b><span \
lang="EN-US" style="font-size:9.0pt;color:#434343;background:#F2F2F2">Vulnerability \
</span></b><span lang="EN-US" style="font-size:10.5pt">in the dissertation of Prof. \
Cristian Cadar for the degree of doctor of philosophy.<o:p></o:p></span></p> </div>
</div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.5pt">the code of \
vulnerability existing in the function safe_addptr in the 32-bit version of HISTAR \
kernel :<o:p></o:p></span></p> </div>
<div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.5pt">uintptr_t \
safe_addptr(int *of , uint64_t a, uint64_t b){<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.5pt">uintptr_t \
r=a+b;<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.5pt">if(r < a \
)<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.5pt">return \
r;<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" \
style="font-size:10.5pt">}<o:p></o:p></span></p> </div>
</div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="font-size:10.5pt">i rewrite a similar \
program as bellow.</span><span style="font-size:10.5pt;font-family:"MS \
Mincho""><span style="background:#BCD3E5"></span></span><span lang="EN-US" \
style="font-size:10.5pt"><o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal" style="background:#BCD3E5"><span style="font-family:"MS \
Mincho";background:#BCD3E5"></span><span lang="EN-US" \
style="font-family:"微软雅黑","sans-serif";color:#464646;background:#BCD3E5">#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; }</span><span lang="EN-US" \
style="background:#BCD3E5"><o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal" style="background:#BCD3E5"><span lang="EN-US" \
style="background:#BCD3E5"><o:p> </o:p></span></p> </div>
<div>
<p class="MsoNormal"><span style="font-family:"MS \
Mincho";background:#BCD3E5"></span><span lang="EN-US" \
style="background:#BCD3E5"> when using klee to run it. there are three \
paths.</span><span style="font-family:"MS \
Mincho";background:#BCD3E5"></span><span lang="EN-US" \
style="background:#BCD3E5"><o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="background:#BCD3E5"> My \
question is about the generated test case which i cannot \
understand.<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" \
style="background:#BCD3E5"><o:p> </o:p></span></p> </div>
<div>
<div>
<p class="MsoNormal"><span lang="EN-US" \
style="background:#BCD3E5">root@sucof-virtual-machine:~/</span><span \
style="background:#BCD3E5">桌面<span lang="EN-US">/xiaojiework/klee_work# \
ktest-tool ./klee-last/test000002.ktest<o:p></o:p></span></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="background:#BCD3E5">ktest file : \
'./klee-last/test000002.ktest'<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="background:#BCD3E5">args \
: ['overflowdetect_klee.bc']<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="background:#BCD3E5">num objects: \
2<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="background:#BCD3E5">object \
0: name: 'a'<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="background:#BCD3E5">object \
0: size: 8<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="background:#BCD3E5">object \
0: data: '\x01\x00FA\x00\x00\x00\x80'<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="background:#BCD3E5">object \
1: name: 'b'<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="background:#BCD3E5">object \
1: size: 8<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="background:#BCD3E5">object \
1: data: '}_9~\x00\x00\x00\x00'<o:p></o:p></span></p> </div>
<div>
<p class="MsoNormal"><span lang="EN-US" \
style="background:#BCD3E5"><o:p> </o:p></span></p> </div>
</div>
<div>
<p class="MsoNormal"><span lang="EN-US" style="background:#BCD3E5"> </span><span \
style="font-family:"MS Mincho";background:#BCD3E5"></span><span \
style="background:#BCD3E5"> <span lang="EN-US"> </span></span><span \
style="font-family:"MS Mincho";background:#BCD3E5"></span><span \
lang="EN-US" style="background:#BCD3E5"> I understand "\x" is to \
</span><span style="font-family:"MS \
Mincho";background:#BCD3E5"></span><span lang="EN-US" \
style="background:#BCD3E5">express hexadecimal number. then what does the \
"}_9~" means in the red circle in the above picture ?<o:p></o:p></span></p> \
</div> <div>
<p class="MsoNormal"><span style="font-family:"MS \
Mincho";background:#BCD3E5"></span><span lang="EN-US" \
style="background:#BCD3E5"> </span><span style="font-family:"MS \
Mincho";background:#BCD3E5"></span><span lang="EN-US" \
style="background:white">I would very much appreciate your help.</span><span \
style="font-family:"MS Mincho";background:white"></span><span \
lang="EN-US"><o:p></o:p></span></p> </div>
</div>
</body>
</html>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
--===============1033098903974470060==--
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic