- Devel - lists.sel4.systems

some unexpected phenomenon about scheduling
by yadong.li 07 Aug '21

07 Aug '21

Hi: Recently, I found some unexpected phenomenon about scheduling on our project. My environment as follows: I run linux guest on seL4, Linux guest has 8 vcpu on 8 Arm PE from core0 ~ core7. WFI is not trap, seL4 is master kernel not mcs kernel I think seL4 idle task will not be run on core1, it will always run vcpu task. But the truth is the idle task will be run. I found when the maintenance and timer interrupt of Linux guest came, it will switch to idle, Because above interrupts handle will call handleFault, the sendIPC will set the ksCurThread(vcpu task) block on send, and the ksReadyQueuesL1Bitmap is empty. The idle task wille be run. But the recv task maybe run on core0, now core1 is in idle, is it reasonable? Thank you very much

2 1

Failure on a CAmkES-VM with more than 150MB RAM
by hamed_ganji＠aut.ac.ir 06 Aug '21

06 Aug '21

Hello, I have a problem on booting a CAmkES-VM with more than 150MB RAM. The following error appears when I set [vm0.guest_ram_mb = 256] in the camkes file of the minimal example of CAmkES-VM and boot the produced image on both QEMU and real hardware system: ------------------------------------------------------------ ... vka_alloc_object_at_maybe_dev@object.h:64 Failed to allocate object of size 4096, error 1 alloc_bios_memory@acpi.c:119 Failed to allocate frame for bios addr 0xe0000 main_continued@main.c:871 [Cond failed: error] Failed to init guest boot structure ------------------------------------------------------------ Please find the full output of the booting process in attachment file. I also examined the effect of other parameters like [vm0.simple_untyped23_pool] and [vm0.heap_size] but no difference was found. Any help/hint would be very appreciated. Best regards, Hamed Ganji

1 0

Where does rumprun mount /
by Ellis 04 Aug '21

04 Aug '21

Hello, I have been messing around with sel4 rumprun and I have been trying to put files onto the file system. Where does rumprun mount the root / ? Sincerely, Ellis

1 0

Operating Systems built on top of seL4
by Sidhartha Agrawal 02 Aug '21

02 Aug '21

Hello sel4-devs, I am a first-year graduate student at the University of British Columbia at their Systopia Lab <https://systopia.cs.ubc.ca/> working on operating systems research. My advisor is Prof. Margo Seltzer <https://www.seltzer.com/margo>. In a past life, I have worked as a software engineer at Oracle and Arista Networks. My research is on General Purpose Isolation Mechanism in the OS. We ask whether we really need to have N different isolation mechanisms or whether instead, we could develop a framework in which all these different mechanisms represent points on a continuum. Here is a write-up <https://sid-agrawal.ca/#research-projects> with some more details. I am using seL4 as the microkernel base to build my research idea. At this stage, I am not looking in to the formal verification aspect of seL4, but that might change once I have a better idea about the type of mechanism I want to build. I would also like to keep the changes in the kernel to be minimum and try to demonstrate my ideas using user space processes. I have tried out the tutorials on the seL4 website. Currently, I am wading through the different helper libraries in seL4/seL4_libs <https://github.com/seL4/seL4_libs>. As someone who is just starting with seL4 ecosystem, I had a few high-level questions: - Are there are example OSes built with seL4, which would be a good place to look at? Specifically, I am looking for components such as basic versions of a process-server, vm-server, pager, file-systems server. - I came across refOS <https://github.com/seL4/refos>, but wasn't sure if it is still being maintained. - Another option was Genode <https://genode.org/documentation/general-overview/index>. This seemed to be maintained by another community and has many layers of abstractions since it supports multiple kernel backends. I am looking forward to engaging with this community, learning about seL4 and making meaningful contributions. Best, Sid sid-agrawal.ca

8 28

Sel4 rumprun has issues compiling
by Vortex 01 Aug '21

01 Aug '21

Hello, I would like to bring this issue to the attention of the community. Sel4’s fork of the rumprun unikernel no longer compiles. Due to the usage of Werror flag, the compiler produces repeated warnings which in turn creates errors. It seems like the rump kernel was tested on an older version of gcc and because it is older, raises warnings and causes the build to fail on newer compilers. This is a similar issue to https://github.com/rumpkernel/rumprun/issues/82 I have tested rumprun in the sel4 docker container. My build logs are also attached to this email. Thank you for taking attention to this issue. Sincerely, Ellis

3 3

Docker for ARM?
by dave＠synergy.org 27 Jul '21

27 Jul '21

I recently moved and my x86-64 machines are in storage. Are there docker images for Debian ARM/32 or Raspbian I can use to build seL4 on my Raspberry Pi? It is my target platform. Thanks, Dave

2 1

Camkes and native tcp/ip and networking
by Amirreza Zarraby 27 Jul '21

27 Jul '21

Hello seL4 team, I am try trying to use camkes to write a simple firewall. I am wondering if you can direct me to any existing camkes project which uses tcp/ip and network driver that I can look into as starting point. There is a seL4 based webserver but it seems to use vm and Linux. Thank you for your time. - Amir

4 3

Jetson AGX Xavier board porting
by bobding＠msn.com 27 Jul '21

27 Jul '21

Has anyone ported to Nvidia AGX Xavier board?

2 1

camkes-vm-examples-manifest cma34cr_centos fails
by christinefragoso＠protonmail.com 27 Jul '21

27 Jul '21

Hello, I'm trying to run the cma34cr_centos application from camkes-vm-examples-manifest, but I get this error: "Kernel entry via Unknown syscall, word: 65". I've set up VMware as described at https://docs.sel4.systems/Hardware/VMware/. In camkes-vm-examples-manifest/cma34cr_centos_x86_build, I've built the kernel: ../init-build.sh -DCAMKES_VM_APP=cma34cr_centos Then I ran these commands: ninja sudo ./seL4vmw.py images/kernel-x86_64-pc99 images/capdl-loader-image-x86_64-pc99 vmrun -T player start $HOME/vmware/seL4/seL4.vmx while :; do socat -d -d UNIX-CONNECT:/tmp/vsock,forever PTY,link=/tmp/mytty done After VMware boots, I ran minicom in a separate terminal to see the serial output: minicom -D /tmp/mytty Here is the full log: Welcome to minicom 2.7.1 OPTIONS: I18n Compiled on Dec 23 2019, 02:06:26. Port /tmp/mytty, 08:47:50 Press CTRL-A Z for help on special keys Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xcf3000 end=0x3821bb8 size=0x2b2ebb8 name='' Parsing GRUB physical memory map Physical Memory Region from 0 size 9f800 type 1 Physical Memory Region from 9f800 size 800 type 2 Physical Memory Region from dc000 size 24000 type 2 Physical Memory Region from 100000 size bfde0000 type 1 Adding physical memory region 0x100000-0xbfee0000 Physical Memory Region from bfee0000 size 1f000 type 3 Physical Memory Region from bfeff000 size 1000 type 4 Physical Memory Region from bff00000 size 100000 type 1 Adding physical memory region 0xbff00000-0xc0000000 Physical Memory Region from f0000000 size 8000000 type 2 Physical Memory Region from fec00000 size 10000 type 2 Physical Memory Region from fee00000 size 1000 type 2 Physical Memory Region from fffe0000 size 20000 type 2 Physical Memory Region from 100000000 size 140000000 type 1 Adding physical memory region 0x100000000-0x240000000 Got VBE info in multiboot. Current video mode is 16703 ACPI: RSDP paddr=0xf6a00 ACPI: RSDP vaddr=0xf6a00 ACPI: RSDT paddr=0xbfeee733 ACPI: RSDT vaddr=0xbfeee733 Warning: Your kernel was not compiled for the current microarchitecture. Kernel loaded to: start=0x100000 end=0xc1f000 size=0xb1f000 entry=0x100300 ACPI: RSDT paddr=0xbfeee733 ACPI: RSDT vaddr=0xbfeee733 ACPI: FADT paddr=0xbfefef67 ACPI: FADT vaddr=0xbfefef67 ACPI: FADT flags=0x21 ACPI: 0 IOMMUs detected ACPI: MADT paddr=0xbfeee937 ACPI: MADT vaddr=0xbfeee937 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x2 ACPI: MADT_APIC apic_id=0x4 ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0x6 ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0x8 ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0xa ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0xc ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0xe ACPI: Not recording this APIC, only support 2 ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x5 ACPI: 2 CPU(s) detected ELF-loading userland images from boot modules: size=0x3fab000 v_entry=0x408828 v_start=0x400000 v_end=0x43ab000 p_start=0x3822000 p_end=0x77cd000 Moving loaded userland images to final location: from=0x3822000 to=0xc1f000 size=0x3fab000 Starting node #0 with APIC ID 0 Mapping kernel window is done Starting node #1 with APIC ID 2 Booting all finished, dropped to user space create_object@main.c:673 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0xb0000000 seL4 root server abort()ed Debug halt syscall from user thread 0xffffff823e027400 "rootserver" halting... Kernel entry via Unknown syscall, word: 65 Any idea what's wrong? I just want to get one x86 application with cross VM connectors working. The other x86 applications (optiplex9020, cma34cr_ubuntu, zmq_samples) in camkes-vm-examples-manifest don't work for other reasons.

2 1

Formally verified AES C code
by Hugo V.C. 20 Jul '21

20 Jul '21

Hi all, I don't want to use SSL/openssl in a project I'm working. Thus, I want to just use my own encryption at the app layer. As performance is not a problem (just very small data packets over a socket) I would like to have the most simple implementation possible of AES, preferably, formally verified. Is anyone aware of any public AES encrytion implementation in C that has been formally or semi-formally verified? Thank you!

5 10