[klee-dev] Problems with symbolic execution of 'rm' from the Coreutil

[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

On 28/08/13 21:36, Samaneh Navabpour wrote:
> 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
>