Date: Fri, 25 Apr 2014 10:45:08 -0700 From: Eitan Adler <lists@eitanadler.com> To: =?UTF-8?Q?Dag=2DErling_Sm=C3=B8rgrav?= <des@des.no> Cc: Ben Laurie <benl@freebsd.org>, "freebsd-security@freebsd.org security" <freebsd-security@freebsd.org>, "Ronald F. Guilmette" <rfg@tristatelogic.com> Subject: Re: OpenSSL static analysis, was: De Raadt + FBSD + OpenSSH + hole? Message-ID: <CAF6rxgmzbPTOeRw=kthbYu_dQv5c2ASZ5u3VKBpp2Afq4moaTg@mail.gmail.com> In-Reply-To: <86zjj9mivi.fsf@nine.des.no> 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> <86zjj9mivi.fsf@nine.des.no>
next in thread | previous in thread | raw e-mail | index | archive | help
On 25 April 2014 10:14, Dag-Erling Sm=C3=B8rgrav <des@des.no> wrote: > 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. <troll>Modern computers can be considered linear bounded automatons , not turing machines, so the halting problem can be solved on them</troll> > 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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?CAF6rxgmzbPTOeRw=kthbYu_dQv5c2ASZ5u3VKBpp2Afq4moaTg>