Abstract:

It has been proved that Linux driver bugs are the major bug source of the whole system, which can lead to serious security problems.A tool called symbolic driver environment (SDE) is designed to detect Linux driver bugs, which consists of the system model,the interactions between driver and kernel, and the interactions between driver and device.Using SDE, we detect two real Linux drivers, and find two bugs. The results prove that the tool is feasible, and the speed is 90% faster and the coverage is 20% larger compared with an existing tool called SymDrive.

Key words: driver bugs;detect bugs;symbolic execution;driver environment