Re: [COFF] [TUHS] Formal Specification and Verification (was Re: TUHS Digest, Vol 33, Issue 5)
20 Aug
2018
20 Aug
'18
4:01 a.m.
On Aug 18, 2018, at 12:57 PM, Perry E. Metzger <perry(a)piermont.com> wrote:
Sorry for the thread necromancy, but this is a _very_ important
topic. Perhaps it doesn't belong on tuhs but rather on coff.
Surely 12 days is not all that long a period?!
This is a pretty long posting. If you don't care
to read it, the TL;DR
is that formal specification and verification is now a real
discipline, which it wasn't in the old days, and there are systems to
do it in, and it's well understood.
On 2018-08-06 at 08:52 -0700, Bakul Shah wrote:
What about Denotational Semantics? 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. Perhaps the definition has tightened
up now that we have things like Coq and Lamport's TLA+.
What counts as a "formal spec"? Is it like Justice Potter
Stewart's "I know it when I see it" definition or something
better?
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.
Isabelle/HOL is another popular system for this sort of work. ACL2 is
(from what I can tell) of more historical interest but it has
apparently been used for things like the formal verification of
floating point and cache control units for real hardware. (It is my
understanding that it has been many years since Intel would dare
release a system where the cache unit wasn't verified, and the only
time in decades it tried to release a non-verified FPU, it got the
FDIV bug and has never tried that again.) There are some others out
there, like F*, Lean, etc.
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. 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].
Generally speaking, a formal specification:
1) Must be machine readable
2) The semantics of the underlying specification language must
themselves be extremely precisely described. You can't prove the
consistency and completeness of the underlying system (see Gödel)
but you _can_ still strongly specify the language.
3) Must be usable for formal (that is, machine checkable) proofs that
implementations comply with the spec, so it has to be sufficiently
powerful. Typical systems are now equivalent to higher order logic.
...
In recent years, I've noted that "old
timers" (such as many of us,
myself included) seem to be unaware of the fact that systems like Coq
exist, or that it is now relatively (I emphasize _relatively_) routine
for substantial systems to be fully formally specified and then fully
formally verified.
This is good to know.
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 and how to prove that the mapping
to a more concrete level implements the same semantics.
I also wonder about the "_relatively_ routine" application
of formal verification. May be for the Intels of the world
but certainly not for 99.99..9% of software. Though hopefully
it *will* become more common.
Thanks to Hellwig Geisse, Noel Chiappa, Steve Johnson, &
especially Perry Metzger for their replies.
Bakul
[1]
Aside: I sort of stumbled upon this area decades ago when
I picked up a stack of tech. reports Prof. Per Brinch-Hansen
had thrown out. It had among other things Bjørner's tutorial
on META-IV and Sussman & Steele's orig. Scheme report. These
led me to denotational semantics via Milner & Strachey's
Theory of Programming Language Semantics book.
20 Aug
20 Aug
12:23 p.m.
New subject: [TUHS] Formal Specification and Verification (was Re: TUHS Digest, Vol 33, Issue 5)
On Sun, 19 Aug 2018 21:01:10 -0700 Bakul Shah <bakul(a)bitblocks.com>
wrote:
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.)
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.
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? 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. 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
2069
days inactive
2069
days old
1 comments
2 participants
participants (2)
-
Bakul Shah -
Perry E. Metzger