[COFF] [TUHS] Formal Specification and Verification (was Re: TUHS Digest, Vol 33, Issue 5)

[Perry E. Metzger]

On Sun, 19 Aug 2018 21:01:10 -0700 Bakul Shah <bakul at bitblocks.com>
wrote:
> > At this point, we have a good definition. A formal specification
> > is a description of the behavior of a program or piece of
> > hardware in a precise machine-readable form that may be used as
> > the basis for fully formal verification of the behavior of an
> > implementation. Often these days, the specification is given in a
> > formal logic, such as the predicative calculus of inductive
> > constructions, which is the logic underlying the Coq system.
>
> What about Denotational Semantics?

Orthogonal. You can have a denotational semantics that is expressed
formally in Coq, or a denotational semantics that's expressed
informally on paper. Similarly for the rest. (BTW, at the moment,
operational semantics are generally considered superior to
denotational for a variety of practical reasons that aren't worth
getting into here at the moment.)

> Or efforts such as Dines
> Bj__rner's META-IV[1] and later VDM? I'd consider them formal
> specification systems even if not machine-readable or fully
> automatically verifiable.

Those are no longer considered "formal" in the community. If it isn't
machine checkable, it isn't formal.

> Perhaps the definition has tightened
> up now that we have things like Coq and Lamport's TLA+.

Precisely.

> > Formal specifications good enough for full formal verification
> > have been made for a variety of artifacts along with proofs that
> > the artifacts follow the specification. There's a fully formally
> > verified C compiler called CompCert for example, based on an
> > operational semantics written in Coq. There's another formal
> > semantics for C written in K, which is a rather different formal
> > system. There's a verified microkernel, seL4, whose specification
> > is written in Isabelle/HOL. There's a fully formal specification
> > of the RISC V, and an associated verified RTL implementation.  
> 
> seL4's verification is described here:
> https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
> 
> They used Haskell to implement an "intermediate layer"
> between OS implementers and formal methods practitioners.
> The *generated* Isobelle scripts weigh in at 200K lines so
> I don't yet know what to think of this.

That's not quite correct. What they did was build a model of the OS
kernel in Haskell and then use it to derive Isabelle/HOL
semantics. They then produced a C implementation they believed was
observationally equivalent, and generated Isabelle/HOL descriptions of
what that C layer did using a C semantics they had created, and then
proved the two observationally equivalent.

> There are a lot
> of assumptions made and crucially, for an OS kernel, they
> sidestep concurrency & non-determinism verification by
> using an event based model to avoid dealing with async.
> interrupts. [On the other hand, this is a 2009 paper and
> more work may have been done since to improve things].

CompCert has also done a lot to improve on seL4. It has much better
guarantees on concurrency etc., and it's C semantics and compilation
are based on CompCert so they closed the loop on that stuff. As you
might suspect, a lot has happened in the last decade.

> But I still think these are merely different levels of
> abstractions. The issue then is how to prove a specification
> at a given level correct

You can't prove a specification correct. If you commit an infelicity
in specifying the C programming language, that mistake is neither
"correct" nor "incorrect". Consider what happens if there's a bad idea
in the in the paper ISO C standard -- it doesn't matter that it isn't
a good idea, it's normative.

What you _can_ do is demonstrate that a formal specification matches
an intuitive idea of what is intended by humans, but it can never be a
"proof".

Now, there's an important point here, and it ought to be underlined
and in boldface with blinking letters, but luckily for everyone this
is plain text:

**Formal verification is not a way of producing "perfect" software,
because we cannot know that we've proven everything that someone might
find important someday. It is, however, a _ratchet_.** Once you've
figured out you need some property to hold and you've proven it,
you've ratcheted and will not backslide.

If you formally verify a property, you know, for good, that this
property holds. If you prove non-interference or memory safety, that
property holds, period. When someday you discover there was a property
(say some freedom cache-timing side channels you hadn't realized was
important), you add that property to your set of properties you
verify, and once you've fixed the issue and have verified it, the
problem is gone.

That is to say: testing gives you, at best, a good guess that your
software is free of some class of problems, but verification gives you
assurance you will not backslide. You've ratcheted forward on
quality. You can't know that you've asked the right questions, but you
absolutely know what the answers are to the questions you asked, which
is not true of testing.

Even with this "imperfection", the ratchet is extremely powerful, and
formal verification is vastly, vastly better than testing. CompCert
has had a handful of issues found in its lifetime, versus tens of
thousands in any other production compiler I can name, and all those
issues were quite obscure (and none the result of a failure in
verification).

Perry
-- 
Perry E. Metzger		perry at piermont.com