Abstract:

Device drivers constitute an important part of an operation system (OS). The reliability of device drivers is critical to the security and reliability of OSs. We propose a property guided symbolic execution based framework for the bug detection of Linux device drivers. To analyze multiple properties simultaneously, we propose a  multiple properties guided symbolic execution method. Based on the LLVM and KLEE, the framework and the property guided method are implemented. The results of the preliminary experiments on real world Linux drivers demonstrate the effectiveness and efficiency of the proposal.

Key words: drivers, symbolic execution, defect detection