Thank you for the response! A pre-compiled configuration helps the whole thing start to make a lot more sense for me. My interest in microkernels and in seL4 in particular is in a more reliable desktop computing experience. While security is certainly important, avoiding a need to reboot is important too. I know I can run Linux in a VM, but if that VM crashes, I still lose my work. Additionally, I did some volunteering for ReactOS a long time ago and found kernel mode development extremely frustrating. I love the idea of being able to help write drivers and it be orders of magnitude easier troubleshooting the driver when it misbehaves. Royce Mitchell, IT Consultant ITAS Solutions royce3@itas-solutions.com There are three hard problems in computer science: naming things, and off-by-one errors. On Tue, Apr 6, 2021 at 3:06 PM Chubb, Peter (Data61, Eveleigh) < Peter.Chubb@data61.csiro.au> wrote:
Hi Royce,
The systems we've built so far have been described completely at build time: there's no need for sevice discovery because all services are known, and all connections between them established at boot time by the root server. This is desirable when building a very secure system --- it allows infoflow analysis of who can talk to what, and it's guaranteed that information flows cannot be changed (in terms of which components can talk to each other) while the system is running.
If you want to build a more dynamic system, you're right: you'd need some kind of directory service that allows components to register what they can do. That's out of scope for the microkernel, but is needed as part of a complete dynamic system.
-- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)