Devel January 2021

devel@sel4.systems

19 participants
18 discussions

gic v2 vs gic v3
by Chris Koziarz 09 Jul '21

09 Jul '21

Hi all, I'm trying to port camkes-arm-vm to a different platform, that supports gic-v3 In the process, I hit a compilation error: Building C object kernel/CMakeFiles/kernel_all_pp_...rapper_temp_lib.dir/ kernel_all_pp_prune_wrapper_temp.c.obj FAILED: kernel/kernel_all_pp_prune_wrapper_temp.c In file included from /home/chris/camkes-tqma8xqp- vm/kernel/src/arch/arm/object/vcpu.c:15: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v2.h:23: error: "IRQ_MASK" redefined [-Werror] 23 #define IRQ_MASK MASK(10u) In file included from kernel/gen_headers/plat/platform_gen.h:23, from /home/chris/camkes-tqma8xqp-vm/kernel/include/plat/ default/plat/machine.h:8, from /home/chris/camkes-tqma8xqp- vm/kernel/include/machine.h:9, from /home/chris/camkes-tqma8xqp- vm/kernel/include/api/syscall.h:10, from /home/chris/camkes-tqma8xqp- vm/kernel/src/api/faults.c:10: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v3.h:30: note: this is the location of the previous definition 30 #define IRQ_MASK MASK(16u) which is an indicative that both gic_v3.h & gic_v2.h headers have been included, which is an error because said headers are not compatible: kernel/include/arch/arm/arch/machine/gic_v3.h:#define IRQ_MASK MASK(16u) kernel/include/arch/arm/arch/machine/gic_v2.h:#define IRQ_MASK MASK(10u) So my question is: how can I configure the build to avoid such a conflict? I can grepp the relevant configuration option in CMakeCache.txt: build_tqma8/CMakeCache.txt:CONFIGURE_INTERRUPT_CONTROLLER:INTERNAL=arch/machine/gic_v3.h but cannot see it in ccmake gui because it's "INTERNAL" What is the solution? - replace this option somehow to use gic_v2 and have my HW use gic v.2, or - change compilation options to use gic_v3 everywhere Thanks for any help, Chris.

4 5

hello_rumprun app not worked
by MOHAMAD REZA SHAFIEI 13 Jun '21

13 Jun '21

hi. i'm recently worked on sel4 with camkes framework. when i compile rumprun_hello on x86_64 platform its compiled and build correctly but when run with qemu by ./simulate script, program crashed with this errors: simple_get_extended_bootinfo_length@simple.h:600 simple_get_extended_bootinfo_length not implemented FAULT HANDLER: data fault from hello.hello_0_control (ID 0x1) on address 0x8, pc = 0x402b7f, fsr = 0x6 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x402b7f , . . so i found that this method not implemented yet so i return 0 in this method and resolved. for second problem that cause failure if trace program and i found that in "init rumprun" process the program failed in the /projects/sel4runtime/include/sel4_arch/x86_64/sel4runtime/thread_arch.h file and sel4runtime_set_tls_base method. so i read git log and in recently commit your team use sel4runtime for thread TLS, so when we run rumprun_hello, the program failed in sel4runtime_set_tls_base method. can you help me fix this bug? thanks for your attention. -- This email was Anti Virus checked by Security Gateway.

4 4

Reducing memory footprint - RISC-V
by porter.188＠osu.edu 19 Apr '21

19 Apr '21

I'm trying to build a low memory footprint of RISC-V based seL4. I'm using QEMU/spike for now. In seL4 12.0 I can modify spike.dts to 8.5 MB of memory 0x00880000. 42 memory@80000000 { 43 device_type = "memory"; 44 reg = <0x00000000 0x80000000 0x00000000 0x00880000>; 45 }; This is the smallest value that builds, lower than this I get the error: [0/1] Re-running CMake... -- Found GCC with prefix riscv64-unknown-linux-gnu- STATUS,KernelDTSList: tools/dts/spike.dts -- /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... STATUS,platform_yaml: /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml -- Detecting cached version of: musllibc -- Found valid cache entry for musllibc -- Configuring done -- Generating done -- Build files have been written to: /mnt/data/femur_12.0/build [18/36] Generating gen_headers/image_start_addr.h FAILED: elfloader-tool/gen_headers/image_start_addr.h cd /mnt/data/femur_12.0/build/elfloader-tool && sh -c "/mnt/data/femur_12.0/tools/elfloader-tool/../cmake-tool/helpers/shoehorn.py /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml /mnt/data/femur_12.0/build/elfloader-tool/archive.o > /mnt/data/femur_12.0/build/elfloader-tool/gen_headers//image_start_addr.h" shoehorn: fatal error: ELF-loader image "/mnt/data/femur_12.0/build/elfloader-tool/archive.o" of size 0x107548 does not fit within any memory region described in "{'devices': [{'end': 2147483648, 'start': 0}, {'end': 549755809792, 'start': 2155872256}], 'memory': [{'end': 2155872256, 'start': 2149580800}]}" ninja: build stopped: subcommand failed. What do I need to modify to get to < 2 MB? Thanks!

4 8

Ethernet device module for odroidc2
by ogosinkem＠gmail.com 24 Feb '21

24 Feb '21

I have been trying to use the ethernet driver for the UNSW Asdvanced Operating Systems course but I still get these messages: find_compatible_driver_module@io.c:434 No suitable driver was found for path /soc/ethernet@c9410000, ignoring server_init@ethdriver.c:382 Unable to find an ethernet device I thought that I had to copy the driver to the utils lib folder and provide a preprocessor macro as someone else had suggested but I may be missing a few other things. Best, Nkem

3 6

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

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 29 Jan '21

29 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

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel January 2021