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.

_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to