On Sun, 19 Aug 2018 21:01:10 -0700 Bakul Shah <bakul(a)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(a)piermont.com