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, …
[View More]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
[View Less]
Hello,
I would like to bring this issue to the attention of the community. Sel4’s
fork of the rumprun unikernel no longer compiles. Due to the usage of
Werror flag, the compiler produces repeated warnings which in turn creates
errors. It seems like the rump kernel was tested on an older version of gcc
and because it is older, raises warnings and causes the build to fail on
newer compilers. This is a similar issue to
https://github.com/rumpkernel/rumprun/issues/82
I have tested rumprun in the …
[View More]sel4 docker container. My build logs are also
attached to this email. Thank you for taking attention to this issue.
Sincerely,
Ellis
[View Less]