- Devel - lists.sel4.systems

Building a simple RISC-V project
by porter.188＠osu.edu 30 Nov '20

30 Nov '20

I am trying to build a simple RISC-V seL4 project. I mean "hello world" simple. I using version 12.0.0. I looked at the documentation here https://docs.sel4.systems/projects/buildsystem/incorporating.html to follow what the project layout is. I also followed this project for x86 v10.0.0. https://github.com/manu88/SeL4_101 I was able rebuild this last one for RISC-V after modifying the CMakeLists.txt to include the proper libraries in my hello project. When I try to use the seL4 12.0.0 kernel there are some configuration differences that I haven't figured out yet. Can anyone shed some light on what the parameters are that need to be set for RISC-V? The verified config in ../kernel/configs/RISCV64_verified.cmake are this, is this all that need set? I suppose these could be modified as necessary. 12 set(KernelSel4Arch "riscv64" CACHE STRING "") 13 set(KernelPlatform "hifive" CACHE STRING "") 14 set(KernelPTLevels "3" CACHE STRING "") 15 set(KernelVerificationBuild ON CACHE BOOL "") 16 set(KernelMaxNumNodes "1" CACHE STRING "") 17 set(KernelOptimisation "-O2" CACHE STRING "") 18 set(KernelRetypeFanOutLimit "256" CACHE STRING "") 19 set(KernelBenchmarks "none" CACHE STRING "") 20 set(KernelDangerousCodeInjection OFF CACHE BOOL "") 21 set(KernelFastpath ON CACHE BOOL "") 22 set(KernelPrinting OFF CACHE BOOL "") 23 set(KernelNumDomains 16 CACHE STRING "") 24 set(KernelMaxNumBootinfoUntypedCap 166 CACHE STRING "") 25 set(KernelRootCNodeSizeBits 19 CACHE STRING "") 26 set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")

2 1

CAmKes Ethdriver Odroid-C2
by Nkem Ogosi 26 Nov '20

26 Nov '20

Hi all, I'm trying to add an odroid-c2 ethdriver implementation and I'm quite confused bout an error im getting. ERROR:CAmkES:CPP failed: /home/nkem/learningHydra/projects/global-components/components/Ethdriver/Ethdriver.camkes:13:10: fatal error: plat/eth_devices.h: No such file or directory ERROR:CAmkES: #include <plat/eth_devices.h> ERROR:CAmkES: ^~~~~~~~~~~~~~~~~~~~ ERROR:CAmkES:compilation terminated. ERROR:CAmkES: CMake Error at /home/nkem/learningHydra/projects/camkes-tool/camkes.cmake:545 (message): Failed to generate /home/nkem/learningHydra/build/ast.pickle Call Stack (most recent call first): It suggests I'm missing the eth_devices header for the odroid-c2 platform but I think I have added all the necessary files in the correct folders. Is there any way to know exactly what files I need or where to look to debug this issue. Thanks, Nkem

2 1

Re: Quotation
by Chubb, Peter (Data61, Kensington NSW) 25 Nov '20

25 Nov '20

>>>>> "Andrew" == Andrew Warkentin <andreww591(a)gmail.com> writes: Andrew> How are these spammers getting onto the list? Is there some Andrew> kind of configuration issue? The person sending it subscribed then unsubscribed. I've temporarily set all messages to moderated to try to catch any others who are doing this. PeterC -- Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group CSIRO's Data61

1 0

Connectivity of 2 sel4 powered systems
by ogosinkem＠gmail.com 24 Nov '20

24 Nov '20

Hi all, I asked earlier about how to connect the odroid-c2 board via Ethernet and I was wondering what additional files I would need to get a CAmkES implementation of an ethernet driver working for this board. Thanks, Nkem Ogosi

1 0

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 20 Nov '20

20 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