Hi all,
I'm working on a Masters research project looking into mapping an object-capability programming language onto seL4, in a way that includes some kind of mapping from the language object capabilities onto seL4's capabilities (or vice versa).
I'm at a stage of the project now where it would be really helpful to have some 'motivating examples' for transferring caps between threads/CSpaces. So I was hoping I could reach out to other seL4 developers to see if they had built any systems that made extensive use of moving capabilities around. Ideally, in an ocap language, these examples would be much easier to program than they currently would be in C...
The simplest example I can think of is a memory allocation server, but that wouldn't necessarily involve handing caps on beyond the one (requesting) process, which is the kind of thing I think more interesting examples would comprise of.
Cheers, Stewart Webb [Masters Research student at University of Melbourne]
On Mon, 16 May 2022 at 18:09, sjwebb@student.unimelb.edu.au wrote:
Hi all,
I'm working on a Masters research project looking into mapping an object-capability programming language onto seL4, in a way that includes some kind of mapping from the language object capabilities onto seL4's capabilities (or vice versa).
I'm at a stage of the project now where it would be really helpful to have some 'motivating examples' for transferring caps between threads/CSpaces. So I was hoping I could reach out to other seL4 developers to see if they had built any systems that made extensive use of moving capabilities around. Ideally, in an ocap language, these examples would be much easier to program than they currently would be in C...
The simplest example I can think of is a memory allocation server, but that wouldn't necessarily involve handing caps on beyond the one (requesting) process, which is the kind of thing I think more interesting examples would comprise of.
Fantastic to hear you will be digging into this! I think I remember you bringing this up in #MontE in the summer.
After running process construction, the next obvious example is opening files. You might have a program that wants the user to select a picture or document to open, and so it requests the user's file picker (powerbox) to make that request. If the user selects a file to give to the program, it hands a capability back to the requester.
I'm currently working in driver code, so my mind turns there - when you plug a new device into a system, the driver needs to initialise it and make it available to the user, at which point they might grant some program access to the device; or alternatively some program might have a capability to enumerate new devices of a certain type.
If you want more complex examples, building shells that can express capability concepts is one. You might want to provide a running process access to listen on a new tcp port, or grant it more of the CPU, or map another directory into its store. TBF there's already a wealth of prior art to build on there; from Ka-Ping Yee through Norm Hardy's writings on shells to Shill and to Genode's launcher. Any of these would benefit from being able to leverage an existing capability language.
I also think that you digging into this stuff will help explore one issue that we will have building large scale systems on existing capability architectures. Capability languages have for the most part been forward-thinking enough that capability invocation is an asynchronous activity. This appears to be a good thing from a liveness perspective because you can invoke other domains without being starved for CPU yourself. On the other hand, capability-based kernels have tended to only implement synchronous send and receive. This is fine if you can trust every subsystem you call, but it is a problem we will need to solve as we build bigger systems. I have begun to explore this in Coyotos, but so far I've had Bigger Fish to Fry. It will be really interesting to see what your research here turns up.
Thanks for the big reply Will. I have no idea what #MontE is so I don't think that was me 😅.
Files and Drivers (or a Driver Manager perhaps) are two examples I've started to curate. A photo picker for mobile phone apps is one motivation that strikes me as a good one - e.g. choosing a photo to post on a social media site shouldn't dictate that its app needs complete access to your filesystem! I'd come across SHILL but got a bit scared off by its sandbox environment and Racket basis. It's been the same for many Javascript-based languages and implementations - big language/runtime bases to have to first wrangle into working on a microkernel... The Genode launcher sounds like something I need to look into.
Your last point on sync v.s. async is indeed one of the core problems that's come up in the research so far. I've been looking a lot at the Pony language, which is capabilities-secure, and has a neat system of 'reference capabilities' for tracking usage rights on object *references*. It also aims at C-level performance which made it seem a good pick for systems development on seL4 (as opposed to say, Javascript...). However one of the primary mechanisms the rcap system is contingent on is the actor model the language is built around, and the fact that all actor interaction is done with asynchronous, non-blocking, send-only message passing (termed actor "behaviours"). Messages are just quickly popped onto queues (in the same address space, another potential seL4 problem) and get picked up to be run by the runtime scheduling later, and rest of the code after the message send point just continues on from there. So to do something dependent on an actor behaviour, introducing some kind of callback would become essential (the language also has no async/await). This leads to somewhat of an impedance mismatch because some kind of asynchronous message pump between ocap vats may be required to get it working on seL4 across protection domains, as capability *transfer* only works with a synchronous Send() call on an seL4 Endpoint capability. Asynchronous events between domains can be implemented with seL4 Notifications, but can't do the cap transfer. It's leading me to think that "the perfect ocap language" for seL4 might need ways to express both synchronous and asynchronous invocations. So I'm now trying to look around at other ocap language implementations to see if there's anything better I could try adapt, lest I have to arrive on the conclusion of writing a whole new language (which I don't really have time for...). If you happen to know of any ocap languages with synchronous stylings do let me know...
Cap'n Proto, whilst not strictly a langauge per se, has also recently struck me as something that might be worth looking at, as it seems that when I look at trying to map ocap contexts onto seL4 protection domains, the API contracts between domains become pretty important. CAmkES is probably another example of this. My experience with capabilities stems more from working with the Barrelfish microkernel in the Advanced OS course at ETH Zurich, and I know that an interface definition language (Flounder, loosely documented here https://barrelfish.org/publications/TN-011-IDC.pdf) was a core part of the Barrelfish project too. (I don't think we were allowed to use it though!)
-
sjwebb＠student.unimelb.edu.au -
William ML Leslie