September 2020 - Devel - lists.sel4.systems

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

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

Userland components in Ring 1/2 (where kernel is in ring 0) to provide protection from less trusted components
by Isaac Beckett 19 Sep '20

19 Sep '20

Hey all, I was wondering if it makes sense for someone building a system on seL4 to run certain drivers or other critical components in a more privileged environment, but still outside the kernel. Does using a different CPU mode in this context make sense? My hunch is that the case is no, because x86 has those extra rings, but ARM only has two modes, Supervisor/System and User mode, which would make it hard to provide any mechanism for the kernel to manage privileged components, because of the differences between platforms.

6 6

capability name change
by Sachin More 17 Sep '20

17 Sep '20

Hi: Between version 9.0.1 and 10.0.0, the capability name seL4_CapIOPort changed to seL4_CapIOPortControl in the file seL4/libsel4/include/sel4/bootinfo_types.h. I have some legacy code written for 9.0.1 that I want to port to 10.0.0. When I changed the occurrences of seL4_CapIOPort to seL4_CapIOPortControl, I am getting the following: Warning: copy: seL4_CNode_Copy (0x7) returned 3 followed some time later by: Warn<<seL4(CPU 0) [decodeInvocation/530 T0xffffff80002de400 "child of: 'child of: 'rootserver''" @20f27a4]: Attempted to invoke a null cap #7.>> What am I doing wrong? thanks in advance, Sachin

2 2

Re: [seL4] Devel Digest, Vol 76, Issue 8
by Chris Koziarz 16 Sep '20

16 Sep '20

Thanks Damon for your help. I've reinstalled Haskell stack this morning> This time I tried fault-handlers tutorial. It appears the reinstall had made the difference as ninja indeed spawned the process: $ stack build --fast and after just a minute or two (yesterday the whole thing was hanging for a good 20-30min before I lost patience), a long log was produced. Among tons of messages, I found this warning: Copied executables to /home/chris/sel4_tutorials/fault-handlers_build/capDL-tool: - parse-capDL Warning: Installation path /home/chris/sel4_tutorials/fault-handlers_build/capDL-tool not found on the PATH environment variable. I hope the warning won't stop me, although I'm curious why capDL wants to live in (and have a path to) a tutorial build directory rather than some common bin dirs like /usr/bin:/snap/bin or such... Thanks again, Chris On Tue, Sep 15, 2020 at 10:53 PM <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Re: CAmkES Linux VM Tutorial/Minimal Build Issue > (Lee, Damon (Data61, Kensington NSW)) > 2. Re: ADL tool hangs (Lee, Damon (Data61, Kensington NSW)) > 3. capability name change (Sachin More) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Tue, 15 Sep 2020 02:16:43 +0000 > From: "Lee, Damon (Data61, Kensington NSW)" > <Damon.Lee(a)data61.csiro.au> > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] CAmkES Linux VM Tutorial/Minimal Build Issue > Message-ID: <tfbr1r3vl6e.fsf(a)coopers.keg.data61.csiro.au> > Content-Type: text/plain; charset="iso-8859-1" > > Hi Jim, > > > So there I was having a lovely time doing the seL4 > > Tutorials...and I got > > hit with debug output #1 below, so I confirmed that I indeed had > > nested > > virtualization working by making an running an Ubuntu VM in side > > of an > > Ubuntu VM on an Ubuntu box in using kvm and qemu, so I do not > > think it is > > that. I tried passing the host processor through just to see if > > there > > something was getting in the way to no avail. > > I took a look at the debug output and it looks like there's > something funny > going on with the kernel and the VMM. I was able to replicate your > issue using > the manifest available on GitHub, but it was working fine using > our internal > manifests. So I suspect there were probably fixes that haven't > been propagated > to GitHub yet via our internal CI processes. > > I'll take a look at why our CI haven't propagated changes to > GitHub and in the > meantime, I've created a fork[1] on GitHub of our internal > tutorial manifest so > you can use that instead. > > [1] https://github.com/nomadeel/sel4-tutorials-manifest > > Hope this helps, > Damon > > > ------------------------------ > > Message: 2 > Date: Tue, 15 Sep 2020 02:25:57 +0000 > From: "Lee, Damon (Data61, Kensington NSW)" > <Damon.Lee(a)data61.csiro.au> > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] ADL tool hangs > Message-ID: <tfbo8m7vkr0.fsf(a)coopers.keg.data61.csiro.au> > Content-Type: text/plain; charset="iso-8859-1" > > Hi Chris, > > > I have recently messed up my ubuntu host seL4 building machine > > and I had to > > recreate it from scratch. But I have missed something on the > > way. So I have > > a problem building anything that involves Camkes components. It > > appears > > that a tool generating ADL or linking capDL or something along > > is missing > > and results in a hang during building. For example when building > > ipc > > tutorial (for x85 platform): > > > > root@ubuntu:/home/chris/sel4_tutorials/ipc_build# ninja > > [0/8] Generating capDL-tool/parse-capDL^C > > ninja: build stopped: interrupted by user. > > > > Or mcs tutorial: > > > > root@ubuntu:/home/chris/sel4_tutorials/mcs_build# ninja > > [0/8] Generating capDL-tool/parse-capDL^C > > ninja: build stopped: interrupted by user. > > This build step builds the capDL-tools which is written in > Haskell. 'stack' is > the toolchain used to build the capDL-tools and we've seen > examples of it taking > a *very* long time on specific distributions like Ubuntu. To > verify this, > perhaps try `ps aux | grep stack` or similar to see if 'stack' is > being run. > > We do cache the build after the first time it's being run, so > subsequent builds > shouldn't take too long. If this build step doesn't finish even > after waiting > for a long time (30 minutes or so), let us know and we'll be happy > to help. > > Regards, > Damon > > > ------------------------------ > > Message: 3 > Date: Tue, 15 Sep 2020 08:51:15 -0400 > From: Sachin More <sachinsureshmore(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] capability name change > Message-ID: > <CAH36oswCDPRDFeNbgFPVnKvgapFyo= > BbsiNRuf+FjqrBaquegg(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > Hi: > > Between version 9.0.1 and 10.0.0, the capability name seL4_CapIOPort > changed to seL4_CapIOPortControl in the file > seL4/libsel4/include/sel4/bootinfo_types.h. > I have some legacy code written for 9.0.1 that I want to port to 10.0.0. > When I changed the occurrences of seL4_CapIOPort to seL4_CapIOPortControl, > I am getting the following: > > Warning: copy: seL4_CNode_Copy (0x7) returned 3 > > followed some time later by: > > Warn<<seL4(CPU 0) [decodeInvocation/530 T0xffffff80002de400 "child of: > 'child of: 'rootserver''" @20f27a4]: Attempted to invoke a null cap #7.>> > > What am I doing wrong? > > thanks in advance, > Sachin > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 76, Issue 8 > ************************************ >

2 1

Subject=Re: CAmkES Linux VM Tutorial/Minimal Build Issue
by Jim McColl 16 Sep '20

16 Sep '20

Damon, Too easy, worked on the first go! Thank you for the help! -Jim Evidence: Welcome to Buildroot buildroot login: [ 2.627354] random: fast init done Welcome to Buildroot buildroot login: root Password: # ls -ali total 4 108 drwx------ 2 root root 0 Sep 15 15:20 . 1 drwxrwxr-x 17 root root 0 Jan 8 2020 .. 1114 -rw------- 1 root root 11 Sep 15 15:20 .ash_history #

1 0

ADL tool hangs
by Chris Koziarz 15 Sep '20

15 Sep '20

Hi all, I have recently messed up my ubuntu host seL4 building machine and I had to recreate it from scratch. But I have missed something on the way. So I have a problem building anything that involves Camkes components. It appears that a tool generating ADL or linking capDL or something along is missing and results in a hang during building. For example when building ipc tutorial (for x85 platform): root@ubuntu:/home/chris/sel4_tutorials/ipc_build# ninja [0/8] Generating capDL-tool/parse-capDL^C ninja: build stopped: interrupted by user. Or mcs tutorial: root@ubuntu:/home/chris/sel4_tutorials/mcs_build# ninja [0/8] Generating capDL-tool/parse-capDL^C ninja: build stopped: interrupted by user. Looking into build.ninja script, I think the problem command be this one: build capDL-tool/parse-capDL: CUSTOM_COMMAND COMMAND = cd /home/chris/sel4_tutorials/mcs_build/capDL-tool && printf capDL-tool/parse-capDL:\ > /home/chris/sel4_tutorials/mcs_build/capDL-tool/parse-capDL.d && find -L /home/chris/sel4_tutorials/projects/capdl/capDL-tool/ -type f -printf %p\ >> /home/chris/sel4_tutorials/mcs_build/capDL-tool/parse-capDL.d && cp -a /home/chris/sel4_tutorials/projects/capdl/capDL-tool/* . && /usr/bin/cmake -E env make DESC = Generating capDL-tool/parse-capDL depfile = /home/chris/sel4_tutorials/mcs_build/capDL-tool/parse-capDL.d restat = 1 but I don't know why it would be hanging my build and how I should fix it. Any help greatly appreciated. Chris.

2 1

CAmkES Linux VM Tutorial/Minimal Build Issue
by Jim McColl 15 Sep '20

15 Sep '20

So there I was having a lovely time doing the seL4 Tutorials...and I got hit with debug output #1 below, so I confirmed that I indeed had nested virtualization working by making an running an Ubuntu VM in side of an Ubuntu VM on an Ubuntu box in using kvm and qemu, so I do not think it is that. I tried passing the host processor through just to see if there something was getting in the way to no avail. That was when I decided to go through the devel archives and the closest similar post I could find was 07 Aug 2020 ( https://sel4.systems/pipermail/devel/2020-August/002845.html) unfortunately there's no debug output so I cannot confirm is it is the same issue. There was also an issue in April ( https://sel4.systems/pipermail/devel/2020-April/002781.html) that also looked similar but I grep'd through the source and could not find the line referenced line from the commit. Finally I natively built minimal from https://github.com/seL4/camkes-vm-examples in the hopes that it was an issue with the tutorial docker container which led to output #2 below. Which brings me to now humbly request for help so I can finish up the tutorials. Thank you advance for any help anyone can provide, hopefully it is a simple mistake on my part. -Jim ====== VERY LONG DEBUG STUFF BELOW ====== - Debug Output #1: ./simulate: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xa1d000 end=0x1e366e0 size=0x14196e0 name='images/capdl-loader-image-x86_64-pc99' Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 7fedf000 type 1 Adding physical memory region 0x100000-0x7ffdf000 Physical Memory Region from 7ffdf000 size 21000 type 2 Physical Memory Region from b0000000 size 10000000 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from feffc000 size 4000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Multiboot gave us no video information ACPI: RSDP paddr=0xf68d0 ACPI: RSDP vaddr=0xf68d0 ACPI: RSDT paddr=0x7ffe210d ACPI: RSDT vaddr=0x7ffe210d Kernel loaded to: start=0x100000 end=0xa1c000 size=0x91c000 entry=0x10125e ACPI: RSDT paddr=0x7ffe210d ACPI: RSDT vaddr=0x7ffe210d ACPI: FADT paddr=0x7ffe1ee5 ACPI: FADT vaddr=0x7ffe1ee5 ACPI: FADT flags=0x84a5 ACPI: DMAR paddr=0x7ffe20c5 ACPI: DMAR vaddr=0x7ffe20c5 ACPI: IOMMU host address width: 39 ACPI: 1 IOMMUs detected ACPI: MADT paddr=0x7ffe1fd9 ACPI: MADT vaddr=0x7ffe1fd9 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: size=0x289a000 v_entry=0x4083af v_start=0x400000 v_end=0x2c9a000 p_start=0x1e37000 p_end=0x46d1000 Moving loaded userland images to final location: from=0x1e37000 to=0xa1c000 size=0x289a000 Starting node #0 with APIC ID 0 Mapping kernel window is done vt-x: Load IA32_PERF_GLOBAL_CONTROL not supported. Hardware debugging may not work IOMMU 0x0: 16-bit domain IDs supported IOMMU: Using 3 page-table levels (max. supported:3) IOMMU: Create VTD context table for PCI bus 0x0 (pptr=0xffffff807e01d000) ===== SNIP ====== IOMMU: Create VTD context table for PCI bus 0xfe (pptr=0xffffff807e11b000) IOMMU: Create VTD context table for PCI bus 0xff (pptr=0xffffff807e11c000) IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space Single bus detected lib_pci_scan_dev found pci device 0 0 PCI :: 00.00.00 : intel Unknown device ID. (vid 0x8086 did 0x29c0) line0 pin0 lib_pci_scan_dev found pci device 0 1 PCI :: 00.01.00 : Unknown vendor ID. Unknown device ID. (vid 0x1234 did 0x1111) line0 pin0 BAR0 : [ mem 0xfd000000 sz 0x1000000 szmask 0xff000000 prefetch ] BAR2 : [ mem 0xfebb0000 sz 0x1000 szmask 0xfffff000 ] lib_pci_scan_dev found pci device 0 2 PCI :: 00.02.00 : intel Unknown device ID. (vid 0x8086 did 0x100e) line11 pin1 BAR0 : [ mem 0xfeb80000 sz 0x20000 szmask 0xfffe0000 ] BAR1 : [ io 0xc000 sz 0x40 szmask 0xffffffc0 ] lib_pci_scan_dev found pci device 0 31 PCI :: 00.1f.00 : intel intel_ich9_8 (vid 0x8086 did 0x2918) line0 pin0 lib_pci_scan_dev found multi function device 0 31 PCI :: 00.1f.02 : intel Unknown device ID. (vid 0x8086 did 0x2922) line10 pin1 BAR4 : [ io 0xc080 sz 0x20 szmask 0xffffffe0 ] BAR5 : [ mem 0xfebb1000 sz 0x1000 szmask 0xfffff000 ] PCI :: 00.1f.03 : intel intel_ich9_6 (vid 0x8086 did 0x2930) line10 pin1 BAR4 : [ io 0x700 sz 0x40 szmask 0xffffffc0 ] ========== KERNEL EXCEPTION ========== Vector: 0xd ErrCode: 0x0 IP: 0xffffffff8080d2e9 SP: 0xffffffff80a0bd88 FLAGS: 0x10002 CR0: 0x8001003b CR2: 0x0 (page-fault address) CR3: 0xa17000 (page-directory physical address) CR4: 0x2220 Stack Dump: *0xffffffff80a0bd88 == 0xffffff807c052880 *0xffffffff80a0bd90 == 0xffffff80318c1400 *0xffffffff80a0bd98 == 0x1 *0xffffffff80a0bda0 == 0xffffffff80812415 *0xffffffff80a0bda8 == 0xffffff8020001580 *0xffffffff80a0bdb0 == 0x1000ff8029831000 *0xffffffff80a0bdb8 == 0xc *0xffffffff80a0bdc0 == 0xffffffff8081eeb8 *0xffffffff80a0bdc8 == 0xc *0xffffffff80a0bdd0 == 0xffffff8020002560 *0xffffffff80a0bdd8 == 0xffffff8029831000 *0xffffffff80a0bde0 == 0x0 *0xffffffff80a0bde8 == 0x1ffed6 *0xffffffff80a0bdf0 == 0xffffff8029831000 *0xffffffff80a0bdf8 == 0xffffff80318c1c00 *0xffffffff80a0be00 == 0xffffff8020002540 *0xffffffff80a0be08 == 0xffffffff80a0be60 *0xffffffff80a0be10 == 0xffffff8020002540 *0xffffffff80a0be18 == 0xffffff80318c18a0 *0xffffffff80a0be20 == 0xffffff8029831000 Halting... halting... Kernel entry via Syscall, number: 1, Call Cap type: 12, Invocation tag: 54 - Debug Output #2: ===== SNIP: Same as above ===== IOMMU: Create VTD context table for PCI bus 0xff (pptr=0xff10d000) IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/208 T0xff10e400 "rootserver" @8048495]: Untyped Retype: Insufficient memory (1 * 8388608 bytes needed, 0 bytes available).>> Single bus detected lib_pci_scan_dev found pci device 0 0 PCI :: 00.00.00 : intel Unknown device ID. (vid 0x8086 did 0x29c0) line0 pin0 lib_pci_scan_dev found pci device 0 1 PCI :: 00.01.00 : Unknown vendor ID. Unknown device ID. (vid 0x1234 did 0x1111) line0 pin0 BAR0 : [ mem 0xfd000000 sz 0x1000000 szmask 0xff000000 prefetch ] BAR2 : [ mem 0xfebb0000 sz 0x1000 szmask 0xfffff000 ] lib_pci_scan_dev found pci device 0 2 PCI :: 00.02.00 : intel Unknown device ID. (vid 0x8086 did 0x100e) line11 pin1 BAR0 : [ mem 0xfeb80000 sz 0x20000 szmask 0xfffe0000 ] BAR1 : [ io 0xc000 sz 0x40 szmask 0xffffffc0 ] lib_pci_scan_dev found pci device 0 31 PCI :: 00.1f.00 : intel intel_ich9_8 (vid 0x8086 did 0x2918) line0 pin0 lib_pci_scan_dev found multi function device 0 31 PCI :: 00.1f.02 : intel Unknown device ID. (vid 0x8086 did 0x2922) line10 pin1 BAR4 : [ io 0xc080 sz 0x20 szmask 0xffffffe0 ] BAR5 : [ mem 0xfebb1000 sz 0x1000 szmask 0xfffff000 ] PCI :: 00.1f.03 : intel intel_ich9_6 (vid 0x8086 did 0x2930) line10 pin1 BAR4 : [ io 0x700 sz 0x40 szmask 0xffffffc0 ] seL4 failed assertion '(cte_t *)mdb_node_get_mdbNext(destSlot->cteMDBNode) == NULL && (cte_t *)mdb_node_get_mdbPrev(destSlot->cteMDBNode) == NULL' at /home/user/Documents/labs/rr/os/seL4-AUS/camkes_vm_examples/kernel/src/object/cnode.c:428 in function cteInsert halting... Kernel entry via Syscall, number: 1, Call Cap type: 12, Invocation tag: 53

2 1

Unable to setup Camkes VM tutorial
by Chris Koziarz 11 Sep '20

11 Sep '20

There is something wrong with Camkes VM repo or with my Linux machine. I am able to setup repo of other tutorials, i.e. repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest works. However when I continue into Camkes VM: root@ubuntu:~/lv4_repo# mkdir camkes_VM root@ubuntu:~/lv4_repo# cd camkes_VM root@ubuntu:~/lv4_repo/camkes_VM# repo init -u https://github.com/sel4/camkes-vm-examples-manifest.git -b tipc-stage I get the following error: Downloading Repo source from https://gerrit.googlesource.com/git-repo fatal: Cannot get https://gerrit.googlesource.com/git-repo/clone.bundle fatal: error [Errno -3] Temporary failure in name resolution fatal: cloning the git-repo repository failed, will remove '.repo/repo' What might be going wrong? As can be seen, I'm running on ubuntu v20.04 Any help appreciated. Chris

2 1

seL4 Summit 2020 - Call for Presentations *extended* to Sep 15.
by Kuz, Ihor (Data61, Kensington NSW) 10 Sep '20

10 Sep '20

Hi, For people not on the seL4 announce list: the 3rd annual seL4 Summit will be held online on November 15-18, 2020. A call for presentations is out, and the deadline for submissions has been extended to September 15, 2020. Please consider submitting something about seL4-based work that you are doing or other seL4/microkernel/trustworthy systems topics. Submission only requires a title and abstract, so it’s pretty low overhead. Submit by email to Summit2020(a)sel4-us.org. See more detail on the announce list[1]. Ihor. [1] https://sel4.systems/pipermail/announce/2020/000036.html

1 0