- Devel - lists.sel4.systems

Public TSC meeting on Fri, 29 Jan
by Gerwin Klein 08 Feb '21

08 Feb '21

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: Fri 29 Jan 2021 15:30-17:00 Sydney time (5:30am in Berlin, 8:30pm in San Francisco). The meeting is by Zoom, and you can register here: https://unsw.zoom.us/meeting/register/tZ0ocO6hrDwiGtTYlzULbKeTK8ybYJyCC7_p Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. Sorry about the very early time for Europe, but there are no time slots that work for the US, Australia, and Europe at the same time. We are planning to swap between better times for Europe and the US for the next meetings. The TSC is the body that decides on the technical direction of seL4: https://sel4.systems/Foundation/TSC/ The agenda for the meeting so far is: - updates from the TSC chair and committees: - seL4 public Jira - Jira + GitHub sync - reviewers who have joined - more GitHub tests - discussion points: - do we have too many different forums? - bug/issue classification (Jira is now public, we shouldn't call everything a bug) - more in-tree docs - test infrastructure - extend RFC process slightly? (see https://sel4.atlassian.net/browse/RFC-6?focusedCommentId=14886& ) - when/how should Committer/Admin role change for people who have left D61 and had the role based on org membership - endorsement process for training and products - vote on: - Platform Owner proposal - discuss, potentially vote on RFC proposals: - https://sel4.atlassian.net/browse/RFC-4 - https://sel4.atlassian.net/browse/RFC-5 - https://sel4.atlassian.net/browse/RFC-6 This is probably already too much for 90min and we may have to prioritise, but we will see how far we get. If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

2 5

Errors while running Virtual Machines on SeL4;
by Jorge Pereira 07 Feb '21

07 Feb '21

Hi all, I’m getting familiar with SeL4 build system and I’ve been running several application examples and also creating my own on top of the kernel using CAmKES. Very good. $ mkdir camkes-project; $ cd camkes-project; $ repo init -u https://github.com/seL4/camkes-manifest.git; $ repo sync; $ ../init-build.sh -DPLATFORM=sabre -DAARCH32=1 -DCAMKES_APP=helloworld -DSIMULATION=1 $ ninja $ ./simulate Again, so far, so good! Several CAmKES examples up and running. Now, I want to run virtual machines on top of it, I’ve seen several posts on internet and even in the official SeL4 website and none of them are working on my side. Can you please give me some pointers to be able to do so? We really want to start using SeL4 in our products with virtual machines, but current documentation is not ideal. I don’t have experience in CMAKE and that might be the real problem 😊. I need your help to ramp up in the SeL4 project! https://docs.sel4.systems/projects/camkes-arm-vm/ repo init -u https://github.com/seL4/camkes-vm-examples-manifest repo sync mkdir build cd build ../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tk1 When running ../init-build.sh I get the following: “ CMake Error at /home/jorge/hdd/work/projects/vm/Findcamkes-arm-vm.cmake:39 (find_package): By not providing "Findcamkes-vm-images.cmake" in CMAKE_MODULE_PATH this project has asked CMake to find a package configuration file provided by "camkes-vm-images", but CMake did not find one. Could not find a package configuration file provided by "camkes-vm-images" with any of the following names: camkes-vm-imagesConfig.cmake camkes-vm-images-config.cmake Add the installation prefix of "camkes-vm-images" to CMAKE_PREFIX_PATH or set "camkes-vm-images_DIR" to a directory containing one of the above files. If "camkes-vm-images" provides a separate development package or SDK, be sure it has been installed. Call Stack (most recent call first): CMakeLists.txt:19 (camkes_arm_vm_setup_arm_vm_environment) -- Configuring incomplete, errors occurred! See also "/home/jorge/hdd/work/build/CMakeFiles/CMakeOutput.log". “ Best, Jorge

1 0

seek for some help
by abdi mahmud haji 01 Feb '21

01 Feb '21

hi sorry for bothering you but i get some problem with sel4 tutorial when i trying to get starting with "repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest" i got down bellow error and how can i fix it pls Traceback (most recent call last): File "/home/sel4/sel4-tutorials-manifest/.repo/repo/main.py", line 56, in <module> from subcmds.version import Version File "/home/sel4/sel4-tutorials-manifest/.repo/repo/subcmds/__init__.py", line s 38, in <module> ['%s' % name]) File "/home/sel4/sel4-tutorials-manifest/.repo/repo/subcmds/upload.py", line 27, in <module> from hooks import RepoHook File "/home/sel4/sel4-tutorials-manifest/.repo/repo/hooks.py", line 472 file=sys.stderr) ^ SyntaxError: invalid syntax tnks

3 2

Fwd: Regarding Ken Thompson's Reflecting on trusting trust...
by Bora Agca 30 Jan '21

30 Jan '21

Hi, i have one question: since the seL4 was written with a C compiler and it is possible that this compiler has an in-built backdoor, how can you still claim, that seL4 is "safe", i.e. non-hackable. Best regards and thanks in advance ___________________________ Bora Agca Diplom Informatiker Oracle Certified Programmer Java SE 6

2 1

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