Problems with symbolic execution of 'rm' from the Coreutil

[Samaneh Navabpour]

Hi,

So I have a question regarding the symbolic execution of operation
'rm' from the Coreutil.

Lets say I run:

klee --only-output-states-covering-new --optimize --libc=uclibc
--posix-runtime ./rm.bc --sym-args 0 2 2

This instruction can hypothetically result in the execution of

rm -f /

In this case, by running the above Klee command I can destroy my file
system. can I not??? or am I wrong?

Can someone please suggest a solution around this problem so I can
symbolically execute 'rm' from the Coreutil.

Im facing the same problem when trying to use Klee to symbolically
execute unlinking of files in libc.

Thank you
Samaneh

[Cristian Cadar]

Yes, you need to be careful with applications such as rm. This being
said, note that the POSIX model in KLEE simply ignores unlink() requests
for concrete files. However, recent kernels (>= 2.6.16) have introduced
unlinkat(), which KLEE currently does not handle. I do have a pending
patch from Paul Marinescu for unlinkat(), which I hope to add soon.

Replaying the test cases for rm is more dangerous, and the best thing
would be to do it in a sandbox.

Best,
Cristian

Hi,
So I have a question regarding the symbolic execution of operation 'rm'
from the Coreutil.
klee --only-output-states-covering-new --optimize --libc=uclibc
--posix-runtime ./rm.bc --sym-args 0 2 2
This instruction can hypothetically result in the execution of
rm -f /
In this case, by running the above Klee command I can destroy my file
system. can I not??? or am I wrong?
Can someone please suggest a solution around this problem so I can
symbolically execute 'rm' from the Coreutil.
Im facing the same problem when trying to use Klee to symbolically
execute unlinking of files in libc.
Thank you
Samaneh

[Samaneh Navabpour]

Thank you Cristian.

Post by Cristian Cadar
Yes, you need to be careful with applications such as rm. This
being said, note that the POSIX model in KLEE simply ignores
unlink() requests for concrete files. However, recent kernels (>=
2.6.16) have introduced unlinkat(), which KLEE currently does not
handle. I do have a pending patch from Paul Marinescu for
unlinkat(), which I hope to add soon.
Replaying the test cases for rm is more dangerous, and the best
thing would be to do it in a sandbox.
Best,
Cristian

Hi,
So I have a question regarding the symbolic execution of operation 'rm'
from the Coreutil.
klee --only-output-states-covering-new --optimize --libc=uclibc
--posix-runtime ./rm.bc --sym-args 0 2 2
This instruction can hypothetically result in the execution of
rm -f /
In this case, by running the above Klee command I can destroy my file
system. can I not??? or am I wrong?
Can someone please suggest a solution around this problem so I can
symbolically execute 'rm' from the Coreutil.
Im facing the same problem when trying to use Klee to symbolically
execute unlinking of files in libc.
Thank you
Samaneh

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev