20 Aug
2018
20 Aug
'18
10: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.