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 <[email protected]> escribió: > 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] > _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
