Hi Timotej, The source code of Aurora probably exists somewhere and could be dug up, but I personally have never seen it, and it has not been used by this group in any systems after the author. That presentation presents a core problem of resource management in seL4, this three way problem can be summarized as * Retyping memory requires capability slots * Capability slots require retyping memory * Book keeping the first two requires retyping memory The presentation claims that the API of seL4 is difficult to program for. I would disagree with that and say that the seL4 object and security model is difficult to program for. Pushing all allocation to the user is not necessarily fundamental to achieving the security and isolation of seL4 (I shall leave it for others more knowledgeable to debate this), but it is fundamental to the three way allocation problem. No API can fix this. This resource management problem can be solved in many ways however, and Aurora chose to solve the most complex problem possible. However, it is not clear yet that any system needs the generality of solutions provided by Aurora. Which is why it was never used. The main assumption our present resource managers make is that you do not want to clean up all meta data resources. For example, if memory is allocated to store meta data, when that meta data is empty (due to freeing other resources) you could release those resources back to the allocator. Or, you could use the assumption that the only time you would want that memory back is once you have run out of other resources to allocate, but to run out of other resources you probably re-used this memory to book keep those allocations. This is the assumption the allocators in allocman (https://github.com/seL4/seL4_libs/tree/master/libsel4allocman) currently make. Although it supports plugging in other allocation strategies that could fully free their book keeping if someone were to write them. Despite that library having multiple different sub allocators inside it and various boiler plate and boot strapping code it is only around 3k LoC, with no constraint solvers or other algorithmically complex code. So even a general purpose allocator does not need to be large and complex if you are willing to solve a less general problem. In practice for our trusted systems the root task uses a very simple allocate only allocator with no book keeping that just is just loading components into partitions. From there, different components can have varyingly complex allocators (or no allocators if they are static components) depending on their requirements. Adrian On Sat 16-Dec-2017 5:12 PM, Timotej Tomandl wrote:

Hi,

while reading about seL4 I have found a presentation "The seL4 capability system" by Matthew P. Grosvenor (https://www.cl.cam.ac.uk/resea rch/security/ctsrd/cheri/workshops/pdfs/20160423-sel4-capabilities.pdf), sadly I was able to track down only the slides, not the talk itself. It mentions the "Aurora project", the constraint solver running in static memory + stack space, concerning itself with the capability allocation. There are these questions which popped into my mind:

1. Is the source code of the Aurora project available anywhere? Is there any more information than the presentation available? 2. Is the constraint solver still necessary with the current version of the API? 3. If it is still necessary, then

- what is the necessary strength of the constraint solver?

- is a design, in which either the root process or the microkernel itself has to include such a constraint solver in static memory + stack space necessary for a microkernel with the guarantees of seL4 or is it a side-effect of the design decisions?

Regards, Timotej Tomandl

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel