Dear seL4 community,
A couple months ago we had a successful 3rd seL4 Summit. Despite having to revert to virtual format, it was a very good event, and I’m sure I’m not the only one who enjoyed it. Thanks for the great work to our friends at IAI, Siege Technologies and the Griffiss Institute for the organisation, and DARPA and AFRL for funding the Summit in particular, and seL4 in general for many years.
DARPA funding for the seL4 Summits is coming to an end, and, as you know, the seL4 Foundation has been created as the community-driven guardians of seL4. Among others, this means it is time to think about how future summits will look like. For example, much of the funding for seL4 has come from defence budgets, but the technology is equally important for critical civilian systems, and the Summit should reflect this. We would also like to see broadened community participation, maybe a flavour of FODSEM or LCA, while continuing to involve our corporate partners, who are key to financial support and widespread deployment.
So we are asking you, the seL4 developer community, what you would like to see at the next summit, in content and format. After this informal community consultation we expect to issue an EOI for organising the next Summit, anticipated timeframe is similar as in the past, Sep–Nov.
Please make/discuss suggestions via reply email within a month (and note that I’ll be off-lline for a fair chunk of this).
Gernot
PS: For those who have missed it, the Summit presentations are still available for about another month to those registered, see https://www.sel4-us.org/summit2020/
On 1/7/21 5:59 PM, Gernot Heiser wrote:
Dear seL4 community,
A couple months ago we had a successful 3rd seL4 Summit. Despite having to revert to virtual format, it was a very good event, and I’m sure I’m not the only one who enjoyed it. Thanks for the great work to our friends at IAI, Siege Technologies and the Griffiss Institute for the organisation, and DARPA and AFRL for funding the Summit in particular, and seL4 in general for many years.
DARPA funding for the seL4 Summits is coming to an end, and, as you know, the seL4 Foundation has been created as the community-driven guardians of seL4. Among others, this means it is time to think about how future summits will look like. For example, much of the funding for seL4 has come from defence budgets, but the technology is equally important for critical civilian systems, and the Summit should reflect this. We would also like to see broadened community participation, maybe a flavour of FODSEM or LCA, while continuing to involve our corporate partners, who are key to financial support and widespread deployment.
So we are asking you, the seL4 developer community, what you would like to see at the next summit, in content and format. After this informal community consultation we expect to issue an EOI for organising the next Summit, anticipated timeframe is similar as in the past, Sep–Nov.
Please make/discuss suggestions via reply email within a month (and note that I’ll be off-lline for a fair chunk of this).
Gernot
PS: For those who have missed it, the Summit presentations are still available for about another month to those registered, see https://www.sel4-us.org/summit2020/
I would like to see the use of seL4 in highly dynamic, non-embedded, security critical systems discussed. Would the Robigalia and/or UX/RT developers be interested?
Also, a permanent and publicly accessible video archive would be awesome.
Sincerely,
Demi
On 9 Jan 2021, at 08:02, Demi M. Obenour <demiobenour@gmail.com mailto:demiobenour@gmail.com> wrote:
I would like to see the use of seL4 in highly dynamic, non-embedded, security critical systems discussed. Would the Robigalia and/or UX/RT developers be interested?
My present question was more about format than specific topics (that would come later) but the suggestion is a good one. In fact, we’re working on the design of such a system and it’s definitely something that should be ready to talk about by the time of the next Summit. Could end up a whole session with talks about various designs.
Also, a permanent and publicly accessible video archive would be awesome.
Agreed.
Gernot
On 1/8/21, Demi M. Obenour demiobenour@gmail.com wrote:
I would like to see the use of seL4 in highly dynamic, non-embedded, security critical systems discussed. Would the Robigalia and/or UX/RT developers be interested?
I'd possibly be interested. Not sure about the Robigalia developers. Seems like they haven't been very active, and I may have passed them with UX/RT as far as what I actually have working. They seem to have abandoned all their old code and tried to start over last year but haven't gotten far since then from what i can tell. I'm not quite sure why they didn't just try to continue with what they had (UX/RT's kernel bindings and allocation subsystem are a mashup of those from feL4 and Robigalia with several major enhancements).
Currently I'm working on UX/RT alone. I'd be a little bit surprised if anyone else actually wanted to contribute at this point, since all I have at the moment is kernel bindings for Rust and an allocation subsystem that is almost working (heap allocation doesn't quite work but CSpace, UTSpace, and VSpace allocation all seem to work OK so far). At least now I've actually been working on it every day, but still not quite as much as I'd like. I am expecting to be done with the allocators and move on to the IPC transport layer pretty soon though.
On 1/9/21 4:34 AM, Andrew Warkentin wrote:
I'd possibly be interested. Not sure about the Robigalia developers. Seems like they haven't been very active, and I may have passed them with UX/RT as far as what I actually have working. They seem to have abandoned all their old code and tried to start over last year but haven't gotten far since then from what i can tell. I'm not quite sure why they didn't just try to continue with what they had (UX/RT's kernel bindings and allocation subsystem are a mashup of those from feL4 and Robigalia with several major enhancements).
Hello Andrew,
We Robigalia developers have indeed been thinking through a better approach to our rust seL4 library. The shortcomings of our previous approach became very apparent as seL4 evolved its build system and added awesome new features that we just weren't able to keep up with.
During this process we have discussed with the broader seL4 community some of the issues and concerns we have about building our own language bindings and ultimately dynamic systems on seL4:
- https://sel4.discourse.group/t/procedural-generation-of-the-sel4-api/24 - https://sel4.discourse.group/t/pre-rfc-specify-a-fixed-kernel-abi-for-each-a... - https://github.com/seL4/seL4/issues/114
Based on these discussions we have started prototyping a procedurally-generated native rust seL4 library built from a complete seL4 IDL specification.
Once we have built this out we intend to share our learnings and continue to advocate for changes to seL4 and/or upstream work that improves the experience for everyone building their own language bindings or dynamic systems on seL4.
We are active in our IRC channel at #robigalia on freenode and invite anyone interested to join us.
-
Andrew Warkentin -
Demi M. Obenour -
Gernot Heiser -
Jimmy Brush