On 7/30/21, Sidhartha Agrawal <[email protected]> wrote: > Hello sel4-devs, > I am a first-year graduate student at the University of British Columbia at > their Systopia Lab <https://systopia.cs.ubc.ca/> working on operating > systems research. My advisor is Prof. Margo Seltzer > <https://www.seltzer.com/margo>. In a past life, I have worked as a > software engineer at Oracle and Arista Networks. My research is on General > Purpose Isolation Mechanism in the OS. We ask whether we really need to > have N different isolation mechanisms or whether instead, we could develop > a framework in which all these different mechanisms represent points on a > continuum. Here is a write-up <https://sid-agrawal.ca/#research-projects> > with > some more details. I am using seL4 as the microkernel base to build my > research idea. At this stage, I am not looking in to the formal > verification aspect of seL4, but that might change once I have a better > idea about the type of mechanism I want to build. I would also like to keep > the changes in the kernel to be minimum and try to demonstrate my ideas > using user space processes. > > I have tried out the tutorials on the seL4 website. Currently, I am > wading through the different helper libraries in seL4/seL4_libs > <https://github.com/seL4/seL4_libs>. As someone who is just starting with > seL4 ecosystem, I had a few high-level questions: > > - Are there are example OSes built with seL4, which would be a good > place to look at? Specifically, I am looking for components such as > basic > versions of a process-server, vm-server, pager, file-systems server. > - I came across refOS <https://github.com/seL4/refos>, but wasn't sure > if it is still being maintained. > - Another option was Genode > <https://genode.org/documentation/general-overview/index>. This > seemed to be maintained by another community and has many layers of > abstractions since it supports multiple kernel backends. >
I'm working on my own QNX-like OS based on seL4 <https://gitlab.com/uxrt/>, although I haven't gotten very far and am still trying to finish up the memory allocators. UX/RT will have its own kind of general purpose isolation mechanism based around file security. It will be the first OS that I'm aware of under which everything truly is a file (even things like process heaps/stacks and the connection to the VFS itself will be files). Each process will have a list of files it is allowed to access (entries will apply to either a particular file or to all files in a particular directory). Since everything will be a file, basically all security will be reduced to file permissions, unlike in OSes with non-file-based primitives. On top of the file permissions there will be a daemon that implements a flexible form of role-based access control with user-definable roles. There will also be mechanisms to securely grant access to files, avoiding confused deputy vulnerabilities but only requiring relatively minor modifications to existing Unix applications rather than porting to a completely new system. There's also the Robigalia project <https://gitlab.com/robigalia/>, although they currently aren't as far along as I am (they abandoned their previous allocators, which I ended up forking, and are still only working on kernel bindings). Unlike what I am trying to do with UX/RT (write an OS that is superior to mainstream OSes while still being natively compatible with existing applications), they are wanting to build something completely new (with only limited sandbox-based backwards compatibility) based on persistent processes and a capability-oriented architecture. Otherwise, I'm not aware of any open seL4-based OSes besides the ones you mentioned. There are a few companies selling seL4-based embedded OSes but they are proprietary AFAIK. _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
