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
Feature changed by: Jiri Slaby (jirislaby) Feature #309767, revision 5 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) 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
+ #3: Jiri Slaby (jirislaby) (2010-06-10 13:13:31) + Available as + git clone git://decibel.fi.muni.cz/~xslaby/llvm-test + or at + http://decibel.fi.muni.cz/cgi-bin/gitweb.cgi?p=llvm-test.git;a=summary (http://decibel.fi.muni.cz/cgi-bin/gitweb.cgi?p=llvm-test.git;a=summary) -- openSUSE Feature: https://features.opensuse.org/309767