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]
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
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…
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?
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
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
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
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.
We’re currently working on formalising VM support for an iMX8 platform (the Avnet MaaXBoard) building upon the existing sylvain/imx8 and sylvain/gicv3 branches.
However on start of the VM we’re seeing the following page fault:
>>>>>>
Booting all finished, dropped to user space
.[0m.[30;1m<<.[0m.[32mseL4(CPU 0).[0m.[30;1m [decodeUntypedInvocation/205 T0x80bf81c400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>.[0m
Install gic v3
Loading Linux: 'linux' dtb: 'linux-dtb'
install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:652 module name: map_frame_hack
install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:652 module name: init_ram
libsel4muslcsys: Error attempting syscall 215
libsel4muslcsys: Error attempting syscall 215
libsel4muslcsys: Error attempting syscall 215
Waiting recv
Ok
--------
.[31;1mPagefault from [Linux]: read prefetch fault @ PC: 0x200 IPA: 0x200, FSR: 0x82000005
Context:
x0: 0xb2000000
x1: 0x0
x2: 0xff058169ac
x3: 0x3ec6
x4: 0x5527eb8
x5: 0x80000
x6: 0x58169c0
x7: 0x45dad8
x8: 0x5816a00
x9: 0x8c3a000038000000
x10: 0x1100000028000000
x11: 0x10000000
x12: 0x543a00003a040000
pc: 0x200
x14: 0x0
sp: 0x480a58
spsr: 0x3c5
x13: 0x0
x15: 0x1000000
x16: 0xb2000000
x17: 0x480a58
x18: 0x5816bd0
x19: 0x664616f6c
x20: 0xb2000000
x21: 0xb0080000
x22: 0x5816a10
x23: 0x405524
x24: 0x5816ab0
x25: 0x5816a40
x26: 0x0
x27: 0xb2000000
x28: 0x480a58
x29: 0x480a50
x30: 0xc63e0000edfe0dd0
.[3.[0mm--------
main_continued(a)main.c<mailto:main_continued@main.c>:1134 Failed to run VM
<<<<<<
From existing reports it is my understanding that the “insufficient memory” and the “error attempting sys call 215” errors are to be expected and are not a concern; please correct me if that is not the case!
Any suggestions as to the possible cause of the page fault or hints on how to progress with debugging this issue would be greatly appreciated.
Thanks for your help,
Stephen
This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.