- Devel - lists.sel4.systems

"Incorporating into your project"
by fosslinux 27 Sep '21

27 Sep '21

Dear seL4 devs and community. I am attempting to integrate seL4 into a new project of mine. To begin setting up this project, I used https://docs.sel4.systems/projects/buildsystem/incorporating.html as a reference to set up the structure of the repository (FWIW, I did not use repo, however I do not believe this should impact the build system). However, it appears these instructions may be outdated(?) or otherwise incorrect. I set up a file structure as shown under the heading "Kernel directory" in the above webpage, taking sources from; kernel/ -> https://github.com/sel4/sel4 projects/seL4_libs/ -> https://github.com/seL4/seL4_libs tools/ -> https://github.com/seL4/seL4_tools I symlinked default-CMakeLists.txt to CMakeLists.txt in the root directory as well as init-build.sh to the root directory. I created a build directory, and from within that directory, executed ../init-build.sh -DPLATFORM=X86_64 -DSIMULATION=TRUE, but this produced the CMake error; CMake Error at kernel/configs/seL4Config.cmake:174 (message): Variable 'KernelArch' is not set. Call Stack (most recent call first): kernel/CMakeLists.txt:10 (include) (I got the same result regardless of PLATFORM value). I cannot tell where the issue lies. Any pointers would be appreciated. Kind regards, ST (fossy)

2 2

Call for participation in embedded power system security exercise
by Gernot Heiser 27 Sep '21

27 Sep '21

Abstract: We are conducting a small embedded power systems security exercise at Charles Darwin University Control Systems Test Facility (CSTF) on the Laot System designed for protecting critical infrastructure (see https://trustworthy.systems/projects/TS/laot, https://eds.power.on.net/laot-pub) The exercise will involve penetration testing with the targets being a generator controlled by a Comap controller and a small nuclear reactor simulator (see https://eds.power.on.net/little-moata/index) These devices will for parts of the exercise be protected by the Laot system. There will be no cost to participants. All material including reports will be provided to all participants at the end. Keywords: seL4, Laot, MODBUS, Security, Protection of Critical Infrastructure, Hybrid Power Systems, AUUG What: Laot is a seL4-based system for protecting critical infrastructure. Why: The exercise is intended to test the system and provide a useful exercise for the penetration testing on industrial control systems. When: Over the next 2-4 weeks. How: Send an email or ring Phil he will give you an exercise brief and timings. Any general enquires are also welcome via the same means. Where: Remote for participants but the lab is in Darwin, Northern Australia. Local Darwin participants will be provided appropriate Darwin food and drink. Who: The 3 members of the Laot team are Gernot Heiser, Ben Leslie and Phil Maker. What: the exercise will be conducted over a 72h period in order to document and describe vulnerabilities in a variety of systems. Please read the Laot and little moata references above and contact Phil. In terms of background you will need to know the usual kali penetration tools (nmap, ...) and have an idea about either C or MODBUS. We will provide example code and exercise instructions. Phil Maker web: https://eds.power.on.net/EDS email: <philip.maker(a)gmail.com> phoneemail: <philmakerphone(a)gmail.com> -- email to phone (fastest) phone: +61 (0)447 630 229

1 0

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