The problem is not with klee. Perhaps you're using it wrong.
me@indomitable:/data/scratchpad$ cat example.c
#include <stdio.h>
#include <klee/klee.h>
void bof(char *bof){
char buf[8];
strcpy(buf,bof);
printf("buf=%s\n",buf);
}
int main(int argc, char *argv[]){
int x=0;
char buf[20];
klee_make_symbolic(&buf,sizeof(buf),"buf");
for(x=0;x<sizeof(buf);x++)
klee_assume(buf[x]!='\x00');
//fgets(buf, 20, stdin);
bof(buf);
return 0;
}
me@indomitable:/data/scratchpad$ klee-gcc -g -O0 -I/data/klee/klee29/include -c
-o example.bc example.c
example.c: In function ‘bof’:
example.c:6: warning: incompatible implicit declaration of built-in function
‘strcpy’
me@indomitable:/data/scratchpad$ /data/klee/klee29/Release+Asserts/bin/klee
--posix-runtime --libc=uclibc example.bc
KLEE: NOTE: Using model:
/data/klee/klee29/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-2"
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: WARNING: undefined reference to function: fprintf
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to function: klee_get_valuel
KLEE: WARNING: undefined reference to function: snprintf
KLEE: WARNING: undefined reference to function: strtol
KLEE: WARNING: calling external: syscall(16, 0, 21505, 47621088)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: WARNING: calling external: __xstat64(1, 47543488, 47812576)
KLEE: ERROR: /data/klee/klee-uclibc-29/libc/string/strcpy.c:27: memory error:
out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 12136
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
me@indomitable:/data/scratchpad$ cat klee-last/test000001.ptr.err
Error: memory error: out of bound pointer
File: /data/klee/klee-uclibc-29/libc/string/strcpy.c
Line: 27
Stack:
#0 00001966 in strcpy (s1=47856160, s2=47911232) at
/data/klee/klee-uclibc-29/libc/string/strcpy.c:27
#1 00000281 in bof (bof=47911232) at /data/scratchpad/example.c:6
#2 00000335 in __user_main (argc=1, argv=38954144) at
/data/scratchpad/example.c:17
#3 00001156 in __uClibc_main (main=34427168, argc=1, argv=38954144,
app_init=0, app_fini=0, rtld_fini=0, stack_end=0) at
/data/klee/klee-uclibc-29/libc/misc/internals/__uClibc_main.c:414
#4 00004052 in main (=1, =38954144)
Info:
address: 47856168
next: object at 47857728 of size 0
MO6860[0] allocated at klee_init_fds(): %63 = call noalias i8*
@malloc(i64 %62) nounwind, !dbg !2969
prev: object at 47856160 of size 8
MO6983[8] allocated at bof(): %buf = alloca [8 x i8]
Paul
On 26 Apr 2012, at 12:23, Lionel PRAT wrote:
> Hi,
>
> I'd like to get the buffer overflow to be detected with klee. It
> detects many memory problem. However, in the code below, impossible
> for him to detect the buffer overflow created on strcpy ... With
> valgrind memcheck is detected. Is it possible to modify a source file
> klee to handle this bug? If so, which?
> thank you
> Sincerely,
> Lionel Prat
>
> ---------------------------
> #include <stdio.h>
> #include <klee/klee.h>
>
> void bof(char *bof){
> char buf[8];
> strcpy(buf,bof);
> printf("buf=%s\n",buf);
> }
>
> int main(int argc, char *argv[]){
> int x=0;
> char buf[20];
> klee_make_symbolic(&buf,sizeof(buf),"buf");
> for(x=0;x<sizeof(buf);x++)
> klee_assert(buf[x]!='\x00');
> //fgets(buf, 20, stdin);
> bof(buf);
> return 0;
> }
> _______________________________________________
> klee-dev mailing list
> [email protected]
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
