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

[Mario Castelán Castro]

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
things).

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

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan

signature.asc
Description: OpenPGP digital signature