基于性质制导符号执行的Limix驱动程序缺陷检测研究.

Device drivers constitute an important part o£ 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. [ABSTRACT FROM AUTHOR]