OpenSSL static analysis, was: De Raadt + FBSD + OpenSSH + hole?

[hcoin]

On 04/25/2014 12:14 PM, Dag-Erling Smørgrav wrote:
> Ben Laurie <benl at freebsd.org> writes:
>> Dag-Erling Smørgrav <des at 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