Selective symbolic execution

Vitaly Chipounov, Vlad Georgescu, Cristian Zamfir, George Candea
[Google Scholar] [DBLP] [Citeseer] [url]
Read: 28 June 2020

Proceedings of the 5th Workshop on Hot Topics in System Dependability (HotDep)
Note(s): symbolic execution, KLEE verifier, S2E verifier

The S2E verifier can analyze application code, complex GUI libraries, kernel code, device drivers, and even hardware devices. It does this by alternating between concrete execution (using QEMU) and symbolic execution (using the KLEE verifier). Switching modes makes it more flexible but it also makes it more efficient because (slower) symbolic execution can be restricted to the code of most interest which might be a library, a recently changed code path, etc.

The big trick is switching from concrete execution to symbolic execution.

The evaluation is fairly sparse but they say they are able to analyze device drivers in Windows with only a 1.7x slowdown relative to unmodified QEMU.

S2E verifier