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

[Óscar Fuentes]

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

> It is true that formal verification of a program requires several times
> the effort compared to writing a comparable non-verified program (but
> with many bugs). I argue that this effort is necessary, because it is
> the only way to write correct software.
>
> I think you will agree that although writing undocumented software is
> easier than writing well-documented software, writing documentation is
> part of software development and thus undocumented software must be
> considered incomplete. In the same way, I extend this to the claim that
> formal verification is part of software development and thus unverified
> software is incomplete.
>
> Although writing incomplete software is easier than writing complete
> software, the task should not be considered solved. It is like just
> building half of a bridge. Surely it is easier than building all of it;
> but it is not enough.

It seems that you think that formal verification says that the software
is correct. That's in theory. Practice is different, as usual.

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/

  "Through code review and testing, we found a total of 16 bugs, many of
   which produce serious consequences, including crashing servers,
   returning incorrect results to clients, and invalidating verification
   guarantees."