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

[Bakul Shah]

On Aug 18, 2018, at 12:57 PM, Perry E. Metzger <perry at 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 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.

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+.

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