Symbolic Execution Based Bug Detection Of Drivers

With the popularity of software,people are increasingly high demand for software reliability.Device drivers constitute an important part of the OS.The reliability of device drivers is critical to the security and reliability of the OS.Studies have shown that,driver defects accounted for more than half of Linux OS defects.Therefore,improving the quality of the drivers is an important part of improving the quality of the software.Drivers need to call the OS kernel interface and the underlying hardware interface.The rules of call interface can be defined as a finite state machine.How to detect the calls of interface are meeting the rules,is an important aspect to improve the reliability of the drivers.Program analysis is an important way to improve the reliability of software.Symbol execution is a kind of accurate program analysis technique.Because of its feasibility,less false positives and wide scope of application,it has been widely concerned by academia and industry.In this paper,we study the automatic detection method of the drivers bug based on symbolic execution.The main contents of this paper include:(1)There are a number of complex construction elements in drivers,such as pointer.However,symbolic execution tool does not support making pointer symbolic.Therefore,this paper implements a lazy initialization algorithm,which can handle the complex data types during the symbol execution,and effectively supports the symbol execution detection of drivers,and improves the scalability of symbol execution technology.(2)This paper proposes a property guided symbolic execution based framework for the bug detection of Linux device drivers.To analyze multiple properties simultaneously,a method for guiding symbolic execution with respect to multiple properties is proposed.Based on LLVM and KLEE,this paper has implemented the framework and the guiding method.(3)This paper summarizes the partial characteristics of driver defects,and carrys out experiments.The results of the experiments on real world Linux drivers demonstrate the effectiveness and efficiency.