Making the first opened file symbolic

[Taddeüs Kroes]

Hi,

I am trying to reproduce results from the KLEE OSDI'08 paper, running symbolic execution on all of coreutils. They use KLEE's --sym-files option which intercepts the open() syscall and returns a descriptor to a symbolic file. It does so for the first N opened files (e.g. stdin and some file whose name was specified in a command-line argument).

In s2e there is only 's2ecmd symbfile' (as far as I can see) for creating symbolic files. In the KLEE paper they run coreutils with arguments --sym-args 10 2 2 --sym-files 2 8. --sym-args can be replicated using init_env.so and stdin can be made symbolic using 's2ecmd symbwrite', but I am not sure how to replicate the behaviour of --sym-files here. I considered running as follows:

echo aaaaaaaa > /tmp/fooba

s2ecmd symbfile 

s2ecmd symbwrite 8 | LD_PRELOAD=init_env.so ./run --concolic /tmp/fooba --sym-args 0 2 2

Where "/tmp/fooba" is a 10-character symbolic string used to replace --sym-arg 10 and at the same time --sym-files. However this makes the filename symbolic, which will likely cause the executor to fork for a whole bunch of possible files it can open and so considerably slow down analysis.

Does anyone have any thoughts on how to more closely replicate the behaviour of KLEE's --sym-files option? Or other suggestions for running these tests?

Thanks!

Taddeüs

[Taddeüs Kroes]

Of course I meant to say 's2ecmd symbfile /tmp/fooba' on the second line of the example

Op vrijdag 19 juni 2015 12:19:18 UTC+2 schreef Taddeüs Kroes: