I have not read the ukernel code, but I would imagine that most of the code needed to launch the multiple servers already exists, i.e. it is necessary to launch the root server. It may require re-factoring, of course. Right? It solves another immediate problem for me. I can develop the various servers without working on device drivers, I/O subsystem, ELF loader, etc. As for the OS architecture, I imagine many approaches are possible depending on the goals of the designer. The nice thing about seL4 is that it doesn't dictate any single approach. Thanks, Dave

Hi all, Just to confirm what has already been stated: while it would be possible for seL4 to load multiple images, however this is incongruent with L4 philosophy. We want to keep the kernel as small as possible to minimise the trusted computing base and maximise policy freedom. The root task can act as a loader to load multiple images according to whatever policies suit the system. One example loader we have is the capdl loader (https://github.com/seL4/capdl) which can load capabilities and set up processes based on a specification. Camkes (https://docs.sel4.systems/CAmkES/) can be used to initialise such specifications. We're working on improving our documentation and tools for setting up seL4 systems, so keep an eye out in the coming year. Cheers, Anna. ________________________________________ From: Devel on behalf of Andrew Warkentin Sent: Sunday, 16 December 2018 3:16 PM To: devel@sel4.systems Subject: Re: [seL4] Multiboot and extra modules On 12/15/18, Dave Richards wrote:

I have not read the ukernel code, but I would imagine that most of the code needed to launch the multiple servers already exists, i.e. it is necessary to launch the root server. It may require re-factoring, of course. Right?

It solves another immediate problem for me. I can develop the various servers without working on device drivers, I/O subsystem, ELF loader, etc.

Yes, there's code to launch the root server, but it's not particularly general, and is just enough to set up the state for the root server's initial thread. It would probably be non-trivial to make it general enough to load multiple servers. Personally I don't think that the kernel should be setting up state for multiple servers though. I'd say that it should leave it up to the root server (my chain-loader's ELF preloading code would make that relatively easy to do from a root server without an ELF loader built in. although UX/RT's root server will just use its own built-in loader since it will treat modules as files rather than processes, and will only start /sbin/init directly, with init starting all other processes; I think a microkernel OS should have as few "special" servers as possible).

As for the OS architecture, I imagine many approaches are possible depending on the goals of the designer. The nice thing about seL4 is that it doesn't dictate any single approach.

What kind of OS are you trying to write? UX/RT is going to be a QNX-like OS with some concepts from Plan 9 thrown in, as well as a high degree of Linux compatibility. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

On 17 Dec 2018, at 21:49, Andrew Warkentin mailto:andreww591@gmail.com> 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. Gernot

At 2018-12-17T11:49:58+0000, 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? 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. 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). At the same time, my intuition is that a theorem prover should be harder to Trojan than a compiler. When Thompson famously subverted the C compiler[1], he apparently did simple (but effective) pattern-matching on strings (in the symbol table, I suppose) to recognize whether the program being compiled was "login", the disassembler, or the C compiler itself. With knowledge of that trick in mind it should be straightforward to produce a version of Isabelle/HOL with symbols arbitrarily renamed. The challenge for attackers then is to develop a backdoor that can recognize a theorem prover by data flow analysis or an unlabeled call graph. And that in turn seems like[2] it should be practically impossible to do without invalidating the theorem prover for other purposes, which exposes the fact of its compromise[3]. This in turn is an argument for having proofs for many more components of the system, not just the kernel; even small and simple ones can contribute to building confidence that the theorem prover has not been subverted, and it also will help us build a literature for teaching the next generation of software engineers how to prove their programs. Imagine an update of Kernighan & Plauger's _Software Tools_ (1976), wherein the reader is taught not only how to develop modular, reusable software components, but how to validate their correctness as well. I can't help thinking that a brighter future lies ahead--a future that is only eight to fourteen years away. ;-) To return from my digression, what is the distance from the status quo to a trusted computing base sufficient to build and validate seL4? Regards, Branden [1] https://www.archive.ece.cmu.edu/~ganger/712.fall02/papers/p761-thompson.pdf [2] I apologize for repeated recourse to my own instinct and intuition to support my assertions; I raise the issues here not to flaunt my ignorance but because I hope the experts here can point me and other interested readers to the real literature on the subject raised. [3] I note also that running coverage analysis of Thompson's subverted C compiler against the Unix sources themselves should also have revealed the fact of its compromise. To truly escape detection, a Thompson-style Trojan must not only recognize the source code of all the tools that might be brought to bear against the subverted executable, but those developed in the future, which is too large a space to tractably exhaust in anticipation--at least in a thriving software ecosystem like that of Unix and its descendants. The pessimism that Thompson expresses is therefore not warranted on technical grounds--but it may still be for cultural ones, in that we don't have enough people subjecting compiled objects to skeptical analysis. Hence formal verification.

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.