August 2023 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 15 Oct '24

15 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

Standalone experiments
by sean bruno 01 Sep '23

01 Sep '23

I'm investigating some of the different microkernels out there for some graduate exploration. The tutorials were awesome and got me bootstrapped *very* quickly, thank you for the effort on those. I am attempting to build a "hello-world" on my own and seem to be missing a step as base.cmake no longer can see the musllibc that I have in my tree. I'm fairly certain my CMake knowledge here is weak or I just flat out missed a step. My checkout tree looks like the following: $ tree -L 1 ├── build ├── CMakeLists.txt -> tools/cmake-tool/default-CMakeLists.txt ├── init-build.sh -> tools/cmake-tool/init-build.sh ├── kernel ├── projects ├── README.md └── tools $ tree -L 1 projects/ projects/ ├── hello-world ├── musllibc ├── seL4_libs └── util_libs When cmake runs from build, I see the following: ~/build]$ cmake -DCROSS_COMPILER_PREFIX=aarch64-linux-gnu- -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -C ../kernel/configs/AARCH64_verified.cmake ../projects/hello-world/ loading initial cache file ../kernel/configs/AARCH64_verified.cmake -- The C compiler identification is GNU 12.1.1 -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /usr/lib64/ccache/aarch64-linux-gnu-gcc - skipped -- Detecting C compile features -- Detecting C compile features - done -- The CXX compiler identification is GNU 12.1.1 -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /usr/lib64/ccache/aarch64-linux-gnu-g++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/lib64/ccache/aarch64-linux-gnu-gcc -- /home/sbruno/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating from DTB... WARNING:root:Only mapping 4096/16777216 bytes from node /iommu@12000000, region 0. Set kernel_size in YAML to silence. -- CPIO test cpio_reproducible_flag PASSED CMake Error at /home/sbruno/tools/cmake-tool/base.cmake:55 (find_package): By not providing "Findmusllibc.cmake" in CMAKE_MODULE_PATH this project has asked CMake to find a package configuration file provided by "musllibc", but CMake did not find one. Could not find a package configuration file provided by "musllibc" with any of the following names: musllibcConfig.cmake musllibc-config.cmake Add the installation prefix of "musllibc" to CMAKE_PREFIX_PATH or set "musllibc_DIR" to a directory containing one of the above files. If "musllibc" provides a separate development package or SDK, be sure it has been installed. Call Stack (most recent call first): CMakeLists.txt:4 (include) -- Configuring incomplete, errors occurred!

2 1

CPU design, Re: Confidentiality and realtime requirements
by Isaac Beckett 26 Aug '23

26 Aug '23

> Date: Sun, 13 Aug 2023 16:18:08 +0000 > From: Gernot Heiser <gernot(a)unsw.edu.au> > Subject: [seL4] Re: Confidentiality and realtime requirements > To: devel <devel(a)sel4.systems> > >>>> On 12 Aug 2023, at 02:07, Demi Marie Obenour <demiobenour(a)gmail.com> wrote: >>>> >>> If you want to relax this, you’ll need a very careful analysis of your security requirements, and deploy TP where needed and omit where it’s not needed. But you can't prevent µarch timing channels without TP. Everybody knows about D-cache channels these days and how easy they are to exploit, and similar with LLC channels. And if you want to prevent at least those, then full TP has no extra cost. >> >> Does time protection require temporal isolation? > > Nope. Time protection is the mechanism that allows providing temporal isolation. > >>> Developing such a framework is on my agenda (it’s a core part of what I said I’m waiting for a good PhD student to work on). Basically I want to be able to make certain security guarantees where components have overt communication channels. An example is tab isolation in a browser: We want to have a fully functional web browser that allows processing of sensitive information in one tab, but guarantee that it cannot be leaked to a different tab. >> >> Another good example is different apps on a mobile device. Android allows any two applications on the same profile to communicate with mutual consent, and yet also allows one application to keep information secret from another. > > Yes. The smartphone space is really interesting. While built on top of the classical Unix security model (but implementable on a much simpler model) it demonstrates that stricter security policies (compared to desktops) can be made acceptable to users. > >> One critical requirement is that such a framework must allow an efficient implementation, both in terms of performance and power consumption. If it isn’t efficient enough to be deployed, then it won’t do people any good. > > Energy is (to first order) proportional to computation, so just looking at “performance” is good enough. > > And performance has always been our driver – see “security is no excuse for bad performance!” ;-) > > As I argued earlier, the performance cost of time protection is not higher than what you need to eliminate just the most easily exploitable cache channels. > > Gernot This makes me wonder if it’d make sense to design a new CPU and/or instruction set with the goal of eliminating timing and other side channels. Like, we had the Lisp machines with hardware support for Lisp, and now most CPUs are optimized for C and similar languages, and in turn those languages are optimized for those CPUs (x86, Arm, etc.). But I can’t say I know enough about computer science at this time to even tinker with the idea. And also, on the other hand maybe it doesn’t make sense to create hardware and accompanying software that are nearly impossible to non-destructively subvert, given the concerning trend of computer manufacturers and tech companies of restricting what code can run on their products. I don’t want to make something that could be set up to prevent an end user from modifying or running their own code. Isaac

4 9

How to understand seL4?
by Jason Long 24 Aug '23

24 Aug '23

Hello,I want to learn seL4 deeply. So that I can figure it out and develop it. Where should I start? Thank you.

2 1

How to enable SMP on qemu-arm-virt
by chenpingyuan＠xiaomi.com 21 Aug '23

21 Aug '23

Hello cool guys, I'm trying SEL4 using qemu-arm-virt platform with command： ../init-build.sh -DPLATFORM=qemu-arm-virt -DSIMULATION=true I noticed that SMP was not enabled by default, so I added: set(KernelMaxNumNodes "4") into kernel\src\plat\qemu-arm-virt\config.cmake. After running it with command ./simulate , I got the following error log and seL4 refused to continue: HVC is not supported for PSCI! My question is how shall I change the build scripts in order to run seL4 with SMP on qemu-arm-virt platform. Regards

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 20 Aug '23

20 Aug '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Aug 23, 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

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 13 Aug '23

13 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 13 Aug '23

13 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