Signed PGP part At 2018-12-17T11:49:58+0000, Gernot.Heiser@data61.csiro.aumailto:Gernot.Heiser@data61.csiro.au wrote: CAmkES is good for building static embedded systems (excluding stuff running in VMs), but can't really do anything more AFAIK. Yes, CAmkES is designed for static architectures, which is where we can give an assurance story. If you want something dynamic, i.e. more resembling a full OS, then have a look at Genode. But then all assurance and ability to reason about security properties goes out of the window. 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. In dynamic systems, that kind of automation will be much harder to achieve, and the properties that you get will likely be either weaker or more complex to formulate. This means, to get verified properties of a CAmkES system, you only need to use the CAmkES tool chain, but to get verified properties of a dynamic system, you will need to invest manual work (at least in the foreseeable future — there are probably classes of things that can be automated there as well, but that’s vague ideas instead of production-ready tools in the next few years). 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. 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. Naturally, the theorem prover itself has to be added to the list of "assumed valid" components; we can't use it to verify itself without disproving Gödel (I think). 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. In essence, you will not have used the prover to verify itself, but you will have used a different prover. There is a project that does exactly that, and we’re very much looking forward to using that prover as a proof checker for the seL4 proofs (the CakeML language already works on top of seL4 in CAmkES components): 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. Hopefully much fewer than 8 years. Cheers, Gerwin