Devel June 2022

devel@sel4.systems

17 participants
22 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

Anyone using capability transfer in an seL4 project? Looking for examples for research
by sjwebb＠student.unimelb.edu.au 12 Jul '22

12 Jul '22

Hi all, I'm working on a Masters research project looking into mapping an object-capability programming language onto seL4, in a way that includes some kind of mapping from the language object capabilities onto seL4's capabilities (or vice versa). I'm at a stage of the project now where it would be really helpful to have some 'motivating examples' for transferring caps between threads/CSpaces. So I was hoping I could reach out to other seL4 developers to see if they had built any systems that made extensive use of moving capabilities around. Ideally, in an ocap language, these examples would be much easier to program than they currently would be in C... The simplest example I can think of is a memory allocation server, but that wouldn't necessarily involve handing caps on beyond the one (requesting) process, which is the kind of thing I think more interesting examples would comprise of. Cheers, Stewart Webb [Masters Research student at University of Melbourne]

2 2

Camkes Cross VM Tutorial
by Sriram 30 Jun '22

30 Jun '22

Greetings, I have been trying to build Camkes Cross VM tutorial but it fails at the end, similarily when we boot Camkes VM Linux, We were not able to input anything from the keyboard and the Serial Output is as follows """ Starting network[ 0.810972] ip (679) used greatest stack depth: 6732 bytes left : OK Failed to locate device consumes_event. Failed to locate device emits_event. Welcome to Buildroot buildroot login: [ 1.431752] clocksource: tsc: mask: 0xffffffffffffffff max_cycles: 0x31015f85297, max_idle_ns: 440795334135 ns [ 1.442241] clocksource: Switched to clocksource tsc [ 2.811817] random: fast init done [ 134.023597] random: crng init done """" Is there any changes to be made in the source files or any other modifications And are there any pre-built images for x86_64 for easier implementation Keenly Awaiting for your Reply Thanks and Regards R.Sriram

1 0

Some questions about porting seL4 to CHERI(Morello)
by Sid Agrawal 29 Jun '22

29 Jun '22

Hi sel4-devs, As I had mentioned in the last developer call, I am porting seL4 to morello architecture. To be exact, I plan to run a hybrid kernel with hybrid userspace. The hybrid mode essentially means that you define CHERI capability pointers explicitly, but if not stated, everything is just a standard 64bit pointer. Based on browsing the code, I have jotted down the following list of items I need to change. 1,2 are just observations, and 3 is where I need some input. 1. Change the type of "registers" field in TCB in the kernel to store 128 bits instead of 64 bits per reg. This ties into the kernel_enter and restore_user_context code. It ensures that if a user app explicitly uses CHERI capabilities, it is not lost on a context switch.[1,2] - Done. 2. Change the syscall and IPC APIs to allow for passing CHERI caps. CHERIcaps are just 128 bits, so we should be able to pass them as arguments in IPC. The use case I have in mind is as follows - Imagine a mmap server. This server would return a VA to the caller, which in the CHERI world would be a CHERI capability. This mmap-server would allocate the memory and map it into the callee's virtual address space. Do you think this is a valid use case? 3. Update seL4_UserContext code to read and write newer regs from the user space. The seL4_UserContext struct will need to be updated to accommodate the new register DDC(default data capability reg). It will also need to be updated to accommodate 128 bit regs instead of 64 bits. This is where I ran into an issue - an assert statement in the build directory checks the size of the seL4_UserContext structure. Looks like it gets its info from the sel4arch.xml file[4]. I am not sure how to change XML processing to have it generate the correct size value for that struct. I have not created ifdef guard for morello yet, as this is just a hacky pass to get it working. My diff so far is available at [3] if anyone wants to take a look. Any help and suggestions on the approach would be greatly appreciated. Thanks, Sid [1] https://gitlab.com/arm-research/security/icecap/seL4/-/blob/morello/include… [2] https://gitlab.com/arm-research/security/icecap/seL4/-/blob/morello/include… [3] https://gitlab.com/arm-research/security/icecap/seL4/-/compare/pre-morello-… [4] https://gitlab.com/arm-research/security/icecap/seL4/-/blob/morello/libsel4…

1 0

SMP documents
by 603644559＠qq.com 23 Jun '22

23 Jun '22

I mainly want to know how threads is scheduled in SMP configuration. Is there any documents or manuals on SMP configuration?

2 1

Details on involvement of Data61/Trustworthy Systems with DARPA, esp. regarding UAVs?
by Isaac Beckett 23 Jun '22

23 Jun '22

Hello, in your answer about camkes VMs, you mentioned a collaboration with DARPA on their SMACCM/HACMS project. While seL4 is undoubtedly a good choice for mixed criticality systems like avionics on a UAV, I’m somewhat frustrated to hear y’all had done a contract for DARPA considering what they *use* those drones to do. Is there somewhere I can read more in detail about this and other military-adjacent contracts?

2 1

SeL4 Tutorial - Camkes CrossVM
by Sriram 22 Jun '22

22 Jun '22

Greetings, We have followed step by step and tried the CAMKES Linux VM tutorial, We have build it successfully but while booting via USB flash drive The Serial Output Stops after root Login and doesn't take any input SERIAL OUTPUT """ Starting network[ 0.810972] ip (679) used greatest stack depth: 6732 bytes left : OK Failed to locate device consumes_event. Failed to locate device emits_event. Welcome to Buildroot buildroot login: [ 1.431752] clocksource: tsc: mask: 0xffffffffffffffff max_cycles: 0x31015f85297, max_idle_ns: 440795334135 ns [ 1.442241] clocksource: Switched to clocksource tsc [ 2.811817] random: fast init done [ 134.023597] random: crng init done """" This is the serial output we got Is there any modifications of the source code required to make it work if so kindly provide the necessary details. Thanks and Regards R.Sriram

1 0

How can I ensure the security of a system developed by Camkes?
by Comet 22 Jun '22

22 Jun '22

Hi, I am using Camkes to develop VM virtualization, but I have a question that is how can I ensure isolation security between virtual machines? If a virus with a Trojan is installed on the VMM, will the virtual machines attack each other? and will the kernel be corrupted ? I didn't find some security instructions about the system developed by Camkes, or the implementation principle of Camkes, that is, how is resource mapping between seL4 and Camkes? Are there any related articles? Thanks, Comet959

2 1

SeL4 Source Code Documentation
by Sriram 20 Jun '22

20 Jun '22

Greetings, We are trying to understand the SeL4 Source Code, is there any documentation available that explains the source code and libraries Thanks and Regards R.Sriram

2 2

Re: SeL4 Source Code Documentation
by Isaac Beckett 20 Jun '22

20 Jun '22

Are those Haskell sources used to generate the C code, or are they an older version of the spec, or something? This is my first time hearing of them, so not sure what they’re used for.

3 2

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel June 2022