August 2023 - Devel - lists.sel4.systems

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

16 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 27 Aug '23

27 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 21 Aug '23

21 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 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