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

[Samaneh Navabpour]

Thank you Cristian.

Quoting Cristian Cadar <c.cadar at imperial.ac.uk>:

> 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
>>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>



-- 
Samaneh Navabpour
Department of Electrical and Computer Engineering
University of Waterloo
200 University Avenue West
Waterloo, Ontario, Canada, N2L 3G1