Date: Fri, 25 Apr 2014 13:16:41 -0500 From: "hcoin" <hcoin@quietfountain.com> To: freebsd-security@freebsd.org Subject: Re: OpenSSL static analysis, was: De Raadt + FBSD + OpenSSH + hole? Message-ID: <535AA689.8000302@quietfountain.com> 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 04/25/2014 12:14 PM, Dag-Erling Smørgrav wrote: > Ben Laurie <benl@freebsd.org> writes: >> Dag-Erling Smørgrav <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. 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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?535AA689.8000302>