- Devel - lists.sel4.systems

seL4 developer hangout reminder
by Birgit Brecknell 28 Apr '24

28 Apr '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 1 May, 8: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 summit: deadline extension to 29 April 2024
by Birgit Brecknell 22 Apr '24

22 Apr '24

The deadline to submit a presentation to the seL4 summit 2024 [0] has been extended by 1 week. You now have until 29 April 2024 to propose a talk [1], by uploading an abstract of one page or less to the submission portal [2]. Looking forward to receiving your proposals. We want to hear about your cool seL4 work! And spread the word! If you want to hear about specific seL4 work, ping people around you or let us know at summit(a)sel4.systems. [0] https://sel4.systems/Foundation/Summit/2024/ [1] https://sel4.systems/Foundation/Summit/2024/cfp [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 LionsOS
by Isaac Beckett 20 Apr '24

20 Apr '24

Hello! Looking at the LionsOS website and documentation you posted, it seems like Lions is an operating system built using Microkit out of components/drivers that use the sDDF? Do I have the right shape of things in my head? Also, would sDDF drivers for a static OS like Lions (or other OS built in Microkit, since that’s what’s it’s built for) be potentially portable to other operating systems using the seL4 kernel and sDDF? Like, if I design a non-static operating system that uses sDDF drivers, could I use existing code from Lions or would I face issues with code assuming that the system’s components can’t change at runtime? Thanks, Isaac

11 26

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

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 13 Apr '24

13 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