At 2018-12-17T22:00:07+0000, [email protected] 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.pdfo [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.
signature.asc
Description: PGP signature
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
