[klee-dev] Is running KLEE on arbitrary programs safe?

[Burhan Akin Y]

Dear KLEE Community,

I am using KLEE to generate test cases for arbitrary programs on GitHub. This includes generating test cases for potential malware infected/related repositories.
>From my understanding of the original paper, KLEE does static code analysis and uses a theorem prover in the backend.
Does KLEE do anything else beyond making variables symbolic, exploring paths and solving constraints?

>From my understanding the only potential danger to generate test cases is, when encountering compiler bombs, or any other ressource intensive programs which can be limited by ulimit. Once the test cases are generated, I would like to get coverage metrics using klee-stats and gcov.

Klee-stats is a python script which only reads stats from the produced files during symbolic execution. There is no security risk involved here too.
But to use gcov we explicitly have to execute the program using klee-replay or setting the KTEST_FILE variable and running the program. Only at this point one should use a virtual environment to take into account that any malware will be executed.

I would like to have some confirmation with my security concerns when using KLEE. I am not interested about repositories which explicitly target exploits in KLEE and make even test generation a dangerous operation.

Best regards

Akin Y.

-------------- next part --------------
HTML attachment scrubbed and removed