At 2018-12-17T22:00:07+0000, Gerwin.Klein@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.