From owner-freebsd-security@FreeBSD.ORG Fri Apr 25 17:45:40 2014 Return-Path: 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 F0E211C9 for ; Fri, 25 Apr 2014 17:45:39 +0000 (UTC) Received: from mail-qg0-x235.google.com (mail-qg0-x235.google.com [IPv6:2607:f8b0:400d:c04::235]) (using TLSv1 with cipher ECDHE-RSA-RC4-SHA (128/128 bits)) (Client CN "smtp.gmail.com", Issuer "Google Internet Authority G2" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id A6E7E11A4 for ; Fri, 25 Apr 2014 17:45:39 +0000 (UTC) Received: by mail-qg0-f53.google.com with SMTP id f51so4288319qge.40 for ; Fri, 25 Apr 2014 10:45:38 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=eitanadler.com; s=0xdeadbeef; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=Lnw/bcOq6JMQkmUDUefJP8b27jHSEIcGS4wcwiRsF3g=; b=CNTuPezjmz8XPdAfF0tqfzayPx9Qpol4NtuCx+kl7e9rTi/6yfQQul/Z9zmsIjdK6X dniaelsh/bQFiyV8NB866dTybqIyLguelgqfddAdV94r/737zpHKSRhzsR1mGEAg6z+U 4M5ySKuJu3fRAIxYsd8WUwubtzDKGKEdBhek8= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc:content-type:content-transfer-encoding; bh=Lnw/bcOq6JMQkmUDUefJP8b27jHSEIcGS4wcwiRsF3g=; b=Ke4fhid94TZwapnczxztbqTykQbiBnVyTF2uyXPg86WgdmiXbyKScKuQF+cjtvs4yt IXaq8iqAtRnVpW2RF2aRnHMRmz98S48pq8hiHAev60SOLoLF/dBEHKgXRBKbs3o2fLv0 OOBH1eNNPOWfCMSaEaXe9B3FRsG1EFjJra9F00Kfn56SbLsgmgwwRPLxGnoZ3PMpeTsJ v2Qx0+9Pw7hWPoy5qQtHZWgWrZqCi1+T6Z+ebR+X8F+TuH/49FC/mxDyrGmI6NQ4uet7 5XhQQoRUYACRkpc8PEbdANxMdciYFxSsEn+iUxjqc/7O5MvDcuRZFG+aAZ7EIJT0Llm0 jWug== X-Gm-Message-State: ALoCoQn9/3JSqtEGmcTW6ePBILwfrL8ZTaQTB1IeN1fGsU5MiVzVki4ftijwiwxaJzxCAIdr94kE X-Received: by 10.224.67.131 with SMTP id r3mr13644458qai.75.1398447938109; Fri, 25 Apr 2014 10:45:38 -0700 (PDT) MIME-Version: 1.0 Received: by 10.96.54.102 with HTTP; Fri, 25 Apr 2014 10:45:08 -0700 (PDT) In-Reply-To: <86zjj9mivi.fsf@nine.des.no> 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> From: Eitan Adler Date: Fri, 25 Apr 2014 10:45:08 -0700 Message-ID: Subject: Re: OpenSSL static analysis, was: De Raadt + FBSD + OpenSSH + hole? To: =?UTF-8?Q?Dag=2DErling_Sm=C3=B8rgrav?= Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Cc: Ben Laurie , "freebsd-security@freebsd.org security" , "Ronald F. Guilmette" 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 17:45:40 -0000 On 25 April 2014 10:14, Dag-Erling Sm=C3=B8rgrav wrote: > Ben Laurie writes: >> Dag-Erling Sm=C3=B8rgrav 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. Modern computers can be considered linear bounded automatons , not turing machines, so the halting problem can be solved on them > Hence, static analysis > must perforce produce both false positive and false negative results. This doesn't follow from the halting problem: for instance static analysis of the form "return nothing" produces no false positives. Modern static analysis are not both sound and complete. In general implementers have leaned towards soundness over completeness. > 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. the clang analyzer operates under a different set of constraints and end user vision than a typical compiler. --=20 Eitan Adler