I have just published a piece about the Intel Excite project on my Software Evangelist blog at the Intel Developer Zone. The Excite project is using a combination of of symbolic execution, fuzzing, and concrete testing to find vulnerabilities in UEFI code, in particular in SMM. By combining symbolic and concrete techniques plus fuzzing, Excite achieves better performance and effect than using either technique alone.
Excite combines a dynamic selective symbolic execution and guided fuzzing for test case generation. It uses the Simics virtual platform to dump platform-dependent data and code, and to replay tests while checking for security issues and measuring coverage to guide the next set of tests. Excite uses some custom Simics code to check for bad code behaviors. The symbolic execution part comes from the CRETE project, and the fuzzing is derived from the AFL fuzzer. It is a very good example of what can be built when combining powerful pieces in new combinations – kind of a mashup of powerful programming/analysis/debug tools.