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 am looking forward to engaging with this community, learning about seL4 and making meaningful contributions.
Best, Sid sid-agrawal.ca