seL4 kernel is formally verified

[Marcus Voelp]

Hi Nicholas,

Nicholas Mc Guire wrote:
> What did supprise me a bit is that: 
>
>  7500 LoC yield 200k Lines of formal proof
>  7500 LoC yield "more than 10k intermediate theorems
>
> I wonder how scalable such an approach is... And of course raising (from a 
> safety perspective) the question if the complexity and potential failures of
> 7.5k of Code were not replaced by a even higher complexity (of course its
> a diverse representation - which takes out a lot of this imediately)
>   
the question is whether lines of Isabelle code, lines of Isabelle proof
script and number of intermediate theorems is really a good metric to
judge about the trustworthiness of the model and the corresponding proofs.

In Robin (sources are here:
http://robin.tudos.org/robin-hw-model-2008-05-15.tgz), we ended up with
approx. 20K LOC of PVS code for the somewhat detailed C++ / Hardware
model. However, most of this code is not to describe the model but to
establish higher level results. There is for example a rather lengthy
proof that establishes that under a bunch of preconditions virtual
memory behaves as normal unaliased memory. That is reading and writing
have the desired property and do not cause side effects (e.g., due to
virtual memory aliases).

The specification of the page-table walker is only about 50 LOC (plus
another 50-100 LOC for the reading and writing page-table entries rather
than bytes). The actual lemma boils down to a number of results such as:

data(read (a1) ; read (a2)) = data(read (a2))

which means the first read to address a1 has no side effects on the data
returned by the second read.

The LOCs for the auxiliary lemmas that were necessary to produce these
results are however in the order of 1500 LOC (proof commands not included).

If you would trust PVS to work correctly (which is critical due to some
reported soundness bugs) all you need to do is to agree with the +- 100
lines of specification and with the lemma results. The intermediate
stuff you can just skip.

A second point is that proof commands in PVS (and also in Isabelle) have
different power. For example, the comand expand just replaces a lemma
with its definition --- a step you can easily follow --- the command
grind however applies almost all known simplification techniques at
once. Thus you have a 1 line proof is grind works and a 100+ line proof
if you would apply the respective simplification steps by hand.

I would therefore very much like to see Nicta's Isabelle code for the
model and for the final lemmas at least.

Best Regards

    Marcus