Is there a way to call an SMT solver such as yices or STP from linux kernel? I want to implement a symbolic execution engine and therefore I need to solve constraints at run time. Thanks in advance!
Asked
Active
Viewed 177 times
0
-
Can you clarify the "constraints at run time" part? Why do you need to run this code in kernel space? – JC1 Jun 15 '14 at 17:07
-
I want to provide inputs for different paths and each path is recognized by the value of conditionals it contains. If I can find inputs that result in different values for conditionals, different paths will be covered. In order to find inputs I need to solve constraints needed by conditionals. – user3564532 Jun 16 '14 at 10:58
-
2If you just want to symbolically execute the Linux kernel you don't need to call a SMT solver from the kernel. I believe S2E does what you want to do. – JC1 Jun 16 '14 at 13:46
-
Thanks! I will check it out. But what if we want to implement a symbolic execution engine? – user3564532 Jun 16 '14 at 13:50
-
The Linux kernel allows "userspace helpers" (see e.g. http://www.ibm.com/developerworks/linux/library/l-user-space-apps/index.html for how to use it). Unless the kernel code is perf-critical, it's possible to "call out to userspace" to offload processing not suitable for executing in kernel, for whatever reason. Also see http://stackoverflow.com/questions/5246636/executing-a-user-space-function-from-the-kernel-space about this. – FrankH. Jun 18 '14 at 09:48