Hi all, I've been passively following seL4 for several years. I've been reading the documentation, tutorials, watching YouTube videos.
The concepts behind capabilities and other types of kernel objects are starting to sink in but there's one piece of understanding that's eluding me.
If I just haven't stumbled across it yet in the documentation, then pointing me in the right direction would be greatly appreciated.
Given:
* An ethernet driver named "e1000" and 2 devices "eth0" and "eth1" controlled by that driver.
* A "tcp" service that would implement that network protocol.
* A higher level service named "network" that implemented some kind of networking abstraction for us.
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)
Thanks,
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.
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.
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)
On 7 Apr 2021, at 06:31, Royce Mitchell III <royce3@gmail.commailto:royce3@gmail.com> wrote:
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.
There’s no seL4-based desktop available out of the box, but there are ways to get there.
One is Genode.orghttp://Genode.org, an OS framework that provides a complete, componentised desktop environment on top of a microkernel. While core functionality of Genode runs on seL4, it doesn’t support the full OS yet.
Another approach is to port Qubes OS to seL4. We have made some investigations on this in the past, and there’s talk about third-party funding for this, but nothing concrete yet.
Gernot
Apologies for the lost quoting in the previous mail, not sure where it gets dropped. Trying again (doing it manually)
On 7 Apr 2021, at 06:31, Royce Mitchell III <royce3@gmail.commailto:royce3@gmail.com> wrote:
| 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.
There’s no seL4-based desktop available out of the box, but there are ways to get there.
One is Genode.orghttp://Genode.org, an OS framework that provides a complete, componentised desktop environment on top of a microkernel. While core functionality of Genode runs on seL4, it doesn’t support the full OS yet.
Another approach is to port Qubes OS to seL4. We have made some investigations on this in the past, and there’s talk about third-party funding for this, but nothing concrete yet.
Gernot
PS: There’ll soon be a white paper on secure OS design...
On 4/6/21, Royce Mitchell III royce3@gmail.com wrote:
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.
UX/RT, the OS that I'm writing, will implement service discovery similarly to QNX Neutrino or Plan 9. All services will be discovered exclusively through the filesystem. Each process will be provided with a permanently-open file descriptor allowing it to communicate with the VFS and open more files. File descriptors will be implemented as a thin wrapper over seL4 IPC, and read/write/seek-family APIs will communicate directly with other processes rather than being forced to go through a specific intermediary server (this will eliminate the chicken-and-egg problem that would otherwise occur when trying to communicate with the VFS itself over a file-based transport).
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)
UX/RT will have the VFS and process/memory management built into the root server and all other services implemented as regular processes with no special semantics, much as under QNX (although of course the process/root server won't be built into the kernel as in QNX). The VFS will be way too intertwined with memory management to separate it out (UX/RT will be the only OS I'm aware of in which literally everything is a file; even anonymous memory will be replaced with mapped files in a tmpfs), so I'm not going to bother with trying to allow recovery from VFS crashes, at least not at first. The root server will be written in Rust so it will have a lower risk of memory bugs than if it were written in C.
On Tue, Apr 6, 2021 at 1:56 PM Royce Mitchell III royce3@gmail.com wrote:
Hi all, I've been passively following seL4 for several years. I've been reading the documentation, tutorials, watching YouTube videos.
The concepts behind capabilities and other types of kernel objects are starting to sink in but there's one piece of understanding that's eluding me.
If I just haven't stumbled across it yet in the documentation, then pointing me in the right direction would be greatly appreciated.
Given:
- An ethernet driver named "e1000" and 2 devices "eth0" and "eth1"
controlled by that driver.
A "tcp" service that would implement that network protocol.
A higher level service named "network" that implemented some kind of
networking abstraction for us.
How would:
the "network" service advertise its services as available via IPC?
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)
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, and the messages it receives or a IDL description of the network capability associated with the allegedType, you could dynamically send it messages to which it purports to understand. This is somewhat a matter of convention, I'm not certain if there is any such thing built in to sel4 tooling e.g. to generate unique alleged types for camkes interfaces and a well-known message to dynamically query them. it sounds like there is not though.
The general benefits of this is that given some enumerable set of capabilities it allows some process to filter the interesting ones, rather than introducing any new connectivity + single point of failure
On 4/7/21, Matt Rice ratmice@gmail.com 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...
That's one of the reasons why UX/RT won't be a pure capability system (compatibility with legacy Unix code without relegating it to a "penalty box" is another major one). Any general-purpose OS needs to have some facility for giving objects names that are meaningful to humans.
UX/RT will use a per-process ACL-like mechanism for files to which access can be authorized statically. For files to which access is granted by another process, either a file descriptor transfer or a "path capability" mechanism will be used. To use the path capability mechanism, the granting process will write the path of a file into the grant list of the receiving process, creating a new path capability file in the process directory (these will be named with integer IDs in a separate space from FDs). The receiving process will then open this file, with the open being directed to the granted path according to both the namespace and permissions of the granting process rather than those of the receiving process. This will allow re-opening and deletion of granted files unlike with file descriptor transfers, but will still mitigate the risk of confused deputy vulnerabilities.
On Wed, 7 Apr 2021 at 19:27, Matt Rice ratmice@gmail.com 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 royce3@gmail.com wrote:
How would:
the "network" service advertise its services as available via IPC?
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
On Wed, 7 Apr 2021 at 22:13, William ML Leslie william.leslie.ttg@gmail.com wrote:
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.
Oh, I should probably clarify with an example: when porting setuid binaries, the common practice (at least to a first order) is to have the "normal" filesystem be the default root filesystem of the exec server, but to also gain a capability to the caller's filesystem to use for resolving user-provided filenames. It's not ideal, and yet already a huge step forward over the unix permissions model.
On 4/7/21, William ML Leslie william.leslie.ttg@gmail.com wrote:
On Wed, 7 Apr 2021 at 22:13, William ML Leslie
Oh, I should probably clarify with an example: when porting setuid binaries, the common practice (at least to a first order) is to have the "normal" filesystem be the default root filesystem of the exec server, but to also gain a capability to the caller's filesystem to use for resolving user-provided filenames. It's not ideal, and yet already a huge step forward over the unix permissions model.
That's a little bit like the path-capability mechanism I'm planning to implement, although the path-capability API will only provide paths for informational purposes such as displaying in a GUI. Also, UX/RT won't have any client-visible concept of a "capability to a filesystem" (that's way too coarse-grained for my liking; security boundaries usually don't correspond to disk partitions or network shares, and having to set up some kind of filter filesystem for every directory/file you want to control access to is cumbersome). However it will be possible to give a process access to all files in a directory (mount point or otherwise) through either its permission list or through a path capability.
On Wed, 7 Apr 2021 at 22:51, Andrew Warkentin andreww591@gmail.com wrote:
On 4/7/21, William ML Leslie william.leslie.ttg@gmail.com wrote:
On Wed, 7 Apr 2021 at 22:13, William ML Leslie
Oh, I should probably clarify with an example: when porting setuid binaries, the common practice (at least to a first order) is to have the "normal" filesystem be the default root filesystem of the exec server, but to also gain a capability to the caller's filesystem to use for resolving user-provided filenames. It's not ideal, and yet already a huge step forward over the unix permissions model.
That's a little bit like the path-capability mechanism I'm planning to implement, although the path-capability API will only provide paths for informational purposes such as displaying in a GUI. Also, UX/RT won't have any client-visible concept of a "capability to a filesystem" (that's way too coarse-grained for my liking; security boundaries usually don't correspond to disk partitions or network shares, and having to set up some kind of filter filesystem for every directory/file you want to control access to is cumbersome). However it will be possible to give a process access to all files in a directory (mount point or otherwise) through either its permission list or through a path capability.
There's nothing to say that a filesystem is a disk partition or such; in CapROS at least you could be handed access to a Directory which is a map to as few or as many capabilities as you like, which may or may not be references to Files or Directories. I have heard stories that KeyKOS has access to a unix-style filesystem, but in all the descendants I have access to, directories were just normal orthogonally-persistent objects that allowed you to ask for a capability by name and any other resemblance to the unix filesystem is probably accidental.
The reason I find forwarding a reference to a filesystem an interesting concept is that you may want some applications interaction with the system state to be transactional. My favourite example is the installer. More and more installers think that it's acceptable to call sudo on your behalf (it's really not; I'm looking at you, nix and waterfox) but even if you use the standard gnu build system `$ ./configure ; $ make ; # make install` there's often no easy way to tell how it might clobber the system on `make install`. Running the installer itself within a transaction and allowing the user to inspect the changes is a great usability improvement, and the way to force the installer to submit to the transaction is to only allow it access to resources that are transaction aware (such as an overlay filesystem).
I'm aware that if you don't have any need to support legacy you can often avoid the need for such things, but that's a rare place to be in, considering we're talking about full-cream desktop operating systems.
It seems with the right vfs design you could create a command like “shadow make install” and it create a view of the file system and allow changes but those changes are stored in the shadow but not written to the actual vfs. This would allow you to do that very kind of inspection. I’ve done something like this at the application level using Python so that I could run unit tests without actually changing the file system.
On Wed, Apr 7, 2021 at 9:14 AM William ML Leslie < william.leslie.ttg@gmail.com> wrote:
On Wed, 7 Apr 2021 at 22:51, Andrew Warkentin andreww591@gmail.com wrote:
On 4/7/21, William ML Leslie william.leslie.ttg@gmail.com wrote:
On Wed, 7 Apr 2021 at 22:13, William ML Leslie
Oh, I should probably clarify with an example: when porting setuid
binaries, the common practice (at least to a first order) is to have
the "normal" filesystem be the default root filesystem of the exec
server, but to also gain a capability to the caller's filesystem to
use for resolving user-provided filenames. It's not ideal, and yet
already a huge step forward over the unix permissions model.
That's a little bit like the path-capability mechanism I'm planning to
implement, although the path-capability API will only provide paths
for informational purposes such as displaying in a GUI. Also, UX/RT
won't have any client-visible concept of a "capability to a
filesystem" (that's way too coarse-grained for my liking; security
boundaries usually don't correspond to disk partitions or network
shares, and having to set up some kind of filter filesystem for every
directory/file you want to control access to is cumbersome). However
it will be possible to give a process access to all files in a
directory (mount point or otherwise) through either its permission
list or through a path capability.
There's nothing to say that a filesystem is a disk partition or such;
in CapROS at least you could be handed access to a Directory which is
a map to as few or as many capabilities as you like, which may or may
not be references to Files or Directories. I have heard stories that
KeyKOS has access to a unix-style filesystem, but in all the
descendants I have access to, directories were just normal
orthogonally-persistent objects that allowed you to ask for a
capability by name and any other resemblance to the unix filesystem is
probably accidental.
The reason I find forwarding a reference to a filesystem an
interesting concept is that you may want some applications interaction
with the system state to be transactional. My favourite example is
the installer. More and more installers think that it's acceptable to
call sudo on your behalf (it's really not; I'm looking at you, nix and
waterfox) but even if you use the standard gnu build system `$
./configure ; $ make ; # make install` there's often no easy way to
tell how it might clobber the system on `make install`. Running the
installer itself within a transaction and allowing the user to inspect
the changes is a great usability improvement, and the way to force the
installer to submit to the transaction is to only allow it access to
resources that are transaction aware (such as an overlay filesystem).
I'm aware that if you don't have any need to support legacy you can
often avoid the need for such things, but that's a rare place to be
in, considering we're talking about full-cream desktop operating
systems.
--
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.
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
--
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 4/7/21, Royce Mitchell III royce3@gmail.com wrote:
It seems with the right vfs design you could create a command like “shadow make install” and it create a view of the file system and allow changes but those changes are stored in the shadow but not written to the actual vfs. This would allow you to do that very kind of inspection. I’ve done something like this at the application level using Python so that I could run unit tests without actually changing the file system.
It will be possible to do something like that under UX/RT because of the scoped namespace support, although the command will almost certainly require specifying a shadow directory. Actually the entire system will normally be installed with such an overlay for everything but certain embedded configurations, due to the underlying packages being treated as immutable except for adding and removing them.
On Wed, Apr 7, 2021 at 12:17 PM William ML Leslie < william.leslie.ttg@gmail.com> wrote:
On Wed, 7 Apr 2021 at 19:27, Matt Rice ratmice@gmail.com 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).
FWIW CapROS does have the mechanism I described it's somewhat hidden in the IDL compiler, Certainly install time could leverage the dynamic check of alleged type, I'm somewhat assuming you might have a capability like a crypto layer which acts as/proxies a network capability like a vpn tunnel... i.e. a capability which is not a genuine network but has one, and exposes the same interface.
https://gitlab.com/william-ml-leslie/capros/-/blob/master/src/base/domain/ne... https://gitlab.com/william-ml-leslie/capros/-/blob/master/src/sys/eros/key.i...
I do believe all the KeyKOS/EROS/CapROS/Coyotos systems had such a mechanism, can't speak for KeyKOS but it was documented, If you look at the netlistener.idl and it's lack of any presence there.
but presumably someone somewhere needs to have gotten one statically for a network capability to be reachable in the domain... I was more responding in regards to dynamic aspects rather than network specifically... anyhow
-
Andrew Warkentin -
Chubb, Peter (Data61, Eveleigh) -
Gernot Heiser -
Matt Rice -
Royce Mitchell III -
William ML Leslie