From owner-freebsd-security@FreeBSD.ORG Fri Apr 25 18:16:49 2014 Return-Path: Delivered-To: freebsd-security@freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) (using TLSv1 with cipher ADH-AES256-SHA (256/256 bits)) (No client certificate requested) by hub.freebsd.org (Postfix) with ESMTPS id C03F8DAD for ; Fri, 25 Apr 2014 18:16:49 +0000 (UTC) Received: from gate2.quietfountain.com (gate2.quietfountain.com [97.64.213.195]) by mx1.freebsd.org (Postfix) with ESMTP id 95E65153C for ; Fri, 25 Apr 2014 18:16:49 +0000 (UTC) Received: from ops1.quietfountain.com (ops1.quietfountain.com [192.168.29.13]) by gate2.quietfountain.com (Postfix) with ESMTP id 44FB2B8237 for ; Fri, 25 Apr 2014 13:16:48 -0500 (CDT) To: freebsd-security@freebsd.org Date: Fri, 25 Apr 2014 13:16:41 -0500 Subject: Re: OpenSSL static analysis, was: De Raadt + FBSD + OpenSSH + hole? References: <8783.1398202137@server1.tristatelogic.com> <20140423003400.GA8271@glaze.hydra> <20140423010054.2891E143D098@rock.dv.isc.org> <20140423012206.GB8271@glaze.hydra> <86bnvpoav7.fsf@nine.des.no> <86zjj9mivi.fsf@nine.des.no> Message-ID: <535AA689.8000302@quietfountain.com> From: "hcoin" Received: from [192.168.29.127] (gate1.quietfountain.com [192.168.29.2]) by ops1.quietfountain.com; Fri, 25 Apr 2014 13:16:42 -0500 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.4.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit X-BeenThere: freebsd-security@freebsd.org X-Mailman-Version: 2.1.17 Precedence: list List-Id: "Security issues \[members-only posting\]" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 25 Apr 2014 18:16:49 -0000 On 04/25/2014 12:14 PM, Dag-Erling Smørgrav wrote: > Ben Laurie writes: >> Dag-Erling Smørgrav 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. All current analyzers are a packaged up collection of correctness intuitions operating on the borders of language syntax and information semantics. If they deliver 'false positives' it is because we don't know how to capture in software the semantics necessary to justify 'not reporting' false positives. If they deliver 'false negatives' it's because either a syntax/grammar only routine can't reach the semantics necessary to detect the problem, we don't know how to capture the semantics in checking routines, or one got by the grammar checkers. And apropos yours above of 'halting problem': 'Halting' has a defined and objectively testable meaning, while 'correct' and 'secure' do not. Hence the corollary you mention is in the manner of professional intuition (and likely correct in our lifetimes), but not the usual meaning of corollary. And in any event the unhappy outcome you mention in 'the halting problem' exists if and only when presupposing infinite program memory, infinite processing time and by implication infinite machine life. It should be possible to write a set of rules that, when taken together define 'secure', inasmuch as 'secure' can be equivalent to whether only allowed information of known finite size running on a known finite computer crosses an interface or edge of a specific program. But first a great deal more has do be done in defining basics, for example if a hashing routine confirms no-match against a stored hashed password, that's leaking information in a mathematical sense because you now know one password isn't it given the password space is finite (if big), but is that routine 'insecure' or 'secure'? 'Correct' on the other hand, that term is much like valor (in the eye of the beholder). One might argue it is a per-program specification and as such more a restatement of the program itself in an as-yet-to-be-written specification language, which itself needs it's own correctness specification in an as-yet-as-yet-to-be-written specification-specification language, and so forth until we get to the eye of the beholder anyhow, or lunch with Kurt Godel. I don't mean to be argumentative, I just want to urge caution in using metaphors from math without consistent application of either hard or soft focus on the rigor. Harry Coin