OpenSSL static analysis, was: De Raadt + FBSD + OpenSSH + hole?

[Kimmo Paasiala]

On 25.4.2014, at 17.15, Ben Laurie <benl at freebsd.org> wrote:

> On 25 April 2014 13:24, Dag-Erling Smørgrav <des at des.no> wrote:
>> Chad Perrin <code at apotheon.net> writes:
>>> Obviously, human judgment is an important part of the process of finding
>>> and fixing bugs.  If it wasn't, the last program we'd ever have to debug
>>> would be the one that finds and fixes bugs.
>> 
>> https://en.wikipedia.org/wiki/Halting_problem
>> 
>> Oh, wait, is this one of those conversations where knowledge and facts
>> are not welcome?
> 
> Curious what the halting problem can tell us about finding/fixing bugs?
> 

It and its direct implications mean that it’s provably impossible to write a program X that would take another program A as its input and be able to decide with 100% certainty whether this other program A has a certain property or not.

In the actual halting problem the property is “The program runs to completion and produces a result with every possible input”. A classic real world example is when property is set to “The program A is/has a virus”. The halting problem applies to this discussion very naturally if you use the property “The program A has a buffer overflow vulnerability” or “The program A uses memory that has already been free()’d”. None of these properties (or any other similar property) can be detected programmatically with 100% certainty, that is what the halting problem tells you about finding bugs.

In essence all this is saying that is foolish to claim that an automated code analyzer could find all bugs in a given piece of code, outside some very trivial programs it is just not going to happen.
 
-Kimmo