Hi,

while reading about seL4 I have found a presentation "The seL4 capability system" by Matthew P. Grosvenor (https://www.cl.cam.ac.uk/research/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,