As computer systems become more ubiquitous in society the negative consequences of security holes and bugs in software and hardware grow larger. In theory, the optimal way to ensure that no such possibilites exists is to conduct formal proofs that the system behaves as it should and that it is incapable of performing unintended side-effects. Today we have no such proofs for entire non-trivial real-word systems, neither are the methods in which such proofs can be conducted well explored. This work is a case study for conducting such verification in the HOL 4 tool.
The work conserns the formal verification of a software monitor that is supposed to guarantee that the Linux driver in incapable of putting a certain Network Interface Card (NIC) in a undefined state and that it does not read or modify memory which it should not have access to. Since the work is large it was constrained to only concider initialization of the device and reception / transmission of messages. The verification was conducted by transcribing the C code of the monitor into an equivalent model into HOL 4 and then constructing an invariant meant to capture the intended possible configuration of the state and ensuring the desired security properties. The final result managed to prove that initialization and most of the transmission cases are secure. The work also lays out a solid foundation to extend the verification.