- Devel - lists.sel4.systems

Release 0.1.0 of LionsOS
by Ivan Velickovic 16 Apr '24

16 Apr '24

Hello all This is a message to let people know that version 0.1.0 of LionsOS has been released. LionsOS is aimed at embedded, IoT and cyberphysical systems and is designed to be formally verifiable, adaptable to a wide class of use cases in the target domain, while at the same time setting the benchmark for performance of microkernel-based operating systems. We expect to achieve all three aims by a highly modular yet ruthlessly performance-oriented design and strict adherence to the time-honoured KISS principle. LionsOS is still in its early stages but we are at the point where we have a non-trivial example system and initial documentation. You can find the website here: https://lionsos.org/ and the source code here: https://github.com/au-ts/lionsos Thanks, Ivan

1 0

One week to go to submit a talk for seL4 summit 2024
by Birgit Brecknell 15 Apr '24

15 Apr '24

One week to go to submit a talk [0] for seL4 summit 2024 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. The seL4 Summit 2024 will be held 15-17 October 2024 at the Holiday Inn Potts Point, Sydney, Australia. The summit will be an in-person event. Registration details to follow soon. We’re looking forward to many exciting proposals! [0] https://sel4.systems/Foundation/Summit/2024/cfp [1] https://sel4.systems/Foundation/Summit/2024/ [2] https://sel4.systems/Foundation/Summit/2024/submit Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

question about the seL4/camkes-vm-examples
by PX 15 Apr '24

15 Apr '24

Hi,All I am trying to build the seL4 VMM example for the qemu-arm-virt platform from seL4/camkes-vm-exmaples. I can build the vmm image successfully, but I cannot run the image. Here are what I did: 1. I use the "../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt" command. 2. ninja After these two steps, the vmm image, capdl-loader-image-arm-qemu-arm-virt is successfully built. But when I run the generated scripts, ./simulate, to run the VMM on qemu, the vmm fails to boot up. The error message is attached below. I use Ubuntu 20.04 and QEMU emulator version 4.2.1. Do I miss something here? Do I use the correct version of the building environment? Any help would be appreciated! ./simulate ./simulate: QEMU command: qemu-system-arm -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a15 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p1 paddr=[61805000..62c02ebf] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 6192264c. Loaded DTB from 6192264c. paddr=[60042000..60043fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60041fff] vaddr=[e0000000..e0041fff] virt_entry=e0000000 ELF-loading image 'capdl-loader' to 60044000 paddr=[60044000..6140cfff] vaddr=[10000..13d8fff] virt_entry=1880c Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. available phys memory regions: 1 [60000000..c0000000] reserved virt address space regions: 4 [e0000000..e0042000] [e0042000..e0043da9] [e0044000..e140d000] [ff000000..ff200000] Booting all finished, dropped to user space *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 65536 bytes needed, 0 bytes available).>>* run@main.c:1332 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1) install_vm_devices@main.c:704 module name: map_frame_hack install_vm_devices@main.c:704 module name: init_ram Loading Kernel: 'linux' Loading Initrd: 'linux-initrd' Loading Generated DTB -------- *Pagefault from [vm0]: read prefetch fault @ PC: 0x4 IPA: 0x4, FSR: 0x6* *Context:* *r0: 0x0* *r1: 0xffffffff* *r2: 0x4f000000* *r3: 0x0* *r4: 0x0* *r5: 0x0* *r6: 0x0* *r7: 0x0* *r8: 0x0* *r9: 0x0* *r10: 0x0* *r11: 0x0* *r12: 0x0* *pc: 0x4* *r14: 0x0* *sp: 0x0* *cpsr: 0x9b* m-------- main_continued@main.c:1310 Failed to run VM Halting...

3 4

seL4 developer hangout reminder
by Birgit Brecknell 15 Apr '24

15 Apr '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 16 Apr, 22:00 UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 docker build issues on Apple Silicon
by Mark Jones 14 Apr '24

14 Apr '24

Dear All, I’m trying to use the instructions on https://docs.sel4.systems/projects/dockerfiles/ to set up an seL4 docker build environment on an Apple Silicon Mac. I’ve actually tried this on two different machines (with small variations in the versions of macOS Sonoma, Apple Silicon, and Docker between each of the machines), but get the same result on each one. I’m hoping that other folks on this list might know how to fix this. I start by running: git clone https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles.git cd seL4-CAmkES-L4v-dockerfiles make user But the make command fails with the output appended below. Any hints (including other places to post this question) would be much appreciated! Best wishes, Mark ______________ scripts/utils/check_for_old_docker_imgs.sh WARNING: Unable to check if your trustworthysystems docker images are getting a bit old! The date command did not behave as expected. Skipping the check. docker build --force-rm=true \ --build-arg=USER_BASE_IMG=trustworthysystems/camkes \ -f dockerfiles/extras.Dockerfile \ -t extras \ . [+] Building 109.7s (6/6) FINISHED docker:desktop-linux => [internal] load build definition from extras.Dockerfile 0.0s => => transferring dockerfile: 602B 0.0s => [internal] load metadata for docker.io/trustworthysystems/camkes:latest 1.4s => [internal] load .dockerignore 0.0s => => transferring context: 153B 0.0s => [1/2] FROM docker.io/trustworthysystems/camkes:latest@sha256:29206d51ef1d09bb5e1934b11a1946a13d13333ab0ff7c2ff2645ea 96.3s => => resolve docker.io/trustworthysystems/camkes:latest@sha256:29206d51ef1d09bb5e1934b11a1946a13d13333ab0ff7c2ff2645ea2 0.0s => => sha256:e943b5afb84223c55b5dfdbe2f383970021765c345c51b08fa8b9b0d4d69ccd7 9.97kB / 9.97kB 0.3s => => sha256:46cbb6e89f5727950fb43b0c4b18a28073c18ad928ccf16c6e2a9f6d708ccb35 80.82MB / 80.82MB 6.9s => => sha256:29206d51ef1d09bb5e1934b11a1946a13d13333ab0ff7c2ff2645ea2e12c65f2 1.79kB / 1.79kB 0.0s => => sha256:678186f76064904e561bbec5cc0fb200e1c7d0435dbeeaf2433d050631a132ab 6.82kB / 6.82kB 0.0s => => sha256:99046ad9247f8a1cbd1048d9099d026191ad9cda63c08aadeb704b7000a51717 31.36MB / 31.36MB 3.0s => => sha256:4f4fb700ef54461cfa02571ae0db9a0dc1e0cdb5577484a6d75e68dc38e8acc1 32B / 32B 0.8s => => sha256:be52171dda4a5d045a589cf92b25fe60ac5b74dac75bb03997d5a049d47b361e 1.15GB / 1.15GB 53.1s => => extracting sha256:99046ad9247f8a1cbd1048d9099d026191ad9cda63c08aadeb704b7000a51717 1.2s => => sha256:460c68d68ad3efcc4c324e3da3ea9a8d7ebee818d87643e78fa551c90106c218 1.19GB / 1.19GB 65.4s => => extracting sha256:e943b5afb84223c55b5dfdbe2f383970021765c345c51b08fa8b9b0d4d69ccd7 0.0s => => extracting sha256:46cbb6e89f5727950fb43b0c4b18a28073c18ad928ccf16c6e2a9f6d708ccb35 3.0s => => extracting sha256:4f4fb700ef54461cfa02571ae0db9a0dc1e0cdb5577484a6d75e68dc38e8acc1 0.0s => => extracting sha256:be52171dda4a5d045a589cf92b25fe60ac5b74dac75bb03997d5a049d47b361e 20.1s => => extracting sha256:460c68d68ad3efcc4c324e3da3ea9a8d7ebee818d87643e78fa551c90106c218 22.7s => [2/2] RUN apt-get update -q && apt-get install -y --no-install-recommends cowsay sudo 11.8s => exporting to image 0.1s => => exporting layers 0.1s => => writing image sha256:29bf5499ec09fe5c0398c5023deb519373d25d2c8ea0d3d0d964759317511415 0.0s => => naming to docker.io/library/extras 0.0s View build details: docker-desktop://dashboard/build/desktop-linux/desktop-linux/ohi6vc8w1dj06hmvvu5ocypjs What's Next? 1. Sign in to your Docker account → docker login 2. View a summary of image vulnerabilities and recommendations → docker scout quickview docker build --force-rm=true \ --build-arg=EXTRAS_IMG=extras \ --build-arg=UNAME=user \ --build-arg=UID=502 \ --build-arg=GID=20 \ --build-arg=GROUP=staff \ -f dockerfiles/user.Dockerfile \ -t user_img-user . [+] Building 0.7s (2/2) FINISHED docker:desktop-linux => [internal] load build definition from user.Dockerfile 0.0s => => transferring dockerfile: 353B 0.0s => ERROR [internal] load metadata for docker.io/library/extras:latest 0.6s ------ > [internal] load metadata for docker.io/library/extras:latest: ------ user.Dockerfile:9 -------------------- 7 | ARG EXTRAS_IMG=extras 8 | # hadolint ignore=DL3006 9 | >>> FROM $EXTRAS_IMG 10 | 11 | # Get user UID and username -------------------- ERROR: failed to solve: extras: pull access denied, repository does not exist or may require authorization: server message: insufficient_scope: authorization failed View build details: docker-desktop://dashboard/build/desktop-linux/desktop-linux/q25mw2voldchjfgf3ybhy2q0d make: *** [build_user] Error 1

2 2

Release 0.4.0 of the seL4 Device Driver Framework
by Ivan Velickovic 09 Apr '24

09 Apr '24

Hello all This is a message to let people know that version 0.4.0 of the seL4 Device Driver Framework (sDDF) has been released. The sDDF aims to provide a collection of interfaces, libraries and tools for writing device drivers for seL4 that allow accessing devices securely and with low overhead. Some may be familiar with the sDDF from previous seL4 Summit talks. Since the pre-release at the 2023 Summit, we have made significant improvements to the networking sub-system, generally rationalising interfaces and further improving performance, the Ethernet device-class interfaces are now mature. We have also introduced preliminary specs and prototype implementations for serial, I2C, block, audio and graphics device classes. You can find information about the release and the accompanying documentation here: https://github.com/au-ts/sddf/releases/tag/0.4.0 Thanks, Ivan

1 0

Two weeks to go to submit a talk for seL4 summit 2024
by Birgit Brecknell 08 Apr '24

08 Apr '24

Two weeks to go to submit a talk [0] for seL4 summit 2024 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. The seL4 Summit 2024 will be held 15-17 October 2024 at the Holiday Inn Potts Point, Sydney, Australia. The summit will be an in-person event. Registration details to follow soon. We’re looking forward to many exciting proposals! [0] https://sel4.systems/Foundation/Summit/2024/cfp [1] https://sel4.systems/Foundation/Summit/2024/ [2] https://sel4.systems/Foundation/Summit/2024/submit -- Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems bbrcknl(a)gmail.com

1 0

sel4test CACHEFLUSH0001 failed
by Leonid Meyerovich 29 Mar '24

29 Mar '24

Hello, I run sel4test on the aarch64 platform. My CACHEFLUSH0001 test in sel4test failed /* Clean makes data observable to non-cached page */ *ptr = 0xC0FFEE; *ptrc = 0xDEADBEEF; test_assert(*ptr == 0xC0FFEE); test_assert(*ptrc == 0xDEADBEEF); I have tried to make to 'improve' memory/cache coherence, but the last assertion still failed /* Clean makes data observable to non-cached page */ *ptr = 0xC0FFEE; *ptrc = 0xDEADBEEF; error = seL4_ARM_Page_Clean_Data(framec, 0, PAGE_SIZE_4K); error = seL4_ARM_Page_Invalidate_Data(framec, 0, PAGE_SIZE_4K); __asm volatile("dmb sy" ::: "memory"); test_assert(*ptr == 0xC0FFEE); test_assert(*ptrc == 0xDEADBEEF); Thank you, Leonid

2 2

Re: Only 512mb ram available on capdl-loader-image-arm-qemu-arm-virt image
by Peter Chubb 26 Mar '24

26 Mar '24

>>>>> "Daniele" == Daniele Feliciani <felicianidaniele(a)gmail.com> writes: Daniele> Hello Peter, I have the same Daniele> problem. i tried to change the guest ram value to Daniele> 0x40000000. I added set(QEMU_MEMORY "2048") in config.cmake Daniele> but I get the following errors while running : " Daniele> map_vm_memory_reservation@guest_memory.c:477 Failed to get Daniele> frame for reservation address 0x60000000" and " Daniele> vm_ram_touch@guest_ram.c:165 Failed to touch ram region: Not Daniele> registered RAM region 32 bit ARM insts not decoded" Check the size of the MMIO region. By default it uses 29 bits; for a 2G region you need 31 bits. In the devices.camkes file, in the untyped_mmios section. There's probably an entry, "0x40000000:29", try increasing this to "0x40000000:31" to get a 2^31 region. -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

3 3

Re: Only 512mb ram available on capdl-loader-image-arm-qemu-arm-virt image
by Daniele Feliciani 25 Mar '24

25 Mar '24

It doesn't seem to work. I'm attaching the device.camkes file and the error screenshots. Il giorno lun 25 mar 2024 alle ore 10:43 Peter Chubb < peter.chubb(a)unsw.edu.au> ha scritto: > >>>>> "Daniele" == Daniele Feliciani <felicianidaniele(a)gmail.com> writes: > > Daniele> I changed the value but now i > Daniele> have the following error: > > Danielle> ./simulate: QEMU command: qemu-system-aarch64 -machine > Danielle> virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 > -nographic > Danielle> -m size=2048 -kernel > images/capdl-loader-image-arm-qemu-arm-virt > Danielle> ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 > Danielle> paddr=[61b07000..62ee00b7] > Danielle> No DTB passed in from boot loader. > Danielle> Looking for DTB in CPIO archive...found at 61c07c68. > Danielle> Loaded DTB from 61c07c68. > Danielle> paddr=[60242000..60243fff] > Danielle> ELF-loading image 'kernel' to 60000000 > Danielle> paddr=[60000000..60241fff] > Danielle> vaddr=[8060000000..8060241fff] > Danielle> virt_entry=8060000000 > Danielle> ELF-loading image 'capdl-loader' to 60244000 > Danielle> paddr=[60244000..6170cfff] > Danielle> vaddr=[400000..18c8fff] > Danielle> virt_entry=408d88 > Danielle> Enabling hypervisor MMU and paging > Danielle> Jumping to kernel-image entry point... > Danielle> > Danielle> Bootstrapping kernel > Danielle> Warning: Could not infer GIC interrupt target ID, assuming 0. > Danielle> available phys memory regions: 1 > Danielle> [60000000..c0000000] > ^^^^^^^^^ this is the physical memory region you have to play > with. Make the region given to the VM start at 0x60000000 > instead of 040000000 > > -- > Dr Peter Chubb https://trustworthy.systems/ > Trustworthy Systems Group CSE, UNSW > Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm. >

1 0