  The seL4 microkernel is currently the only kernel that has been fully
formally verified. In general, the increased interest in ensuring the security
of a kernel's code results from its important role in the entire operating
system. One of the basic features of an operating system is that it abstracts
the handling of devices. This abstraction is represented by device drivers -
the software that manages the hardware. A proper verification of the software
component could ensure that the device would work properly unless there is a
hardware failure.In this paper, we choose to model the behavior of a device
driver and build the proof that the code implementation matches the expected
behavior. The proof was written in Isabelle/HOL, the code translation from C to
Isabelle was done automatically by the use of the C-to-Isabelle Parser and
AutoCorres tools. We choose Isabelle theorem prover because its efficiency was
already shown through the verification of seL4 microkernel.
