From owner-freebsd-security@FreeBSD.ORG  Fri Apr 25 17:14:24 2014
Return-Path: <owner-freebsd-security@FreeBSD.ORG>
Delivered-To: freebsd-security@freebsd.org
Received: from mx1.freebsd.org (mx1.freebsd.org [8.8.178.115])
 (using TLSv1 with cipher ADH-AES256-SHA (256/256 bits))
 (No client certificate requested)
 by hub.freebsd.org (Postfix) with ESMTPS id DC8A19D9;
 Fri, 25 Apr 2014 17:14:24 +0000 (UTC)
Received: from smtp.des.no (smtp.des.no [194.63.250.102])
 by mx1.freebsd.org (Postfix) with ESMTP id 9B4ED1D2F;
 Fri, 25 Apr 2014 17:14:24 +0000 (UTC)
Received: from nine.des.no (smtp.des.no [194.63.250.102])
 by smtp-int.des.no (Postfix) with ESMTP id 5936F6505;
 Fri, 25 Apr 2014 17:14:23 +0000 (UTC)
Received: by nine.des.no (Postfix, from userid 1001)
 id 7BAC23112A; Fri, 25 Apr 2014 19:14:25 +0200 (CEST)
From: =?utf-8?Q?Dag-Erling_Sm=C3=B8rgrav?= <des@des.no>
To: Ben Laurie <benl@freebsd.org>
Subject: Re: OpenSSL static analysis, was: De Raadt + FBSD + OpenSSH + hole?
References: <DC2F9726-881B-4D42-879F-61377CA0210D@mac.com>
 <8783.1398202137@server1.tristatelogic.com>
 <20140423003400.GA8271@glaze.hydra>
 <20140423010054.2891E143D098@rock.dv.isc.org>
 <20140423012206.GB8271@glaze.hydra> <86bnvpoav7.fsf@nine.des.no>
 <CAG5KPzyTCTbe_vTcP8HDa_KU0agNZQjzVmQ4XnZZjgGFEVnyaQ@mail.gmail.com>
Date: Fri, 25 Apr 2014 19:14:25 +0200
In-Reply-To: <CAG5KPzyTCTbe_vTcP8HDa_KU0agNZQjzVmQ4XnZZjgGFEVnyaQ@mail.gmail.com>
 (Ben Laurie's message of "Fri, 25 Apr 2014 15:15:29 +0100")
Message-ID: <86zjj9mivi.fsf@nine.des.no>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (berkeley-unix)
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
Cc: "freebsd-security@freebsd.org security" <freebsd-security@freebsd.org>,
 "Ronald F. Guilmette" <rfg@tristatelogic.com>
X-BeenThere: freebsd-security@freebsd.org
X-Mailman-Version: 2.1.17
Precedence: list
List-Id: "Security issues \[members-only posting\]"
 <freebsd-security.freebsd.org>
List-Unsubscribe: <http://lists.freebsd.org/mailman/options/freebsd-security>, 
 <mailto:freebsd-security-request@freebsd.org?subject=unsubscribe>
List-Archive: <http://lists.freebsd.org/pipermail/freebsd-security/>
List-Post: <mailto:freebsd-security@freebsd.org>
List-Help: <mailto:freebsd-security-request@freebsd.org?subject=help>
List-Subscribe: <http://lists.freebsd.org/mailman/listinfo/freebsd-security>, 
 <mailto:freebsd-security-request@freebsd.org?subject=subscribe>
X-List-Received-Date: Fri, 25 Apr 2014 17:14:24 -0000

Ben Laurie <benl@freebsd.org> writes:
> Dag-Erling Sm=C3=B8rgrav <des@des.no> writes:
> > https://en.wikipedia.org/wiki/Halting_problem
> Curious what the halting problem can tell us about finding/fixing bugs?

Some participants in this thread claim that there is no such thing as a
false positive from a static analyzer.  A corollary of the halting
problem is that it is impossible to write a program capable to proving
or disproving the correctness of all programs.  Hence, static analysis
must perforce produce both false positive and false negative results.
The purpose of static analysis in a compiler is to identify possible
optimizations; therefore it must be conservative, because a false
negative may result in incorrect code; therefore it will produce many
false positives.

DES
--=20
Dag-Erling Sm=C3=B8rgrav - des@des.no