- Devel - lists.sel4.systems

A desktop OS based on seL4
by Jason Long 19 Aug '23

19 Aug '23

Hello,Is there an operating system that uses seL4 as a kernel and is suitable for home or server users like GNU/Linux or Windows OS? Thank you.

2 2

sel4cp and networking driver
by Sid Agrawal 14 Aug '23

14 Aug '23

Hi, I would like to setup a working example on sel4 with picoTCP and an eth driver. I came across this [1] from one of the seL4CP/sDDF demos and [2] from the camkes examples. However, I do not have access to those particular boards. I have a rspi4 and a Toradex Colibri iMX8X module with the aster carrier board. This Toradex has the same SoC ( iMX8X) as the tqma8xqp-1gb mentioned on the sel4cp website. Do you folks have any thoughts on how much effort it is getting seL4 working on "Toradex Colibri iMX8X" given it is supported on "tqma8xqp-1gb" which has the same SoC? I do not mind buying a specific development board as long as I know that I can use it for a while :) For folks who are working on sel4cp, what kind of dev setup do you have? I am looking for basic conveniences like flashing the image via USB (so I do not have to add/remove an SD card), TFTPboot, and some simple device drivers. I did see the instructions on TFTPbootat [3]. However, does it matter if the image was built via the sel4test of sel4cp? I think not, but I just wanted to double-check. And lastly, a higher-order question about seL4cp. How does sel4cp tie into the example in seL4_Libs [3], which has barebones libc and a VMM? Which is what I have used so far with sel4test. I understand that both sel4cp and camkes are for static systems, but I thought that I could use sel4cp to start some initial processes, such as a driver, a memory server, and some management processes. And later use process_spawn from seL4 libs to start additional PDs. Best, Sid [1] https://github.com/lucypa/sDDF [2] https://github.com/seL4/global-components/tree/master/components/Ethdriver/… [3] https://docs.sel4.systems/Hardware/GeneralARM

4 10

Confidentiality and realtime requirements
by Demi Marie Obenour 14 Aug '23

14 Aug '23

One of the goals of the MCS scheduler is to allow untrusted parts of the system (such as device drivers) to still have low interrupt latency. However, this seems to interact badly with the domain scheduler, as interrupts can arrive when the domain that will serve them is not scheduled. Worse, it appears that interrupts will generally require an IBPB (or equivalent) on both entry and exit, since they may interrupt any code. Is this accurate? If so, it seems that the “flush all μArch state” instruction coming to some RISC-V CPUs is insufficient, and full speculative taint tracking is required. More generally, requiring mutually distrusting domains to be explicitly marked seems to be problematic for anything that is not a static system: in a dynamic system (one that can run third-party code), one must typically assume that different address spaces are mutually distrusting, with the result that IPC latency will be severely impacted. Am I missing something, or will a general-purpose OS need full speculative taint tracking in hardware if it is to have fast IPCs between mutually-distrusting code on out-of-order CPUs? -- Sincerely, Demi Marie Obenour (she/her/hers)

3 13

Changing the cspace of a TCB while it is listening on a EP
by Sid Agrawal 08 Aug '23

08 Aug '23

Hi, I have a scenario and would like to understand how the kernel is expected to behave when I change the CSpace of a TCB when it is blocked on an EP. 1. A TCB (say TCB_1) is blocked on seL4_reply() on an endpoint (say EP_1). 2. Now, another PD, which has the capability to TCB_1, changes the CSpace of TCB_1 by using seL4_TCB_SetSpace(). Let's assume that the VSpace is identical. This new CSpace can be different from the old CSpace in 4 ways: A. It doesn't have the endpoint EP_1 B. It has the endpoint EP_1 but at a different CSlot. C. It has the endpoint EP_1 at the same CSlot. But since it is a different CSpace(so CNodes shared), it is a minted copy of the EP_1. Let's call it EP_1-prime. D. It has the endpoint EP_1 at the same CSlot, and it is the same EP as I have shared the CNode containing the EP_1 from the original CSpace. New and old CSpaces share the CNode containing that EP_1 like two trees sharing a sub-tree. I think scenario D should work as if nothing happened, but I do not know what to expect in scenarios A, B, and C. I will try these out soon, but I wanted your input as I did not find a clear answer in the manual. Best, Sid

2 2

Reminder seL4 developer hangout
by Birgit Brecknell 07 Aug '23

07 Aug '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Aug 9, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Ultra96V2 in sel4cp_VMM is cautiously here - initial support
by Nataliya Korovkina 06 Aug '23

06 Aug '23

Highlights, briefly... 1. Project "ultra96v2-sel4cpvmm" The project introduces changes to the three components: seL4, sel4CP, sel4cp_VMM. * Xilinx Linux booting requires SMC calls support in seL4. The project uses the SMC cap impelementation offered by DornerWorks (approved but not merged). * Changes in sel4CP relate to the new capability in seL4. * As for sel4cp_VMM, a policy of VM's SMC calls handling will be different from one VMM-PD to another. The project introduces registration of a custom handler by PD application as well as it provides the default handler - the simplest "pipe" passing calls and responses through. The project published as sets of patches to the components. More the details are in the README.md and Issue #1 - https://github.com/malus-brandywine/ultra96v2_sel4cpvmm/issues/1 of the project: https://github.com/malus-brandywine/ultra96v2_sel4cpvmm 2. Project "petalinux-ultra96v2-sel4cpvmm" The project enables generation of linux image and minimal rootfs to run VM with sel4cp_VMM. More details are in README.md of the project: https://github.com/malus-brandywine/petalinux-ultra96v2-sel4cpvmm Status: Linux VM loads to login prompt

1 0

2 weeks left to get the early-bird registration at the seL4 summit
by Birgit Brecknell 04 Aug '23

04 Aug '23

2 weeks left to get the early-bird registration at the seL4 summit! A friendly reminder that the early bird cut-off date is 18 August 2023. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and Dinner Registrations: https://events.linuxfoundation.org/sel4-summit/register/ seL4 summit 2023: https://sel4.systems/Foundation/Summit/2023/<https://sel4.systems/Foundation/Summit/2023/> --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

CMake error “Variable 'KernelArch' is not set.” Happens when building RISCV based seL4 system.
by sueboxian＠gmail.com 25 Jul '23

25 Jul '23

Hi, I met a CMake error, “Variable KernelArch is not set” when I tried to build a seL4 project based on the open source code of the UNSW course, Advanced Operating System, aka. AOS. The original version uses odroidc2 as the building platform, and I want to build it with the riscv gnu toolchain and simulate it on qemu-riscv-virt. Here is the repository: https://github.com/SEL4PROJ/AOS-manifest The building hierachy is as the basic build system structure, with init-build.sh, setting.cmake and CMakeLists.txt in the top level. And the top level contains kernel, tools, and project folders, in which there are CMakeLists.txt and .cmake files. Since I have no experience on cmake, I tried to compare the manifest xml between AOS project and seL4test project. I found that the major difference between them are in “init-build.sh”, “setting.cmake” and the “CMakeList.txt” in the top level. There are also some unused libraries in AOS project. I tried deleting the “set PLATFORM odroidc2” command in the setting.cmake, and added the DCROSSCOMPILER=riscv-unknown-linux-gnu, DPLATFORM=qemu-riscv-virt in the build command. But they doesn’t work. After checking the “/kernel/configs/seL4Config.cmake”, it says that the error is caused since KernelArch is left as empty string… And I want to ask whether I have set anything improperly.... I will appreciate for any help. Thank you for reading my question!

3 2

Reminder seL4 developer hangout
by Birgit Brecknell 24 Jul '23

24 Jul '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Jul 26, 5pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Soft-float problem happens when building seL4test using riscv64-unknown-linux-gnu-gcc toolchain
by sueboxian＠gmail.com 15 Jul '23

15 Jul '23

Hi, I met a problem when building seL4test project with riscv toolchain, with the float operations compiled as soft-float. Here are my configuration commands:  python3 ~/bin/repo init -u https://github.com/seL4/sel4test-manifest  python3 ~/bin/repo sync  mkdir build-riscv  cd build-riscv  ../init-build.sh -DPLATFORM=qemu-riscv-virt -DCROSS_COMPILER_PREFIX=riscv64-unknown-linux-gnu- -DSIMULATION=TRUE  ninja The terminal reported "can't link double-float modules with soft-float modules" errors when compiling fpu.c, and thus stopped compilation. I have tried rebuilding the glibc version riscv toolchain, with multilib enabled. But it doesn't work. I also checked the terminal, it says that I'm compiling with march=riscv64imac_zicsr_zifencei -mabi=lp64, which as the best of my knowledge, means compiling the float as soft-float. I want to know whether I lossed something. I would appreciate for any help. Thanks in advance.

3 6