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

[Emanuel Berg]

Óscar Fuentes wrote:

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

Hold - perhaps the verification has to be
verified as well?

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.

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.

[1]

@book{ammann,
    author    = {Paul Ammann and Jeff Offut},
    title     = {Introduction to Software Testing},
    publisher = {Cambridge University Press},
    year      = 2008,
    ISBN      = {978-0-521-88038-1},
    edition   = {6th edition}
}

-- 
underground experts united
http://user.it.uu.se/~embe8573