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

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

[bakul]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 5031 bytes --]

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.

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

[perry]

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