[seL4] Re: seL4 service discovery question

On Wed, 7 Apr 2021 at 19:27, Matt Rice wrote:

It is a bit difficult to introduce string -> capability lookups without introducing some form of ambient authority, where the object connectivity graph of a typical capability system is heavily reliant on application and services having direct connectivity. service managers of the sort introduce a difficult many to many applications -> service manager, service manager -> services type of object graph, which in turn loses many valuable properties...

historically capability systems have typically avoided introducing such a mechanism. Instead relying on some kind of reflection mechanism or protocol. Some systems (keykos and eros) had an allegedType message that could be sent to capabilities, so if you know the allegedType of a network capability,

I can't speak for EROS as I don't have the full source, but its descendant CapROS only supports static association of an application with the network driver. https://gitlab.com/william-ml-leslie/capros/-/blob/master/src/tutorials/http... For something like network access which tends to be a static requirement of an application, a slightly more capability-oriented pattern would be to include network access in an application manifest, to be granted at install time (or stubbed, or switched on/off via the system settings menu), as approximated by mobile operating systems. The manifest could limit access to specific interfaces and ports, or to addresses obtained by resolving a limited set of hostnames (though think carefully about exactly what that buys you).

On Tue, Apr 6, 2021 at 1:56 PM Royce Mitchell III wrote:

...

How would:

1) the "network" service advertise its services as available via IPC?

2) an application locate this "network" service to be able to IPC with it?

I assume the mechanisms here would also apply to interactions between services as well. I picked the "network" service in this example only because it would be the boundary between application and OS services.

I'm guessing that maybe this is purely an OS design decision and not the purvue of the kernel itself. Perhaps init could launch a "service manager" process that would be responsible for starting up services and drivers for example and this "service manager" could provide an IPC endpoint back to init (or whomever) to use for IPC discovery. Then, whenever a new process is started, it is provided with the IPC discovery endpoint information that it is to inherit.

If my assumptions are correct or close, or even dead wrong, would someone be willing to share some pseudo-code on what this could/should look like in seL4?

If a central service manager is needed to glue the core OS together, does it represent a single point of failure and how would the OS recover if it crashes and loses it's database of available services without having to rebuild and restart all drivers and services? (I'm not saying that's a bad thing, just trying to wrap my head around how this particular part of seL4 works)

You've got the gist. It's central to the operating system design what the initial grant is to applications and services. The equivalent of an RC system or a service for managing the lifecycle of user sessions would need to have some degree of policy for what capabilities to hand out to the services they start. For some idea of what that looks like, you might enjoy the source of the Eros Window System, which was prescriptive about who could place what windows and where, and about how input could flow to each one, but left the actual policy of what to do up to the window manager (and I'm terribly sorry that I don't have the source for a single one, as neither WM nor display driver was ever shipped with CapROS that I know about). https://gitlab.com/william-ml-leslie/capros/-/tree/master/src/base/domain/wi... To support existing applications (e.g. via WASI), you may have a small set of naturally inherited capabilities representing the filesystem, network, controlling terminal etc. It will probably become natural to substitute these at service boundaries according to need. c.f. https://git.savannah.gnu.org/cgit/hurd/hurd.git/tree/hurd/hurd_types.h#n367 -- William Leslie Q: What is your boss's password? A: "Authentication", clearly Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement.