Deductive Verification of Linux Kernel Library Functions at the Machine Code Level

In the modern world, the software takes an increasing part in critical systems management. To control the correctness of such systems by using different methods, among which not last part is taken by methods of formal verification. In contrast to testing, formal verification allows proving the complete correctness of the function being checked, which fully pays for the complexity of using this technology. At this moment, there are a large number of successful applications of formal verification, but the absolute majority of them stopped at verifying the correctness of the source code. After verification, the source code is passed to the compiler, which correctness is not proven. As a result, the machine code generated by the compiler may not meet the high-level function specification. To date, there are very few examples of successful verification projects at the machine code level, and none of them allows us to fully automatic re-use the source code level proofs. This paper shows the structure and examples of the successful use of a machine code deductive verification system that can automatically re-use the specification of a source code level function to prove the correctness of the corresponding machine code.