OS caps x ocap languages masters thesis complete

[Stewart Webb]

Hi all,

Some of you here may be interested in the Masters thesis I finally completed last year, looking into trying to map ocap languages onto the seL4 microkernel and its cap system. I have just finished self-publishing the thesis on my website (as my uni doesn't publish masters theses themselves...) so you can take a look at the abstract and full PDF here: https://swebb.id.au/research. There's also a slide deck from a few presentations I gave on the thesis.

Probably the most interesting outcome of the research was my discovery that Pony (and most other ocap languages?) arguably have an ambient authority case when it comes to memory allocation. This was basically teased out by seL4 because of its very strict cap authority system/hierarchy that describes all memory on the running system, which is a core part of how it delivers its iron-clad security guarantees. On seL4, if you want more physical memory in your protection domain, you have to be handed it explicitly, via cap transfer (through an explicit IPC capability) from something else.

There is a reasonably good contrasting example of this I found just after the thesis in the form of the Zig programming language. While it is not an ocap language, the use of allocators is made explicit, by convention at least - any function that allocates beyond its stack will declare an allocator argument as its first argument (slide 34 of my slide deck has an example of this).

Conclusion-wise, unfortunately nothing really ended up working out in a nice way from what is currently available from ready-to-use ocap languages, dependency/development issues in running them on seL4, and some quirks in the seL4 cap system from an async perspective (which most ocap languages seem to be oriented around). This was additionally compounded by the relatively short Masters project timeframe I had to look at it all. However I was at least able to somewhat map out the various "dimensions" of capability stuff on the language and OS sides within the thesis, to try and better reason about how they could be made to potentially line up usefully.

In Gernot Heiser ("Mr seL4", at UNSW Trustworthy Systems)'s words after the project: "It looks like a PhD..."

You may also find interesting the "capability timeline" diagram I made as part of all the research (available on the same webpage linked above). It shows a map of various papers and theses on OS capabilities throughout the years, which I put together to try and get my head around it all and also work out where seL4's cap system came from specifically.

Cheers,

Stewart Webb
(Melbourne, Australia)

P.S. if Jon Shapiro is on this list... your PhD thesis appears to have not (yet?) made it through a reshuffle/rebuild of the UPenn repository system - my link that worked last year (https://repository.upenn.edu/dissertations/AAI9926195) now goes to a 404, and searches of the new system didn't seem to turn up anything...