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

[Mario Castelán Castro]

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

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

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.

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.

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

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

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan

signature.asc
Description: OpenPGP digital signature