Re: CVE-2017-14482 - Red Hat Customer Portal

[Óscar Fuentes]

Mario Castelán Castro <marioxcc.MT@yandex.com> writes:

> On 24/09/17 09:42, Óscar Fuentes wrote:
>> It seems that you think that formal verification says that the software
>> is correct. That's in theory. Practice is different, as usual.
>
> This depends on what exactly is meant by “correct”.

"correct" means that the client (the people who required the software)
says that the program fulfills his requirements. Sometimes you need to
wait an infinite amount of time for obtaining client's approbation :-)

> If by “correctness” it is meant a formula in *formal logic*, then yes,
> we can prove that the program behaves correctly.

Ever heard of a chap named Kurt Gödel? Or his cousin Alan Turing? :-)

> If by “correct” it is meant an informal concept, then proving
> correctness is in general not possible because a specification in formal
> logic is required to prove anything. One may believe that one has
> formalized correct behavior but later one finds that the formalization
> does not accurately capture the informal concept.

Yes. But we have to deal with informal specifications. Furthermore, it
is almost certain that there are "correct" informal specifications that
do not admit a verifiable formal specification.

> The cases of the “bugs” mentioned in the paper you referenced are error
> in formalizing “correct behavior”. That this is possible is not breaking
> news, as you seem to think. This is a caveat well known to anybody
> involved in formal verification.

Yet you seem to give it little importance. Once we assume that a
verifiable specification might be incorrect in the sense you mention, we
must acknowledge that the verification itself does not say that the
program is correct (wrt the "informal yet correct" specification).

That is, the formal approach might help to improve software quality, but
it is no guarantee of bug-free software.

Why I said "might" above? I postulate that there will be cases where
experts will consider more trustworthy a program written on a
traditional but convenient language than other which passed
verification. This is because some formal specifications will look more
suspicious than a program that implements the informal specification,
because of the constraints imposed by the formalization process.

> Specifically, several of those “bugs” are errors in describing the
> behavior of the environment in which the program is assumed to run. One
> possible view in this circumstance is that the program *is* correct, but
> it was run in an environment where the formal guarantees does not apply.
> This is similar as how one can prove the implication that *if* ‘X’ is a
> real number *then* ‘X^2≥0’. Suppose somebody applies the conclusion
> where the antecedent fails; for example, in the complex numbers, then
> the conclusion is false, but so is the antecedent, so there is no
> contradiction here.
>
> There is also the issue of having a fundamentally unsound logic. We can
> reason about this risk as follows: The underlying logic of many proof
> assistants is, or can, be proved sound (note that soundness implies
> consistency) assuming that ZFC is consistent. In turn we have reasons to
> believe that ZFC is consistent (I will not elaborate on that because it
> deviates too much from the original topic of this conversation).

Oh! the consistence of ZFC! now we are on pure mathematical land! :-)

Software is an industry. We must provide what is requested from us, in
terms of functionality, performance and cost (both in time and money).
Formal methods are being proposed as (yet another) silver bullet, which,
as every other silver bullet we were sold on the past, will fail to
deliver its grandiose promise. An improvement? absolutely. For some
types of software formal verification is a huge advance. But for other
classes of software (see it? types/classes :-) its impact will not go
further than the indirect improvement gained from building upon solid
implementations of algorithms, at least on the cases where the price to
pay on performance is not too much.

>> Instead of writing a lengthy explanation about why formal verification
>> can't be a guarantee about the correctness of a piece of sotware, I'll
>> simply reference a study about failures on verified systems:
>> 
>> https://blog.acolyer.org/2017/05/29/an-empirical-study-on-the-correctness-of-formally-verified-distributed-systems/
>
> The paper is of interest to me. Thanks for bringing it into my
> attention. I only took a glance but maybe I will eventually read it with
> detail. The blog post is just padding; you should have linked the paper
> directly.

You are welcomed. The blog post is a good comment on the paper that
exposes the gist of it and might be of interest to non-experts or people
who is too busy.