Devel April 2022

devel@sel4.systems

21 participants
21 discussions

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

Getting Badge Value of a badged EP capability
by Sid Agrawal 22 May '22

22 May '22

Hi seL4-devs and users, I have a question about implementing server and client using badged endpoints. Below I have laid out the scenario, the issue, and some questions. *Scenario* I have a userspace server that implements the functionality for an object(say type obj_T1). The server hands out badged-endpoints to clients to interact with this object. The badge is the virtual address of the object's struct in the server’s virtual address space. A client can interact with the object by sending messages on this badged endpoint. The client never learns the badge value. The kernel extracts the badged value when the server receives a message on this endpoint. By using the badge value, the server knows which object the client is trying to manipulate. The same PD, which implements the 1st server, also implements another server(in a separate thread, but same address space) for another object type (say type obj_T2). The server follows the same paradigm of handing out badged endpoints and using the badges values to keep track of the object. *Issue* I have a scenario where the client wants to invoke the functionality of obj_T1. This functionality needs access to obj_T2 as well. The client has badged EP caps to both objects. The client can invoke the badged EP handed out by server-1 for obj_T1 and give the badged EP of obj_T2 as an extraCap in the IPC message(or vice versa). Since the server has no way to look up the badge of the second cap, it cannot look up the underlying object for obj_T2. So my questions are: 1. Is there a way for a PD to look up the badge value of badged EP? I think the answer is no, but I thought I would still ask. 2. Is my idea of using the badge to keep track of the underlying object on the right track? Is there a better way of going about doing it? 3. As a potential solution, I can extend my server to add a new function, say GETID, which returns the badge value of a given object(i.e., EP). Since I know that the server always badges the EP with the virtual address of the struct, it is a trivial call to implement. But I somehow feel like this is not a neat idea, not quite sure why. Thanks for the help, everyone! Sid CS Graduate Student @ UBC sid-agrawal.ca

3 7

The seL4 Summit 2022 will be in Munich, Germany, on 10-12 Oct 2022
by June Andronick (seL4 Foundation) 29 Apr '22

29 Apr '22

It is our pleasure to confirm that the seL4 Summit 2022 will be in: Munich, Germany in the week of Oct 10th, 2022 It will be hosted by seL4 Foundation member Hensoldt Cyber. It will be a hybrid in-person/online event (if you'd like to propose a talk to be delivered remotely, please notify it in the submission). Remember that you have until Monday 9th of May 2022 to propose a talk. https://sel4.systems/news/2022 https://sel4.systems/Foundation/Summit/ https://sel4.systems/Foundation/Summit/cfp

1 0

Sending extraCaps over IPC | Unable to send 2 caps
by Sid Agrawal 29 Apr '22

29 Apr '22

Hello seL4 devs and users, I am trying to send two capabilities from one process to another via the extraCaps mechanism in the IPC. I can get it working when I send just 1 cap, but when I am sending 2 caps, the 2nd one never makes it. The extraCaps field on the receiver side is somehow always 1. Looking at the seL4 manual, I understood that I could send more than 1 capability via an IPC. But since on the receiver side, I can only specify one receive slot, I assumed that if more than 1 capability is received, it will be put in the consecutive slots. Not sure if this is a valid assumption. Looking at kerne/libsel4/include/sel4/constants.h <https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/constants.h#L…>, I see that seL4_MsgMaxExtraCaps is set to 2, so I think I should be able to send 2 caps. I have spent about 3 days trying to make this work and thought that at this stage, it would be best to ask :) My C code on the sender side looks something like this: seL4_CPtr cap1 = <alloc some capability> seL4_CPtr cap2 = <alloc some capability> seL4_SetMR(0, 0xabcd); seL4_SetCap(0, cap1); seL4_SetCap(1, cap2); seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 2, 1); tag = seL4_Call(receivers_ep_cap, tag); On the receive side, the code looks something like this: /* Allocate one csapce slot */ cspacepath_t received_cap_path_1; error = vka_cspace_alloc_path(simple-vka, &received_cap_path_1); <- slot = 2786 assert(error == 0); /* Allocate another csapce slot */ cspacepath_t received_cap_path_2; error = vka_cspace_alloc_path(simple-vka, &received_cap_path_2); <- slot = 2785(somehow decreasing) assert(error == 0); /* Since the allocated slots are decreasing in count, I pick the lesser one as my first slot * assuming that if more than 1 cap is received it will be put in the next slot */ seL4_CPtr min_cptr = MIN(received_cap_path_1.capPtr, received_cap_path_2.capPtr); seL4_SetCapReceivePath( /* _service */ received_cap_path.root, /* index */ min_cptr, /* depth */ received_cap_path.capDepth); tag = recv(&sender_badge); assert(seL4_MessageInfo_get_extraCaps(tag) == 2); <--- This asser fails. Thanks again!! Sid Graduate Student @ UBC

2 2

RTReply and cap xfer
by Sam Leffler 22 Apr '22

22 Apr '22

The kernel supports attaching a capability to an RTReply xfer. sel4test even checks this WAI. But capdl doesn't seem to support it as I see no way to express the set of rights associated with a capability to an RTReply object. I added capdl support so I can mark the Grant right and verified cap xfer works. TWas this intentional? -Sam

1 0

Running vm_multi app on qemu-arm-virt platform, udhcpc can not return
by ybbekele＠aggies.ncat.edu 22 Apr '22

22 Apr '22

Hi, I tried to build vm_multi for qemu-arm-virt using the procedures in this link https://docs.sel4.systems/projects/camkes-vm/. After building, I used the generated simulation file to do ./simulate in my build directory. After displaying 'welcome to buildroot', the console always prints the log "udhcpc: sending discover",which indicates udhcpc can not return. The related log was shown below: Starting syslogd: OK Starting syslogd: OK Starting syslogd: OK Starting klogd: OK Starting klogd: OK Starting klogd: OK Running sysctl: OK Running sysctl: OK Running sysctl: OK Initializing random number generator... [ 7.195263] random: dd: uninitialized urandom read (512 bytes read) done. Initializing random number generator... [ 7.315113] random: dd: uninitialized urandom read (512 bytes read) done. Initializing random number generator... [ 7.300770] random: dd: uninitialized urandom read (512 bytes read) done. Starting network: OK Starting network: OK Starting network: OK udhcpc: started, v1.31.0 udhcpc: started, v1.31.0 ifconfig: SIOCGIFFLAGS: No such device [ 9.077855] random: mktemp: uninitialized urandom read (6 bytes read) [ 9.177878] random: mktemp: uninitialized urandom read (6 bytes read) Welcome to Buildroot udhcpc: sending discover udhcpc: sending discover udhcpc: sending discover udhcpc: sending discover As the simulation process progresses there was an error: _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0x10080000 alloc_vm_device_cap@main.c:938 Grabbing the entire cap for device memory alloc_vm_device_cap@main.c:941 Failed to grab the entire cap My question is: 1. Is the two things have dependencies (The error and the hang at booting the system up)? 2. How can this issue be solved? 3. Is this issue related to the TimeServer component being imported to Qemu (as this is indicated as a requirement to run multi_vm on qemu-arm-virt)? Thank you for your time

1 0

Why vppi is sent from kernel to vmm by fault endpoint but not by notification ?
by wtliang785 21 Apr '22

21 Apr '22

hello devel, Why vppi , such as vtimer interrupt to guest, is sent from kernel to vmm by fault endpoint but not by notification? I see that spi to guest is sent from kernel to vmm by notification. thank you.

1 0

Reminder seL4 developer hangout/video call
by Gerwin Klein 19 Apr '22

19 Apr '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Apr 19, 10pm (UTC) * Sydney: Wed, Apr 20, 8am * Central Europe: Wed, Apr 20, 12 midnight * US Pacific Time: Tue, Apr 19, 3pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

Re: Combatting spam on this list
by Isaac Beckett 13 Apr '22

13 Apr '22

Thanks Peter! In my experience posts like that, linking to pornographic websites, are not made by humans anyway, but rather by bots. I don’t think this will effect humans too much except at the very beginning. It may make sense to implement a different captcha, as often the developers of those bots can outsource solving common captcha providers to underpaid humans. Using an uncommon or home-grown captcha solution will make it less likely that bots will be able to get around them using that method. And attacks like these aren’t targeted, usually, so I doubt the bot writers will adapt for one specific mailing list. That will stop bots from signing up in the first place, hopefully. We could also maybe report abuse of free email services like Gmail or Hotmail or similar in a semi-automated fashion. Would not surprise me if there is some sort of API for that. But on the other hand with the way those companies work it could be a waste of time and effort, since they might not do anything. And it may also make sense to keep track of which domains non-malicious users are sending email from. That way we can ban entire domains without worrying about getting rid of legitimate users unintentionally. For example, a small webmail service that we may not realize is a public email service at first, could be used by both a malicious user and a legitimate one. That way we’re only banning domains controlled by spammers exclusively. There’s lots of resources for this stuff thankfully, you can go on a whole tangent reading about email spam prevention on Wikipedia. I wish you luck with figuring out how to stop this annoying nonsense.

3 2

Unrecognized OPCODE fence.i/csrw
by porter.188＠osu.edu 13 Apr '22

13 Apr '22

I'm trying to setup a development machine for seL4 work. I would like to use v12.1.0. I setup seL4test-manifest per instructions here https://docs.sel4.systems/Hardware/spike.html repo init -u https://github.com/seL4/sel4test-manifest.git repo sync mkdir cbuild cd cbuild ../init-build.sh -DPLATFORM=spike -DRISCV64=1 # The default cmake wrapper sets up a default configuration for the target platform. # To change individual settings, run `ccmake` and change the configuration # parameters to suit your needs. ninja # If your target binaries can be executed in an emulator/simulator, and if # our build system happens to support that target emulator, then this script # might work for you: ./simulate I used repo init -u https://github.com/seL4/sel4test-manifest.git -b refs/tags/12.1.0 to be sure I got 12.1.0 but it doesn't matter, both branches/tags give the same error when I configure/compile. $ ../init-build.sh -DPLATFORM=spike -DRISCV64=1 -DSIMULATION=1 loading initial cache file /mnt/data/sel4test/projects/sel4test/settings.cmake -- Set platform details from PLATFORM=spike -- KernelPlatform: spike -- Setting from flags KernelSel4Arch: riscv64 -- Found seL4: /mnt/data/sel4test/kernel -- Found GCC with prefix riscv64-unknown-linux-gnu- -- Found GCC with prefix riscv64-unknown-linux-gnu- -- The C compiler identification is GNU 10.2.0 -- The CXX compiler identification is GNU 10.2.0 -- The ASM compiler identification is GNU -- Found assembler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc - skipped -- Detecting C compile features -- Detecting C compile features - done -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-g++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- Found elfloader-tool: /mnt/data/sel4test/tools/seL4/elfloader-tool -- /mnt/data/sel4test/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... -- CPIO test cpio_reproducible_flag PASSED -- Found musllibc: /mnt/data/sel4test/projects/musllibc -- Found util_libs: /mnt/data/sel4test/projects/util_libs -- Found seL4_libs: /mnt/data/sel4test/projects/seL4_libs -- Found sel4_projects_libs: /mnt/data/sel4test/projects/sel4_projects_libs -- Found sel4runtime: /mnt/data/sel4test/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- libmuslc architecture: 'riscv' (from KernelSel4Arch 'riscv64') -- Detecting cached version of: musllibc -- Found Git: /usr/bin/git (found version "2.25.1") -- Not found cache entry for musllibc - will build from source -- Found PythonInterp: /usr/bin/python (found version "2.7.18") CMake Warning (dev) at /home/user/.local/lib/python3.8/site-packages/cmake/data/share/cmake-3.22/Modules/FindPackageHandleStandardArgs.cmake:438 (message): The package name passed to `find_package_handle_standard_args` (NANOPB) does not match the name of the calling package (Nanopb). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): /mnt/data/sel4test/tools/nanopb/extra/FindNanopb.cmake:340 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) /mnt/data/sel4test/tools/seL4/cmake-tool/helpers/nanopb.cmake:29 (find_package) /mnt/data/sel4test/projects/sel4_projects_libs/libsel4nanopb/CMakeLists.txt:11 (include) This warning is for project developers. Use -Wno-dev to suppress it. -- Found NANOPB: /mnt/data/sel4test/tools/nanopb -- Configuring done -- Generating done -- Build files have been written to: /mnt/data/sel4test/build user@user-KVM:/mnt/data/sel4test/build$ ninja [42/267] Building ASM object kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj FAILED: kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj /usr/bin/ccache /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc --sysroot=/mnt/data/sel4test/build -I/mnt/data/sel4test/kernel/include/plat/default -I/mnt/data/sel4test/kernel/include -I/mnt/data/sel4test/kernel/include/64 -I/mnt/data/sel4test/kernel/include/arch/riscv -I/mnt/data/sel4test/kernel/include/arch/riscv/arch/64 -I/mnt/data/sel4test/kernel/include/plat/spike -I/mnt/data/sel4test/kernel/include/plat/spike/plat/64 -I/mnt/data/sel4test/kernel/libsel4/include -I/mnt/data/sel4test/kernel/libsel4/arch_include/riscv -I/mnt/data/sel4test/kernel/libsel4/sel4_arch_include/riscv64 -I/mnt/data/sel4test/kernel/libsel4/sel4_plat_include/spike -I/mnt/data/sel4test/kernel/libsel4/mode_include/64 -I/mnt/data/sel4test/build/kernel/gen_config -I/mnt/data/sel4test/build/kernel/autoconf -I/mnt/data/sel4test/build/kernel/gen_headers -I/mnt/data/sel4test/build/kernel/generated -march=rv64imac -mabi=lp64 -D__KERNEL_64__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=medany -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -MD -MT kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj -MF kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj.d -o kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj -c /mnt/data/sel4test/kernel/src/arch/riscv/head.S /mnt/data/sel4test/kernel/src/arch/riscv/head.S: Assembler messages: /mnt/data/sel4test/kernel/src/arch/riscv/head.S:24: Error: unrecognized opcode `fence.i' /mnt/data/sel4test/kernel/src/arch/riscv/head.S:31: Error: unrecognized opcode `csrw sscratch,x0' [44/267] Invoking muslc build system /mnt/data/sel4test/projects/musllibc/src/unistd/getcwd.c: In function 'getcwd': cc1: warning: function may return address of local variable [-Wreturn-local-addr] /mnt/data/sel4test/projects/musllibc/src/unistd/getcwd.c:9:7: note: declared here 9 | char tmp[PATH_MAX]; | ^~~ ninja: build stopped: subcommand failed. I tried riscv-gcc 10.2.0 and 11.1.0 with the same results. $ riscv64-unknown-linux-gnu-gcc --version riscv64-unknown-linux-gnu-gcc (gca312387ab1) 10.2.0 Copyright (C) 2020 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. Is there some extension I need to add to get this working? Where do I do that?

2 2

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel April 2022