[Top][All Lists]

[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 <> 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:

  "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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]