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

[Emanuel Berg]

Mario Castelán Castro wrote:

> 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. [...]

Also, formal verification that is applied on
a model will only prove that *the model* is
correct, not the real thing.

There is one automated way of testing that
I know of that actually works, and that is for
shell tools that have the super-simple text
interface where the tool accepts a limited set
of arguments. Say that it accepts one integer
as the first argument and then one string as
its second. Then it is trivial to setup a test
program that will just invoke repeatedly with
randomized integers and strings. Because its
random, it might find borderline cases which
makes absolutely no sense (but still shouldn't
break the program), but which supposedly
rational human beings would never think of
to input, and thus without the test program,
would never get tested.

But for a huge software system like Emacs,
formal verification being obviously out of the
question, even simple-minded brute-force
testing is difficult to set up, at least for
anything bigger than the smallest module.el.
So the byte-compiler and style checks
(`checkdoc-current-buffer') is what you got.

Instead, I think the best way to test is just
to have lots of people using it. At least major
flaws will surface really soon this way.

There are also languages like Dafny where you
can state formally what a function should do,
and the verification tool will match that to
your code. Problem is, it isn't refined to any
degree where it actually will matter for
every-day programming. Often, the code will be
correct, and the formal description is correct
as well, only the verifier will still say it
doesn't compute. And programming should
obviously not be about tinkering with code and
expressions that already makes sense, just so
that the computer will agree it does.
So straight down the line, this will amount to
toy/demo programs as well.

Here is an example:

    method Main () {
      var n := f(4, 5);
      print "The result is ";
      print n;
    }

    method f(a:int, b:int) returns (r:int)
      requires a >= 0;
      requires b >= 0;
      ensures  r == 4*a + b;
    {
      r := 0;
      var i := 0;
      var j := 0;
      while (i < a || j < b)
        decreases a + b - (i + j);
        invariant 0 <= i <= a;
        invariant 0 <= j <= b;
        invariant r == 4*i + j;
      {
        if (j < b) {
          r := r + 1;
          j := j + 1;
        }
        else {
          r := r + 4;
          i := i + 1;
        }
      }
    }

There is a Dafny mode for Emacs, and with Mono
(because it is an .NET thing to begin with),
perhaps one could hook that up into a neat IDE.
Still, it will only amount to poor Dafny.

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