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

[Eitan Adler]

On 25 April 2014 10:14, Dag-Erling Smørgrav <des at des.no> 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.

<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.



-- 
Eitan Adler