- Devel - lists.sel4.systems

Known working embedded device for CAmkES VMs
by christinefragoso＠protonmail.com 23 Sep '21

23 Sep '21

I want to run cross-communicating CAmkES VMs on an embedded device. I see from https://github.com/seL4/camkes-vm-examples that my options are optiplex9020, cma34cr, and exynos5422. Are there any other options? Which of these options are known to work properly with a recent seL4 image?

1 0

Removing support for KZM, i.MX31 and ARMv6
by Matthew Brecknell 16 Sep '21

16 Sep '21

To reduce maintenance burden, we would like to remove seL4 support for the KZM evaluation board, which is based on the freescale i.MX31 processor with an ARM1136 core. Since this is the only ARMv6 platform supported by seL4, this would also remove support for ARMv6. We've previously sought feedback here, and in the seL4 discourse: https://sel4.discourse.group/t/should-we-continue-to-support-armv6-and-kzm-… https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/EQ27WY… We've now prepared an RFC to begin the formal process to remove KZM support: https://sel4.atlassian.net/browse/RFC-8 If you have concerns about this, please raise them as soon as possible! If you support the change, please also let us know, since that helps us establish consensus.

1 0

sel4webserver build problem
by Michael Neises 14 Sep '21

14 Sep '21

Hello, I'm trying to learn from the "sel4webserver" app here: https://docs.sel4.systems/projects/sel4webserver/. I believe I've been able to configure my network the way described on that page, but I'm failing to build because I'm missing the docsite dependencies here: https://github.com/seL4/docs/blob/master/tools/Dockerfile I build all my camkes apps using docker's `make user` with these files here: https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles.git I'm sure there's a way to have a docker container with these camkes dependencies as well as the docsite dependencies, but I'm not an expert with docker. Does anyone have any tips on how to make all these things play nice together? Cheers, Michael Neises

1 0

Steal This Drone: High Assurance Cyber Military Systems
by William ML Leslie 02 Sep '21

02 Sep '21

Looks like the HACMS talk from Collins Aerospace at DEFCON is up. This covers the system they built to fly aircraft on seL4, and especially the tools they used to do so. It's pretty light on technical content, but still quite impressive. https://youtu.be/X9rsv4YIShY -- William Leslie Q: What is your boss's password? A: "Authentication", clearly Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement.

1 0

Port to a cartesi-machine (riscv:rv64ima)
by marcelo.politzer＠cartesi.io 30 Aug '21

30 Aug '21

Hi, I'm in the process of porting seL4 to a cartesi-machine, which is basically a riscv:rv64ima without PMP (at least for now). after increasing the available memory 4G and a tweak in the elfloader to accept the flattened device tree from OpenSBI I got the kernel to start[1], but with errors. Tried to boot a hello world and the sel4tests, both give pretty much the same result. I have a suspicion that the unsupported PMP may have something to do with this but since I'm still pretty new to seL4 so I would like advice on how to debug this further. Best, Marcelo [1] ``` OpenSBI v0.9 ____ _____ ____ _____ / __ \ / ____| _ \_ _| | | | |_ __ ___ _ __ | (___ | |_) || | | | | | '_ \ / _ \ '_ \ \___ \| _ < | | | |__| | |_) | __/ | | |____) | |_) || |_ \____/| .__/ \___|_| |_|_____/|____/_____| | | |_| Platform Name : Cartesi Platform Features : mfdeleg Platform HART Count : 1 Platform IPI Device : aclint-mswi Platform Timer Device : aclint-mtimer Platform Console Device : htif Platform HSM Device : --- Platform SysReset Device : htif Firmware Base : 0x80000000 Firmware Size : 260 KB Runtime SBI Version : 0.3 Domain0 Name : root Domain0 Boot HART : 0 Domain0 HARTs : 0* Domain0 Region00 : 0x0000000002080000-0x00000000020bffff (I) Domain0 Region01 : 0x0000000002000000-0x000000000207ffff (I) Domain0 Region02 : 0x0000000080000000-0x000000008007ffff () Domain0 Region03 : 0x0000000000000000-0xffffffffffffffff (R,W,X) Domain0 Next Address : 0x0000000080200000 Domain0 Next Arg1 : 0x000000017fff0000 Domain0 Next Mode : S-mode Domain0 SysReset : yes Boot HART ID : 0 Boot HART Domain : root Boot HART ISA : rv64imasu Boot HART Features : scounteren,mcounteren,time Boot HART PMP Count : 0 Boot HART PMP Granularity : 0 Boot HART PMP Address Bits: 0 Boot HART MHPM Count : 0 Boot HART MIDELEG : 0x0000000000000222 Boot HART MEDELEG : 0x000000000000b109 ELF-loader started on (HART 0) (NODES 1) paddr=[80200000..806e5037] Loaded DTB from 17fff0000. paddr=[84025000..84025fff] ELF-loading image 'kernel' to 84000000 paddr=[84000000..84024fff] vaddr=[ffffffff84000000..ffffffff84024fff] virt_entry=ffffffff84000000 ELF-loading image 'sel4test-driver' to 84026000 paddr=[84026000..8445bfff] vaddr=[10000..445fff] virt_entry=1eef8 Enabling MMU and paging Jumping to kernel-image entry point... Init local IRQ Bootstrapping kernel Initialing PLIC... Booting all finished, dropped to user space /host/cartesi/kernel/src/kernel/faulthandler.c:156 :: Caught cap fault in send phase at address 0 while trying to handle: user exception 0x2 code 0 in thread 0xffffffc17feca200 "rootserver" at address 0x101f0 With stack: 0x333e70: 0x4 0x333e78: 0x3 0x333e80: 0x333ec0 0x333e88: 0x1f884 0x333e90: 0x333f30 0x333e98: 0x333f20 0x333ea0: 0x333f10 0x333ea8: 0x100000000 0x333eb0: 0x333f00 0x333eb8: 0x1f008 0x333ec0: 0x0 0x333ec8: 0x333f30 0x333ed0: 0x333f20 0x333ed8: 0x333f10 0x333ee0: 0x1 0x333ee8: 0x14540 ```

4 7

Compiling rumprun's libc as a shared object
by Ellis 26 Aug '21

26 Aug '21

Hello, Recently I have been trying to use sel4 rumprun on another build system after compiling but I've noticed that rumprun or musl libc only produce static libraries. How would I compile libc as a shared object? Sincerely, Ellis

1 0

Re: Is the project port Minix 3 to run on seL4 already in work?
by Christian Sagstetter 24 Aug '21

24 Aug '21

@Gernot yes that's exactly what I meant when I saw the suggested project here: https://docs.sel4.systems/SuggestedProjects.html. is there anything left from the student project that I could continue working on? best, christian

2 1

DeclareCAmkESComponent questions
by Grant Jurgensen 23 Aug '21

23 Aug '21

Hi, I have a couple questions about the `DeclareCAmkESComponent` CMake function. First, is there a way to add a dependency to a CAmkES component? Normally I would use the CMake function `add_dependencies`, but this requires a target name, and I don't believe that the `DeclareCAmkESComponent` function exposes any such target name. If the function deliberately obscures the target name, perhaps a `DEPENDENCIES` argument could be added to the function? Second, does the `INCLUDES` argument to `DeclareCAmkESComponent` ignore / filter out certain include paths? My compilation was failing because it could not find the proper headers packaged with my compiler. Even if I added the path explicitly by passing it to the `INCLUDES` argument, it was seemingly ignored. It wasn't until I copied the headers to a new directory, and explicitly passed that directory to `INCLUDES` that my compilation succeeded. Any ideas what's going on here? Thanks! Grant Jurgensen

3 6

Is the project port Minix 3 to run on seL4 already in work?
by christian.sagstetter＠googlemail.com 23 Aug '21

23 Aug '21

hello everyone, I would be interested in the project and wanted to know if it is already being worked on. best christian

3 3

Uses and description for seL4_CNode_Mutate?
by Mark Jones 23 Aug '21

23 Aug '21

This isn't a big issue, but I'm curious about how seL4_CNode_Mutate is intended to be used, and have found that the description in the seL4 reference manual doesn't seem to match the implementation. Is it for changing rights? The manual (Section 3.1.2) says: "seL4_CNode_Mutate() can move a capability similarly to seL4_CNode_Move() and also reduce its rights..." Section 3.1.4 also refers to the possibility to specify a new set of rights with an invocation of seL4_CNode_Mutate(). However, the summary of seL4_CNode_Mutate in Section 10.3.1.6 does not include a parameter that specifies any rights information, so it appears that it cannot actually be used in this way. Is it for changing badges? In Section 4.2.1, the manual says that "An endpoint capability with a zero badge ... can be badged with the seL4_CNode_Mutate() or seL4_CNode_Mint() invocations" There is a similar statement for Notifications in Section 5.1. But a comment in the (Haskell version of the) spec says "endpoint capabilities may not have their badges changed" when they are updated by a Mutate or Rotate operation. And the kernel seems to follow this: I added a test to sel4test to confirm that you get an illegal operation error if you try to badge an endpoint using Mutate. (Assuming I wrote the test correctly ...) Unless there are other arch-specific use cases, it looks like the only thing you can do with Mutate is to change the guard of a CNode capability. Even then, that is only possible if you are moving the capability at the same time. Of course, you could combine a mutate with a regular move to simulate an in-place update ... but you could also use an in-place mutate and a separate move to simulate the current behavior, without having to find an empty slot if you just wanted the in-place operation. One conclusion is that the manual's description of Mutate probably needs an update. But if nobody else has tripped over problems using it to create badged endpoints, then perhaps Mutate just isn't being used very much at all and could be removed altogether? A second thought is whether Mutate could be modified to perform an in-place update if the source and destination are the same (i.e., similar in some ways to how you specify a swap with Rotate)? Best wishes, Mark

4 5