[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: Fri, 22 Sep 2017 15:12:01 -0500
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.3.0

On 22/09/17 02:48, Emanuel Berg wrote:
> It would be interesting to see the original
> code that created this vulnerability. I mean,
> so you know what *not* to write... ehem.

That is the problem with nearly all contemporary programs: Instead of
verifying that they are correct; it is verified that they are not
incorrect according to a small set of ways in which a program may be
incorrect. This idea doomed to fail is the foundation of conventional
testing, SMT testing (as in Klee), lint-like tools and manual source
code auditing.

Paraphrasing Dijkstra, all these methods can prove that a program is
incorrect, but almost never (only trivial toy programs) can prove that
it is correct.

Only verifying that programs are correct using formal logic and an
appropriate specification can eliminate software bugs (hardware can
always malfunction, because of ionizing radiation, “metastability” of
flip-flops, because somebody disconnects the power cord, and many other

At present there is limited infrastructure for verified programming, but
it can be done. See e.g.:

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]