On 04/25/2014 12:14 PM, Dag-Erling Smørgrav wrote:
Ben Laurie <b...@freebsd.org> writes:
Dag-Erling Smørgrav <d...@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
_______________________________________________
freebsd-security@freebsd.org mailing list
http://lists.freebsd.org/mailman/listinfo/freebsd-security
To unsubscribe, send any mail to "freebsd-security-unsubscr...@freebsd.org"
