From owner-freebsd-security@FreeBSD.ORG  Fri Apr 25 21:21:48 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 A918DAA3
 for <freebsd-security@freebsd.org>; Fri, 25 Apr 2014 21:21:48 +0000 (UTC)
Received: from outgoing.tristatelogic.com (segfault.tristatelogic.com
 [69.62.255.118]) by mx1.freebsd.org (Postfix) with ESMTP id 894C91878
 for <freebsd-security@freebsd.org>; Fri, 25 Apr 2014 21:21:48 +0000 (UTC)
Received: from segfault-nmh-helo.tristatelogic.com (localhost [127.0.0.1])
 by segfault.tristatelogic.com (Postfix) with ESMTP id BA72A3AE0E
 for <freebsd-security@freebsd.org>; Fri, 25 Apr 2014 14:21:47 -0700 (PDT)
From: "Ronald F. Guilmette" <rfg@tristatelogic.com>
To: "freebsd-security@freebsd.org security" <freebsd-security@freebsd.org>
Subject: Re: OpenSSL static analysis, was: De Raadt + FBSD + OpenSSH + hole?
In-Reply-To: <CAG5KPzw_cOfFLX_kn=5DWAX+z+9VeXuzo3Q8YekDJG37tDQ_wQ@mail.gmail.com>
Date: Fri, 25 Apr 2014 14:21:47 -0700
Message-ID: <32377.1398460907@server1.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 21:21:48 -0000


In message <CAG5KPzw_cOfFLX_kn=5DWAX+z+9VeXuzo3Q8YekDJG37tDQ_wQ@mail.gmail.com>
Ben Laurie <benl@freebsd.org> wrote:

>But that would then hide the error condition of it being not set to a
>new value after initialisation.

The (modified/quieted) code example under discussion is as follows:

	variable = value0;  /* initialization */
	if (condition) variable = value1;
	if (!condition) variable = value2;
	use (variable);

Please note that variable *is* *always* set to some value (either value1
or value2) after initialization.  The "error condition" that you seem
concerned about having explicitly flagged does not in fact exist in the
example code snippet under discussion.

>One better answer would be to have a way to annotate that after the
>two conditionals you assert that |variable| is initialised. Then a
>future, smarter static analyzer can attempt to prove you wrong.

Sir, is there any sense in which the final line of the above example
_does not_ already and standing all by itself constitute an implicit
assertion that "variable" has been initialized by that point in the
code?


Regards,
rfg