Re: OpenSSL static analysis, was: De Raadt + FBSD + OpenSSH + ho

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

> On 25 April 2014 13:24, Dag-Erling Sm=F8rgrav <des@des.no> wrote:
>> Chad Perrin <code@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=92s provably impossible to writ=
e 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 prop=
erty or not.

In the actual halting problem the property is =93The program runs to comple=
tion and produces a result with every possible input=94. A classic real wor=
ld example is when property is set to =93The program A is/has a virus=94. T=
he halting problem applies to this discussion very naturally if you use the=
 property =93The program A has a buffer overflow vulnerability=94 or =93The=
 program A uses memory that has already been free()=92d=94. None of these p=
roperties (or any other similar property) can be detected programmatically =
with 100% certainty, that is what the halting problem tells you about findi=
ng bugs.

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

-Kimmo

_______________________________________________
freebsd-security@freebsd.org mailing list
http://lists.freebsd.org/mailman/listinfo/freebsd-security
To unsubscribe, send any mail to "freebsd-security-unsubscribe@freebsd.org"