- Devel - lists.sel4.systems

[Camkes] Access control for memory or the entire component?
by Seo Yeon Hwang 11 Dec '20

11 Dec '20

Hello all, I wonder if it is possible for a component to directly access some specific part of memory with an address or access the whole component (not some dataports) using Camkes. I can see how to set up the permissions (R/W) for each dataport in the tutorial #port_privileges part, but I wonder if one component can read some specific memory region with starting and ending addresses, or read the whole memory where another component is located. Thanks for your help! Best regards, Seoyeon

2 1

CfP: FOSDEM 2021 - Microkernel Devroom
by Martin Decky 08 Dec '20

08 Dec '20

Microkernel Devroom at FOSDEM 2021 CALL FOR PARTICIPATION On-line version of this CfP: http://fosdem.microkernel.info/ The developers and users of several free and open source microkernel-based operating systems will meet on-line as part of FOSDEM 2021 [1] and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-based, unikernel-based, component-based operating systems and similar topics. The devroom has been preliminarily scheduled to Saturday February 6th 2021. The devroom will take place during European day hours. Possible topics of the devroom include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * used languages, tools and toolchains * enabling support for hardware (architectures, device drivers) * enabling support for programming languages * development processes, debugging * maintenance, testing and release engineering * security and robustness * trends and challenges * community and governance * use cases, experiences and status updates * best practices, lessons learned and demos This is a call for your participation. We kindly ask you to submit your proposals no later than on December 26th 2020. Please use the Pentabarf website [2] to submit your proposals. If you already have a user account in Pentabarf, please do not create a new one. Please make sure to select the Microkernel devroom as the track when submitting your talk and include at least the following information in your proposal: * title of your talk * your full name * short abstract of your talk (one or two paragraphs) * duration of your talk (at least 20 minutes and no longer than 50 minutes), excluding a Q&A part * your short bio * your photo The talks will be pre-recorded in advance in January and streamed during the event. This means that you will need to complete and submit your talk by around mid January. However, each speaker should be also present on-line just after the streaming of the talk for a live Q&A. You can specify your prefered time slot of your talk. The communication language of the devroom is English. The official devroom schedule (along with the accepted talks) will be announced on December 31st 2020 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM website. You are also invited to send any other suggestions for what you want to see or do at the devroom to the mailing list. About the Devroom Since the first Microkernel devroom at FOSDEM 2012 [4], this devroom has been part of each following FOSDEM. The focus gradually widened to include component-based and unikernel-based operating systems. By now it has become a somewhat institutionalized tradition for the community to meet there. To this date, over a dozen projects have participated in one way or another. Each of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Extraordinary Circumstances in 2021 Due to the extraordinary mode of organization of FOSDEM 2021 (being an on-line event for the first time), many practical aspects of the devroom are still in the process of determination. For example, the devroom talks will be required to be pre-recorded in January and streamed during the event (with a live Q&A), but the technical details are still sketchy at this moment. The talk videos will be published under Creative Commons license by FOSDEM. By submitting a recorded talk, the speaker agrees to have it made available publicly indefinitively. For organizational purposes, we also need contact information of the speakers of accepted talks. Please check the official CfP page [5] of our devroom regularly. We will keep updating it as new guidelines will be determined by the FOSDEM organizers. Sadly, it will not be possible to arrange our traditional microkernel dinner and other in-person social gatherings in Brussels this time. However, we plan to organize an on-line replacement. The details will be announced later in January. On the other hand, the on-line nature of the devroom allows us to "overflow" to a second day in case we receive a substatial number of quality proposals. About FOSDEM FOSDEM [6] is a two-day event organised by volunteers to promote the widespread use of free and open source software. FOSDEM is widely recognised as one of the best such conferences worldwide. FOSDEM covers a wide spectrum of free and open source software and hardware projects and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and proposals. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, and in the past instances certification exams and project stands. In recent years, FOSDEM has been hosting more than 5000 developers at the ULB Solbosch campus. Due to the circumstances, FOSDEM 2021 will be organized as an on-line event. Despite this, the participation in FOSDEM is still totally free, although the organisers gratefully accept donations and sponsorship. No registration is necessary, but attendees are expected to follow the FOSDEM's code of conduct [7]. Important Dates Recap * 2020-12-26: Deadline for talk proposal submission * 2020-12-31: Schedule published and speakers notified of acceptance * mid January 2021: Time frame for talk pre-recoding * 2021-02-06: Devroom taking place on-line Contact In case of any questions, comments and suggestions, please do not hesitate to contact the devroom organizers via the devroom's mailing list [3]. The primary organizers of the devroom in 2021 are: * Martin Decky * Jakub Jermar Links [1] https://fosdem.org/2021/ [2] https://penta.fosdem.org/submission/FOSDEM21/ [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://archive.fosdem.org/2012/schedule/track/microkernel_os_devroom.html [5] http://fosdem.microkernel.info/ [6] https://fosdem.org/ [7] https://fosdem.org/2021/practical/conduct/

1 0

More enhancements for general-purpose systems that wouldn't be accepted into seL4?
by Andrew Warkentin 06 Dec '20

06 Dec '20

Am I correct to assume that support for running 32-bit code on a 64-bit kernel using compatibility mode rather than virtualization and support for (presumably limited) direct system calls from VMs, bypassing any user-mode VMM (using something like Xen's trampoline page) wouldn't be accepted into seL4? These are yet more things that I am going to want at some point and can't think of any other way to do them (besides adding them to the kernel) without significant penalties to hardware compatibility (in the case of the 32-bit support; while UX/RT will mostly be focused on 64-bit systems, it will support 32-bit Linux programs in its compatibility layer) or performance (in the case of direct kernel traps from VMs; I am planning to write a dynamic general-purpose hypervisor to go with UX/RT eventually, and adding an extra trap into the VMM on every IPC would likely add a fair bit of overhead).

4 8

whether seL4 support c++ code
by yadong.li 03 Dec '20

03 Dec '20

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.

3 2

repo move from sel4proj to sel4 on github
by Klein, Gerwin (Data61, Kensington NSW) 01 Dec '20

01 Dec '20

As some may have already noticed, we have moved a few repositories from github.com/sel4proj/ to github.com/seL4/ recently, This is part of the hand-over of these repositories to the seL4 foundation. Github will forward all related URLs and git operations etc, so there is nothing really that you need to do, and old manifests and repo collections should continue to work as before. For those who would still like to update their mirrors or own manifests to avoid the redirect, below the list of repos that were moved: sel4-tutorials-manifest polyml seL4-CAmkES-L4v-dockerfiles camkes-arm-vm-manifest sel4webserver-manifest rumprun-sel4-demoapps camkes-vm-linux riscv-pk camkes-arm-vm cakeml_libs rumprun-packages seL4_projects_libs sel4-tutorials global-components camkes-vm-images projects_libs sel4webserver sel4runtime rumprun HOL camkes-vm-apps mcs-examples-manifest mcs-examples picotcp picotcp-bsd Cheers, Gerwin

1 0

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