- Devel - lists.sel4.systems

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

Cannot reserve memory for camkes VM guest
by Alex Ling 17 Jul '21

17 Jul '21

Hi All, I'm trying to bring up camkes VM Linux guest on Firefly RK3399 board which is with a GICv3 ARMv8. I'm using the "rockpro64" target and my work is based on [1] and [2]. When I run the "capdl-loader-image-arm-rockpro64", there's error "Range not available at 0xfef10000, size 0x10000". Bootstrapping kernel Booting all finished, dropped to user space Undelivered IRQ: 132 Install gic v3 sel4utils_reserve_range_at_no_alloc@vspace.c:595 Range not available at 0xfef10000, size 0x10000 vm_reserve_memory_at@guest_memory.c:328 Failed to allocate vm reservation: Unable to create vspace reservation at address 0xfef10000 of size 65536 vm_install_vgic_v3@vgic_v3.c:87 Error installing vgic Assertion failed: !err (/mnt/data3/projects/rk3399/build/seL4/camkes-vm-app/projects/vm/components/VM_Arm/src/main.c: main_continued: 1098) Here's my projects/seL4_projects_libs/libsel4vmmplatsupport/plat_include/rockpro64/sel4vmmplatsupport/plat/devices.h content: #define GIC_VERSION_3 #define GIC_PADDR 0xfee00000 #define GIC_DIST_PADDR (GIC_PADDR + 0x00000000) #define GIC_DIST_SIZE 0x10000 #define GIC_REDIST_PADDR 0xfef00000 #define GIC_REDIST_SIZE 0xC0000 #define GIC_REDIST_SGI_PADDR (GIC_REDIST_PADDR + 0x00010000) #define GIC_REDIST_SGI_SIZE 0x10000 I think the problem is related to GIC_REDIST_SIZE. I set it to 0xC0000 according to the rockpro64 device tree file in kernel/tools/dts/rockpro64.dts interrupt-controller@fee00000 { compatible = "arm,gic-v3"; #interrupt-cells = < 0x04 >; #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; interrupt-controller; reg = < 0x00 0xfee00000 0x00 0x10000 0x00 0xfef00000 0x00 0xc0000 0x00 0xfff00000 0x00 0x10000 0x00 0xfff10000 0x00 0x10000 0x00 0xfff20000 0x00 0x10000 >; interrupts = < 0x01 0x09 0x04 0x00 >; phandle = < 0x01 >; I tried to reduce it to 0x10000 and it can boot to VM guest but the guest Linux will fail in gic_iterate_rdists() because it cannot read from GIC's GICR_TYPER register correctly. Did I miss anything? Any suggestion is highly appreciated. Thank you very much! [1] https://github.com/seL4/seL4/pull/378 [2] https://github.com/seL4/seL4_projects_libs/tree/sylvain/gicv3 Regards, Alex

2 2

Passing caps through CAmkES procedures?
by Austin Appleby 14 Jul '21

14 Jul '21

Hi, I've got what seems like a simple task that I can't quite figure out how to implement - I am sketching out a key-value-store component where the "values" can be quite large (tens or hundreds of K). I would like clients of the component to pass caps to their own buffers in and out of this component's API to minimize copying and temporary buffer allocation and ensure that multiple clients can't see each other's data. In plain seL4 this would be done via the client passing a cap in its seL4_Call(), but I don't see an equivalent for this in CAmkES. Is there a way of declaring this in the .camkes syntax? If not, is there a way to build this component outside of CAmkES and still allow it to interact with existing CAmkES components? -Austin Appleby @ Google

1 0

CI infrastructure outage
by Peter Chubb 09 Jul '21

09 Jul '21

Hi Folks, Our continuous integration testing infrastructure is being relocated from CSIRO to UNSW premises this weekend. Because Sydney is in COVID lockdown, and because we're reworking the system not to rely on commercial software we no longer have a licence for (Atlassian Bamboo), we will probably not have everything working again for two or three weeks. The upshot for you is that any pull request that needs extensive testing will not be merged for at least two weeks, possibly longer. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0