Formal Analysis And Verification Of Embedded Interface Driver Based On Model Checking

The security of embedded system not merely depends on the stability of the system hardware,and that has a close relationship with the realization code of the system function.In some complex embedded systems,the embedded system hardware needs to connect a large number of peripherals,which leads to the embedded system software not only contains a large number of user codes,these driver codes,if not verified by security,will cause a series of security problems such as deadlock.Formal method is one of the most favorable methods to verify the security of embedded system driver.Through analyzing the flow of data in kernel driver and the interaction between processes,the potential security risks can be found and the security of embedded system can be guaranteed.This paper focuses on the security of Linux character drivers.Based on timed automata design and the definition of the key data structures in the kernel driver,a general method for the formal description of Linux character driver is proposed.The main research results of this paper are as follows:(1)A general method of character driver formal analysis is proposed.Formally define data structures such as devices,resource functions,platform drivers,and file manipulation structures.The loading process of the character driver and the process of the user access driver are analyzed,and timed automata semantics of the loading and running of the response driver are given.Splitting the loading process of character driver makes device registration and platform driver registration relatively independent,so as to reduce the number of states.(2)The PWM driver model based on timed automata is established.The platform bus model is introduced to realize device registration and platform registration asynchronously.PWM driver was modeled according to the general method of character driver formalization analysis,and UPPAAL tool was used to verify whether the PWM driver model satisfied the properties abstracted from the computation tree logic.(3)The driver model of UART based on timed automata is established.The UART driver is divided into the driver structure part and the protocol implementation part.The running and loading of the UART driver and the running of the underlying implementation code are verified respectively.It is found that if the data cache is not cleaned regularly,it will lead to memory overflow.