November 2020 - Devel - lists.sel4.systems

by Chris Koziarz

Hi all, I'm trying to port camkes-arm-vm to a different platform, that supports gic-v3 In the process, I hit a compilation error: Building C object kernel/CMakeFiles/kernel_all_pp_...rapper_temp_lib.dir/ kernel_all_pp_prune_wrapper_temp.c.obj FAILED: kernel/kernel_all_pp_prune_wrapper_temp.c In file included from /home/chris/camkes-tqma8xqp- vm/kernel/src/arch/arm/object/vcpu.c:15: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v2.h:23: error: "IRQ_MASK" redefined [-Werror] 23 #define IRQ_MASK MASK(10u) In file included from kernel/gen_headers/plat/platform_gen.h:23, from /home/chris/camkes-tqma8xqp-vm/kernel/include/plat/ default/plat/machine.h:8, from /home/chris/camkes-tqma8xqp- vm/kernel/include/machine.h:9, from /home/chris/camkes-tqma8xqp- vm/kernel/include/api/syscall.h:10, from /home/chris/camkes-tqma8xqp- vm/kernel/src/api/faults.c:10: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v3.h:30: note: this is the location of the previous definition 30 #define IRQ_MASK MASK(16u) which is an indicative that both gic_v3.h & gic_v2.h headers have been included, which is an error because said headers are not compatible: kernel/include/arch/arm/arch/machine/gic_v3.h:#define IRQ_MASK MASK(16u) kernel/include/arch/arm/arch/machine/gic_v2.h:#define IRQ_MASK MASK(10u) So my question is: how can I configure the build to avoid such a conflict? I can grepp the relevant configuration option in CMakeCache.txt: build_tqma8/CMakeCache.txt:CONFIGURE_INTERRUPT_CONTROLLER:INTERNAL=arch/machine/gic_v3.h but cannot see it in ccmake gui because it's "INTERNAL" What is the solution? - replace this option somehow to use gic_v2 and have my HW use gic v.2, or - change compilation options to use gic_v3 everywhere Thanks for any help, Chris.

11 months, 3 weeks

4
5
0 0

hello_rumprun app not worked

by MOHAMAD REZA SHAFIEI

hi. i'm recently worked on sel4 with camkes framework. when i compile rumprun_hello on x86_64 platform its compiled and build correctly but when run with qemu by ./simulate script, program crashed with this errors: simple_get_extended_bootinfo_length@simple.h:600 simple_get_extended_bootinfo_length not implemented FAULT HANDLER: data fault from hello.hello_0_control (ID 0x1) on address 0x8, pc = 0x402b7f, fsr = 0x6 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x402b7f , . . so i found that this method not implemented yet so i return 0 in this method and resolved. for second problem that cause failure if trace program and i found that in "init rumprun" process the program failed in the /projects/sel4runtime/include/sel4_arch/x86_64/sel4runtime/thread_arch.h file and sel4runtime_set_tls_base method. so i read git log and in recently commit your team use sel4runtime for thread TLS, so when we run rumprun_hello, the program failed in sel4runtime_set_tls_base method. can you help me fix this bug? thanks for your attention. -- This email was Anti Virus checked by Security Gateway.

1 year

4
4
0 0

whether seL4 support c++ code

by yadong.li

Hi， I have two questions about whether seL4 support C++: 1. When we create a component, whether the src file of component can be c++ style file like **.cxx, or **.cpp ? I found it will print “camkes.environment.c : undefined reference to run” error when compile 2. If our app code write by c++, how can I use it in seL4 environment as native component？Is there some example ？ Thank you very much.

1 year, 6 months

3
2
0 0

Building a simple RISC-V project

by porter.188＠osu.edu

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 "")

1 year, 7 months

2
1
1 0

CAmKes Ethdriver Odroid-C2

by Nkem Ogosi

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

1 year, 7 months

2
1
0 0

Re: Quotation

by Chubb, Peter (Data61, Kensington NSW)

>>>>> "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 year, 7 months

1
0
0 0

Connectivity of 2 sel4 powered systems

by ogosinkem＠gmail.com

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 year, 7 months

1
0
0 0

Possibility of adding a system call origin limit similar to that of OpenBSD?

by Andrew Warkentin

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?

1 year, 7 months

4
7
0 0

Proposed future Core Platform extension: hosting other seL4-native OSs

by Demi M. Obenour

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

1 year, 7 months

3
2
0 0

RFC-5: seL4 Core Platform

by Gernot Heiser

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

1 year, 7 months

6
16
0 0

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel November 2020