The Halting Problem and Formal Verification
Seth Nielson
Jun 20, 2016
Trying to create a secure computer system is a terrible headache. For both theoretical and practical reasons, the odds are rarely in favor of the good guys. As an example of an unhappy theoretical dilemma, it has been known since the 80's, based on the well-known Halting Problem, that it is impossible to build a perfect anti-virus capable of identifying all possible malware. And on the practical side, Ross Anderson demonstrated that if a bad guy finds a bug in a sufficiently complex program, a security team that successfully finds and fixes 10,000 bugs only has a 1% chance of finding the right one (see pages 868-869 in chapter 26 of Security Engineering).
So we can't write a program that identifies all possible malware, and we can't even find all the bugs in our own programs. What options are left?
As I discussed in my previous post, Formal Verification is an interesting potential solution. While there are no silver bullets in computer security, creating formally verified programs may become a significant aide to computer security in the coming years and decades.
The basic idea behind formal verification is that we use mathematics to verify and prove certain properties of a single program. While the Halting Problem says we cannot write a program that can determine a property for all other possible programs, it is possible to prove properties for certain specific programs.
The seL4 microkernel is the first operating system kernel that has been formally proven correct in an end-to-end fashion. The verification proves that the binary code is a correct implementation of the specification, and that certain other security properties are guaranteed. It is very important that the binary code is what is verified, because it ensures that there have been no bugs introduced by the compiler (or malice either, for that matter). This is what is meant by the end-to-end verification.
Of course there are limitations on formal verification, and they are important to understand. One issue, in particular, is that some programs have sufficiently complex user inputs and outputs wherein the program is able to act like a kind of simulated general purpose computer. Without going into the gory details, such a system is said to be Turing Complete or Computationally Universal. In other words, the user could write any known algorithm by using the input and output to the program. Depending on how the input and output are used internally, the program can basically become every other program and the halting problem dictates that its correctness cannot be proven.
It should be noted that the seL4 kernel does not include DMA (Direct Memory Access) operations. I'm not sure all of the reasons for this, but I was interested to find that a colleague of mine, Michael Rushanan had just shown that you can create a Turing Complete system using DMA (provided the DMA engine has certain properties). I'm guessing it would be very difficult for the seL4 kernel to be formally verified if it had a DMA engine of this type.