- Devel - lists.sel4.systems

Possibility of adding a system call origin limit similar to that of OpenBSD?
by Andrew Warkentin 23 Nov '20

23 Nov '20

I am wanting to implement a system call origin limit (akin to that of OpenBSD) in UX/RT. This could probably be accomplished by adding a "set system call range" TCB method that takes the start and end addresses of the range in which system calls will be permitted without interception. Any system call issued from code outside this range would incur a user exception (which would provide all the state required for user code to handle the system call and resume the thread if desired). UX/RT will require all binaries to be dynamically linked with a minimal "libroot" library that will contain an IPC transport layer that will be the only part of the system outside the root server that makes direct system calls. This will make it easier for later versions to retain backwards compatibility. Limiting system call origin should also make certain kinds of attacks more difficult. I am also planning to use the system call origin limit in the Linux compatibility environment in order to distinguish Linux syscalls from seL4 ones, since Linux syscalls will never come from libroot. Each process in the Linux compatibility environment will have a fault handler thread that looks up the syscall and calls the corresponding UX/RT APIs, and will also replace the trap with a call to a jump table if the function containing it is a known syscall wrapper in order to cut down on the number of trips through the kernel. Would it be possible to add something like this to the mainline seL4 tree?

4 7

Proposed future Core Platform extension: hosting other seL4-native OSs
by Demi M. Obenour 23 Nov '20

23 Nov '20

While reading Andrew’s message on syscall origin checking, I realized that UX/RT could potentially replace Linux VMs in Core Platform applications. I imagine that this would require changes to both the Core Platform and UX/RT. Andrew, would you be interested in adding a hosting interface to UX/RT, so that static systems such as the Core Platform can use UX/RT as a Linux VM replacement? UX/RT seems like a fantastic alternative, with both better security and (eventually) better performance. I would imagine that it also would use less memory than a Linux VM. Gernot (and the rest of the seL4 team): would it be possible to support running other seL4-based systems as protection domains in a future version of the Core Platform? Such systems would be opaque from the Core Platform’s perspective, but they might need capabilities that normal protection domains are not provided. Of course, they would not be granted any capabilities that would allow them to violate system security. Yes, I know that one can run seL4 in a VM, but it seems rather wasteful to do so. Sincerely, Demi

3 2

RFC-5: seL4 Core Platform
by Gernot Heiser 23 Nov '20

23 Nov '20

Dear seL4 Community, Those who attended today’s closing session at the seL4 Summit have heard about this, for the rest I’m pleased to announce that we have an RFC out for the seL4 Core Platform, a minimal seL4-based OS for embedded/cyberphysical/IoT applications, see https://sel4.atlassian.net/browse/RFC-5 Feedback welcome. Gernot

6 16

Issues with PR
by Iker Galardi 22 Nov '20

22 Nov '20

Hi! I'm having certain issues with the PR where I propose another way to get the gic cpu id directly from hardware registers instead of guessing like before. First of all, inside CI/Links some errors appear about sel4 webpage links that I haven't touched, how can I solve this? At last, on the PR/Preprocess test failure appears but it's not clear what the problem is and after the compilation test is successful. Thanks for your time. Sincerely, Iker Galardi.

3 4

RCF-6: seL4 Core
by Gernot Heiser 22 Nov '20

22 Nov '20

Dear seL4 Community, There is a second RFC just released, for the seL4 Core, a policy-free runtime and build environment for “plain” seL4, see https://sel4.atlassian.net/browse/RFC-6 Again, we are looking for feedback. Gernot

3 2

QEMU vs Spike on RISC-V Debugging
by Porter, Jeremy 19 Nov '20

19 Nov '20

I've built a simple hello for RISC-V. It runs in Spike as expected. In QEMU it doesn't run. It stops at loading the kernel in elfloader/src/common.c at the lines below: 199 printf("ELF-loading 199\n"); 200 /* Copy the data. */ 201 unpack_elf_to_paddr(elf, dest_paddr); I'd really like to use QEMU/GDB to debug my kernel. Can anyone shed some light on what's happening here? The failed output from QEMU looks like this: user@user-KVM:/mnt/data/femur/build$ qemu-system-riscv64 --machine spike --nographic --bios images/hello-image-riscv-spike bbl loader ELF-loader started on paddr=[80200000..802fb90f] ELF-loading image 'kernel' paddr=[c0000000..c0026fff] vaddr=[ffffffff80000000..ffffffff80026fff] virt_entry=ffffffff80000000 ELF-loading 187 ELF-loading 195 ELF-loading 199 The output from spike is the same but complete: ser@user-KVM:/mnt/data/femur/build$ /mnt/data/rocket-tools/bin/spike images/hello-image-riscv-spike bbl loader ELF-loader started on paddr=[80200000..802fb90f] ELF-loading image 'kernel' paddr=[c0000000..c0026fff] vaddr=[ffffffff80000000..ffffffff80026fff] virt_entry=ffffffff80000000 ELF-loading 187 ELF-loading 195 ELF-loading 199 ELF-loading 203 ELF-loading 211 ELF-loading image 'hello' paddr=[c0027000..c013afff] vaddr=[10000..123fff] virt_entry=10216 ELF-loading 187 ELF-loading 195 ELF-loading 199 ELF-loading 203 ELF-loading 211 Jumping to kernel-image entry point... Booting all finished, dropped to user space hello, world! Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() hrintf is bac seL4 root server abort()ed Debug halt syscall from user thread 0xffffffc0bffd8a00 "rootserver" halting...Power off

3 4

Re: [seL4] Simple hello for RISC-V/spike
by Porter, Jeremy 10 Nov '20

10 Nov '20

Answering my own question here--maybe this will help someone else trying to get this kind of setup running. The problem is that there are additional libraries required. The CMakeLists.txt for the hello project looks like this: cmake_minimum_required(VERSION 3.7.2) project(hello C) # create a new C project called 'Hello' add_executable(hello src/main.c) # add files to our project. Paths are relative to this file. target_link_libraries(hello sel4platsupport sel4muslcsys ) # we need to link against the standard C lib for printf # Set this image as the rootserver DeclareRootserver(hello) ---------------------------------- This works for the debug build. For the release build there is a dependency on some debugging for early print functions. I think if those are removed it might work ok.

1 0

Odroid-C2 help
by ogosinkem＠gmail.com 06 Nov '20

06 Nov '20

Hi, Ive been following all the steps at https://www.cse.unsw.edu.au/~cs9242/19/project/linux.shtml and I'm not too clear on how to put a built image on the board. Or even if I've done the whole setup correctly for that matter. Any tips would be appriecated? Thanks, Nkem Ogosi

1 0

How is CMake told to build a given app.
by Chris Koziarz 06 Nov '20

06 Nov '20

I'm setting up a new application (and the libraries coming with it) but I have hard time figuring out the process of building, esp. how CMake knows where to start building from.. By way of example, I'm trying to follow the process of setting up and building sel4test. Setting up the source dir structure: repo init -u https://github.com/seL4/sel4test-manifest.git & repo sync and creating the build dir md build & cd build Are perfectly understandable steps: create source tree that includes the app sources (./projects/sel4test/apps/sel4test-driver/ in this case) kernel (./kernel/) libraries (other subdirs under ./projects/) and misc tools (./tools/) and an extra subdir for build output The third "magic" CMake setup step ../init-build.sh -DPLATFORM=<platform> -DRELEASE=FALSE -DSIMULATION=TRUE enables a simple "ninja" command (without any params) to build an application from the sources at ./projects/sel4test/apps/sel4test-driver/ This is a mystery to me. Where is the target (sel4test-driver) specification in these steps? I looked into init-build.sh and my understanding is the CMake setup must be carried by this command: cmake -G Ninja "$@" -DSEL4_CACHE_DIR="$CACHE_DIR" -C "$project_dir/settings.cmake" "$project_dir" but I cannot figure how said command finds that the application we are trying to build is located in ./projects/sel4test/apps/sel4test-driver/ Now, when I try to setup my own app, how do I tell init-build.sh command where my app is? Thanks for any clarification, Chris

2 1

what does "#include <autoconf.h>" do and how to set the path to include it ?
by Chris Koziarz 05 Nov '20

05 Nov '20

I'm creating a new project that uses existing libraries, e.g. seL4_libs/libsel4utils, a header page_dma.h, because I want to use dma in my IO transfer. When I include header page_dma.h in question, at line 15, <autoconf.h> is pulled in. There are 100s of autoconf.h files (usually auto-generated ones in kernel binaries) and I have no idea which one should be included and how to setup -I option for gcc to include it. Can anyone educate me on it? Thanks very much! Chris ninja output: [1/9] Building C object apps/sel4test-driver/fat32-sel4/CMakeFiles/fat32-sel4.dir/src/interfaces/sel4.c.obj FAILED: apps/sel4test-driver/fat32-sel4/CMakeFiles/fat32-sel4.dir/src/interfaces/sel4.c.obj /usr/bin/ccache /usr/bin/aarch64-linux-gnu-gcc --sysroot=/home/chris/sel4_test/tqma8xqp_build -I/home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/inc -I/home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/config -I/home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/../../../sel4_projects_libs/libsdhcdrivers/include/sdhc -I/home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/../../../util_libs/libplatsupport/include -I/home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/../../../util_libs/libutils/include -Iapps/sel4test-driver/musllibc/build-temp/stage/include -march=armv8-a -D__KERNEL_64__ -g -nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mstrict-align -std=gnu11 -MD -MT apps/sel4test-driver/fat32-sel4/CMakeFiles/fat32-sel4.dir/src/interfaces/sel4.c.obj -MF apps/sel4test-driver/fat32-sel4/CMakeFiles/fat32-sel4.dir/src/interfaces/sel4.c.obj.d -o apps/sel4test-driver/fat32-sel4/CMakeFiles/fat32-sel4.dir/src/interfaces/sel4.c.obj -c /home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/src/interfaces/sel4.c In file included from /home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/src/interfaces/sel4.c:12: /home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/src/interfaces/../../../../../seL4_libs/libsel4utils/include/sel4utils/page_dma.h:15:10: fatal error: autoconf.h: No such file or directory 15 | #include <autoconf.h>

2 2