January 2021 - Devel - lists.sel4.systems

Request for Speakers/Collaboration with WASI
by Zach Lym 29 Jan '21

29 Jan '21

I'm a community organizer for WASI <https://wasi.dev/>, a post-POSIX runtime with features that I think make it suitable for SeL4's planned post-POSIX runtime: * Fast and fine grained SFI via WASM. * Fast IPC and capability oriented security via WASM Reference Types <https://github.com/WebAssembly/reference-types/blob/master/proposals/refere…> . * High level interoperability across programming languages via WASI Interface Types <https://hacks.mozilla.org/2019/08/webassembly-interface-types/> and shared garbage collection <https://github.com/WebAssembly/gc/blob/master/proposals/gc/Overview.md>. * Wide range of targets: embedded, TEE, blockchain, browser, server, and (eventually) consumer operating systems. Industry cooperation is happening through the Bytecode Alliance <https://bytecodealliance.org/>, with partners like Red Hat ensuring commercial viability [1 <https://github.com/bytecodealliance/wasmtime/issues/70#issuecomment-4773292…> , 2 <https://github.com/bytecodealliance/wasmtime/issues/71#issuecomment-5180066…>]. Fastly is already using it for their serverless offering <https://www.youtube.com/watch?v=QdWaQOgvd-g>, which can scale to 20K processes/machine with a 35.4 microsecond cold start time. However, I believe the project would benefit *greatly* from the SeL4 community's experience architecting high-performance/high-assurance microkernels, IPC, and capability based security models. SOIL <https://soil-initiative.org/> is an academic effort to foster cross-pollination through biweekly seminars <https://soil-initiative.org/seminar/>. *We are seeking presenters from the SeL4 to better understand your needs and potential areas of collaboration*. Please contact Ross Tate (ross(a)cs.cornell.edu) if you are interested in presenting and jump on our Zulip Channel <https://bytecodealliance.zulipchat.com/> if you have any questions! Thank you, -Zach Lym

1 0

Accessing GPIOs on Raspberry Pi
by Zohra Charania 29 Jan '21

29 Jan '21

Hello All, I am new to seL4. I want to use seL4 in my project. As a starting point, I have compiled seL4 for Raspberry pi 3. As a next step, I have been trying to access GPIOs on Raspberry Pi. I used gpio.h from util_libs/libplatsupport/arch_include/arm/platsupport. I could not find any gpio.c for Rpi3/bcm2837 platform. When I compile the code, I am getting error: undefined reference to `gpio_sys_init'. Is there any support for GPIO access already available for Raspberry Pi? Could you please provide me guidance on how I can work with the Raspberry Pi GPIOs with seL4. Best Regards Zohra

1 0

Re: Cross VM Connectors
by PityTheFool 28 Jan '21

28 Jan '21

I discovered the answer by looking at the optiplex9020 example. Because the tutorial used the old modules, I had not fully integrated the new connector module into my project.

1 0

Re: Ethernet device module for odroidc2
by Todd Carpenter 28 Jan '21

28 Jan '21

I've been following this exchange with some interest, since I also could use an odroidc2 ethernet driver supported by camkes. > From: "Lee, Damon (Data61, Eveleigh)" > The issue is more clear now, the issue lies with the fact that the Ethernet > driver structure layout is different from the expected layout in libethdrivers. Yes, very much so. I had looked at this awhile ago, and the differences seemed daunting. > If aren't in a rush to solve these issues, the team is considering porting over > the AOS Ethernet driver for the C2 over to libethdrivers in the next few days. > Though this would take a few days to do, review, and have it pushed out to > upstream. I would really appreciate a this. Two thumbs up!

1 0

RFC discussion before vote
by Gerwin Klein 27 Jan '21

27 Jan '21

If you have an opinion on any of these RFCs before we vote on them on Fri, please comment on the Jira issue: - Ability to build additional bootloaders inside the seL4 build system https://sel4.atlassian.net/browse/RFC-4 - The seL4 Core Platform https://sel4.atlassian.net/browse/RFC-5 - The seL4 Core https://sel4.atlassian.net/browse/RFC-6 Cheers, Gerwin

1 0

Cross VM Connectors
by ndaughety13＠gmail.com 26 Jan '21

26 Jan '21

**Problem:** In my unsuccessful attempt to complete the cross vm connectors tutorial, [1](https://docs.sel4.systems/Tutorials/camkes-vm-crossvm.html), I discovered [2](https://github.com/seL4/sel4-tutorials/issues/49). I am now trying to use [3](https://github.com/seL4/camkes-vm-examples/tree/master/apps) with the new connection module which I thought would expose the dataport device to the VM but the corresponding device does not exist in */dev*. I have confirmed that the module is loaded with *lsmod* in the guest. The original tutorial uses an executable *dataport_init*, which is called from the *camkes_init* script. I assume that this executable would provide the setup for the dataport, however the executable *dataport_init* is not in the *default_buildroot_rootfs.cpio* (note: *consumes_event_init* and *emits_event_init* do exist in the rootfs archive) or as a project anywhere in the project files to be overlayed. Because I could not find this executable in the arm example, I assumed that the connection module aided in the dataport initialization process. **Questions:** 1. Where and how is the dataport device (*/dev/uio0* in this case) exposed/initialized so that read/write can occur? 2. Is there an up-to-date version of the Cross VM Connectors tutorial for x86? I have limited knowledge on this and I may not even be asking the right questions -- therefore any feed back and responses are welcome, thanks. **References:** [1]: https://docs.sel4.systems/Tutorials/camkes-vm-crossvm.html [2]: https://github.com/seL4/sel4-tutorials/issues/49 [3]: https://github.com/seL4/camkes-vm-examples/tree/master/apps

1 0

Cross VM Connectors
by Nathan Daughety 25 Jan '21

25 Jan '21

To whom it may concern, I am looking at https://github.com/seL4/camkes-vm-examples repo, specifically, vm_cross_connectors. Side note, I am just learning CAmkES and seL4 so my knowledge is limited. Looking at the connection kernel module, it looks like it should be initializing the dataport device in /dev but when I run the example, it does not appear that the device has been exposed (no uio0 in /dev) which is what I thought the module did. I confirmed with lsmod that the connection module (connection.ko) is loaded. What do I need to do to expose /dev/uio0 (or any device name that refers to the dataport)? I am looking at seL4HardwareMMIO but I noticed that the example does not use it. If you could point me in the right direction I would really appreciate it. Thanks, Nathan

1 0

Ethernet device module for odroidc2
by ogosinkem＠gmail.com 22 Jan '21

22 Jan '21

Im having trouble with creating a ethernet driver device module for odroid c2. I have tried to create one based on the examples that exists in "/util_libs/libethdrivers/src/plat" to no avail. Looking at it, it does not seem to call the function to intialise the module. This is also evident when I step through the "find_compatible_driver_module" function in the "/camkes-tool/libsel4camkes/src/io.c" file as it does not go in to the loop that, from my understanding, should cycle through a list of modules in order to select an appropriate one. Any suggestions to what I may be missing or any references that would help point me in the right direction will be much appreciated.

3 2

Re: Rust bindings, was: Re: What do you want from the next seL4 Summit?
by Andrew Warkentin 13 Jan '21

13 Jan '21

On 1/12/21, Jimmy Brush <code(a)jimmah.com> wrote: > > 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. > Is there any particular reason why you didn't just port your bindings to feL4? It does use the C bindings underneath (through bindgen), but I don't think that's a big problem, as they don't have much room for memory bugs (and UX/RT is not meant to be a "Rust OS" like Redox and Robigalia; it will just be an OS that has a lot of subsystems written in Rust, but there will still be a lot of third-party C code). It was relatively easy for me to port your old bindings and allocators to my fork of feL4. Here is the UX/RT subproject with the bindings and allocators (rust-bitmap, rust-sel4, and sel4-alloc are forked from Robigalia; the rest is from feL4 except for sel4-slabmalloc): https://gitlab.com/uxrt/core-supervisor/fel4/

1 0

What do you want from the next seL4 Summit?
by Gernot Heiser 12 Jan '21

12 Jan '21

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/

4 4