At 2018-12-17T22:00:07+0000, Gerwin.Klein(a)data61.csiro.au wrote:
To invert a
classic naïve programmer's question, isn't that true only in
practice?
Yes, that is a problem only in practice, not in theory.
I.e. it is perfectly possible, just hard and work intensive to have a
verified dynamic system. We even have a PhD project looking to make
first steps in that direction. The main difference is that for static
systems, it is (relatively) easy to provide automation for
verification, and the CAmkES toolchain will be able to produce proofs
automatically for you that it has implemented the desired
architecture, which then plugs into the seL4 security theorems. It’s
basically free for the user of the toolchain.
That's an exciting value proposition.
In principle,
once sufficient components are in place for seL4 to
host its own build dependencies including the theorem prover, then it
is a general enough development environment to compile and verify
arbitrary extensions.
Yes. It’s even easier than that: you only need to be able to host a
proof checker, not a full theorem prover.
This makes it even more likely that we will eventually see a diversity
of proof checkers. For many years I've been used to thinking in terms
of security as being a matter of "reducing attack surface", which can be
concretized in many ways from number of open network ports to lines of
code; it is noteworthy to me that we stand to actually benefit by
writing more code, when that code is part of a diverse polyculture (cf.
monoculture) deployed for the purpose of mutual verification.
Of course this idea is not original to me; it is a generalization of
what I first encountered in David Wheeler's paper on "Diverse
Double-Compiling"[1].
You can then produce the proof on a different system,
but check it on
a verified system. Proof checking is vastly simpler (and faster) than
proof search.
I seem to remember having had a conversation like this before; it pays
to remember that we don't always need the heavy lift of a prover.
Incompleteness is overrated :-). It is true, of
course, but the
incompleteness theorem only bites, if you use precisely the logic that
the prover implements for the verification of the prover itself. If
you change only one of the axioms to something less powerful and still
manage to verify your prover, the incompleteness theorem does not
apply, and you still have a very verified prover.
That's exciting but it gets me to wondering abstractly. Consider a pair
of provers A and B which are duals in some sense. Each one has been
weakened as you describe, but in different ways. Because I am not
competent to contrive a believable example, I must settle for a dubious
one[2]. Let us say that prover A cannot decide logical ORs, and prover
B cannot decide logical ANDs. If--and it may be a big if--we can verify
each of these two provers by using the other, then have we not solved
every class of problem equivalent to Hilbert's Second Problem[3]?
Of course, if two provers don't suffice to make this demonstration, we
need not stop at two. As long as we can construct a set of provers of
finite cardinality, each appropriately weakened, then assuming unbounded
computing resources we have achieved the same thing.
I assume there is some result in mathematical logic which has foreclosed
this possibility. Perhaps that it is impossible to construct a finite
set of mutually reinforcing provers. I would have guessed that your
statement that we can use a weakened prover to verify a stronger one was
already foreclosed by incompleteness. If not, you have persuaded me
that generations of computer scientists have overestimated what,
exactly, was foreclosed by Gödel.
I should refresh myself with Nagel and Newman in the near future.
https://github.com/CakeML/cakeml/tree/master/candle
Given that you could even leave out file system and most other
infrastructure by baking a proof representation into the image that is
loaded into memory at boot, a fully verified binary-level proof
checking system is not that far off once the Candle prover is usable
and we have a powerful-enough export tool from Isabelle (which we use)
into Candle.
I now imagine an object loader which invokes the proof-checking system,
coupled with "fat binaries" that embed proofs about themselves inside a
dedicated ELF section.
Hopefully much fewer than 8 years.
I admit that my time projection is due entirely to the Coen Brothers and
not any sort of engineering estimate.
Regards,
Branden
[1]
https://dwheeler.com/trusting-trust/dissertation/wheeler-trusting-trust-ddc…
[2] My example is unconvincing because NOR is a functionally complete
operator for Boolean logic. That is, one can construct both AND and OR
operators through appropriate combinations of NOR gates.
https://en.wikipedia.org/wiki/Functional_completeness
[3] This is the one that Whitehead and Russell purported to have
cracked, only for Gödel to have kicked the football away.