[seL4] Re: Operating Systems built on top of seL4

Hi Andrew, your project looked interesting to me too so I decided to give it a look and I coud read here: https://gitlab.com/uxrt/core-supervisor/sel4-kernel "The seL4 microkernel with patches for UX/RT" But my question is: by modifying the seL4 kernel, don't you loose the security of the formal verification? I mean, the nice thing of a formally verified code is you can forget about it's security. Don't you fear you can introduce vulnerabilities? Cheers, El sáb., 31 jul. 2021 3:53, Andrew Warkentin escribió:

On 7/30/21, Sidhartha Agrawal 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 -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems