[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: CVE-2017-14482 - Red Hat Customer Portal
From: |
Óscar Fuentes |
Subject: |
Re: CVE-2017-14482 - Red Hat Customer Portal |
Date: |
Sun, 24 Sep 2017 16:42:54 +0200 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/26.0.50 (gnu/linux) |
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."
- CVE-2017-14482 - Red Hat Customer Portal, ken, 2017/09/21
- Re: CVE-2017-14482 - Red Hat Customer Portal, Kaushal Modi, 2017/09/21
- Re: CVE-2017-14482 - Red Hat Customer Portal, ken, 2017/09/21
- Re: CVE-2017-14482 - Red Hat Customer Portal, Alberto Luaces, 2017/09/22
- Re: CVE-2017-14482 - Red Hat Customer Portal, Emanuel Berg, 2017/09/22
- Re: CVE-2017-14482 - Red Hat Customer Portal, Mario Castelán Castro, 2017/09/22
- Re: CVE-2017-14482 - Red Hat Customer Portal, Emanuel Berg, 2017/09/22
- Re: CVE-2017-14482 - Red Hat Customer Portal, Mario Castelán Castro, 2017/09/23
- Message not available
- Re: CVE-2017-14482 - Red Hat Customer Portal, Emanuel Berg, 2017/09/24
- Re: CVE-2017-14482 - Red Hat Customer Portal, Mario Castelán Castro, 2017/09/24
- Re: CVE-2017-14482 - Red Hat Customer Portal,
Óscar Fuentes <=
- Re: CVE-2017-14482 - Red Hat Customer Portal, tomas, 2017/09/24
- Re: CVE-2017-14482 - Red Hat Customer Portal, Narendra Joshi, 2017/09/26
- Re: CVE-2017-14482 - Red Hat Customer Portal, Emanuel Berg, 2017/09/24
- Re: CVE-2017-14482 - Red Hat Customer Portal, Mario Castelán Castro, 2017/09/25
- Re: CVE-2017-14482 - Red Hat Customer Portal, Emanuel Berg, 2017/09/25
- Re: CVE-2017-14482 - Red Hat Customer Portal, Mario Castelán Castro, 2017/09/25
- Re: CVE-2017-14482 - Red Hat Customer Portal, Emanuel Berg, 2017/09/25
- Re: CVE-2017-14482 - Red Hat Customer Portal, Mario Castelán Castro, 2017/09/25
- Re: CVE-2017-14482 - Red Hat Customer Portal, Óscar Fuentes, 2017/09/25
- Re: CVE-2017-14482 - Red Hat Customer Portal, Mario Castelán Castro, 2017/09/26