Feature changed by: Jiri Slaby (jirislaby) Feature #309767, revision 4 Title: Symbolically execute kernel parts Requested by: Jiri Slaby (jirislaby) Description: Use symbolic execution to find bugs in kernel. It is a promising approach nowadays and may find tons of bugs without false positives. I'm working on that myself. Discussion: #1: Martin Seidler (pistazienfresser) (2010-06-10 12:37:01) Is this already been done by someone else? Comparisem with real execution in a virtual machine? A (link to) a bit more information about this feature? Example/Testcase (maybe with an existing bug like: https://bugzilla.novell.com/show_bug.cgi?id=593463 and http://forums.opensuse.org/get-help-here/pre-release-beta/438965-intel-gpu-8... + #2: Jiri Slaby (jirislaby) (2010-06-10 13:04:24) (reply to #1) + > Is this already been done by someone else? + Not that I know of. It is not as that straightforward as it may seem. + Some parts of the kernel (especially block devices) were simulated + symbolically to exercise filesystems, but there is no tool that uses + symb. exec. (SE) systematically on the arbitrary kernel parts. + + > Comparisem with real execution in a virtual machine? + With real execution the code will not be checked through all its paths. + SE tries to navigate the code through all the code paths. It stores + path conditions and does mangling on the inputs according to the path + condition. + + > A (link to) a bit more information about this feature? + It is not a new technique. The first paper is from King from 70's, but + even after 2000 it got to the scope of people when it was used in + tools. Previously it was though the results cannot be computed in some + reasonable time, but the paper from after 2000 proved this wrong -- + both due to newer hardware and optimizations used before changed path + conditions are passed down to the solver. + + Papers: + J.C. King: Symbolic execution and program testing + Engler et al.: Klee : Unassisted and automatic generation of high- + coverage tests for complex systems programs + Godefroid et al.: DART: Directed Automated Random Testing -- openSUSE Feature: https://features.opensuse.org/309767