[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Mario Castelán Castro
Subject: Re: CVE-2017-14482 - Red Hat Customer Portal
Date: Mon, 25 Sep 2017 16:23:49 -0500
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.3.0

On 24/09/17 18:06, Emanuel Berg wrote:
> Hold - perhaps the verification has to be
> verified as well?

What any proof of correctness proves is an implication saying roughly:
“IF the environment meets these requisites THEN the program does […]”.

The “bugs” described in the aforementioned paper are not a flaw in the
proof. The source of the problem is that EITHER the programs under test
were being used in an environment does not meet the requisites (i.e.:
“IF the environment meets”) OR the user was expecting the program to do
something different than what is guaranteed by the conclusion “the
program does […]”.

> C'mon now, this is just another
> Computer Science hangup. Just like
> functional programming, or testing for that
> matter - which also is an academic pursuit, by
> the way! [1] - but as always, there is no
> silver bullet solution.

This is the prevalent attitude among programmers, and this is the reason
that we are showered by an endless stream of security patches and bug fixes.

> If I'd send the space fleet to the oldest
> galaxies of the universe, I'd like all methods
> anyone could think of to make as sure as
> possible the software is correct.
> I'd start with very skilled and motivated
> programmers, proceed with sound programming
> practices, then code review, and then
> excessive testing.
> I suppose formal verification would be
> a distant fourth.

Well, then it is a very good thing that you are NOT in charge of
designing that piece of software.

Do not eat animals; respect them as you respect people.

Attachment: signature.asc
Description: OpenPGP digital signature

reply via email to

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