- Devel - lists.sel4.systems

Runtime Measurement Hiccup
by Michael Neises 25 Oct '21

25 Oct '21

Hello seL4 developers, I want to be able to retrieve data from seL4's virtual Linux machine, in order to store it in a persistent way. Namely, I want to be able to simulate a seL4 kernel, boot its Linux virtual machine, compute some hash digests, and then export those hash digests. These digests are valuable because they represent the "clean room" runtime-state of the linux machine. Currently I can export these digests by way of hand-eye coordination, but I consider this unusable as a piece of software. To date I've taken two main approaches: CAmkES FileServer or virtual networking. I'm under the impression that the FileServer changes are not persistent through reboot, and even if they were, to change the boot image after compile-time would seem to fly in the face of seL4's principles. Virtual networking seems to promise I can host my digests on a webpage that is visible to my "root host" machine; that is, the simulated seL4's linux instance hosts a site available on my 192.168.x.x network. I know there is a seL4webserver app as part of the seL4 repositories which claims to do this, but unfortunately its prose is unhelpful and it doesn't seem to work even when it compiles and simulates. I've taken two distinct strategies to investigate the virtual network approach. First, I tried to get it to work on my normal stack: Windows 10 using WSL2 using a Docker container to simulate the seL4 image. The problem with this approach is that it appears I'm required to blindly thread 3 or 4 needles all at once, without getting feedback more descriptive than "you didn't do it." In other words, there does not appear to be a partial success available, and without ICMP ping, I honestly have no idea how to debug these "virtual" networks. Next, I tried simplifying my stack by installing the dependencies natively on a Debian 10 machine, which should bypass several layers of the virtual network I was suggesting in my first strategy. Unfortunately, I met with the same "AttributeError: module 'yaml' has no attribute 'FullLoader'" error that inspired me to begin using Docker several years ago. Of course I should note that "pip/pip2/pip3 install pyyaml" all report that pyyaml is already installed, so I would be in debt to anyone who has an idea about that error. To conclude, I find virtual networks opaque, and I would be grateful for any guidance. If you have a different idea how I might achieve my goal, I would be similarly effusive in my thanks. Cheers, Michael Neises

4 6

Verified platform (Sabre lite)
by ouvl 15 Oct '21

15 Oct '21

Good afternoon. The only verified platform is Sabre lite (Platform Sabre lite, System-on-chip i.MX6). There is a link for the board on the website https://docs.sel4.systems/Hardware/sabreLite.html, but the link https://boundarydevices.com/product/sabre-lite-imx6-sbc/ is not working. On the same site https://boundarydevices.com, board https://boundarydevices.com/product/bd-sl-i-mx6/ is displayed. There are different boards with iMX6 processor, and processors, for example, i.MX 6 ULL, i.MX 6 UltraLite, i.MX 6 SLL, i.MX 6 SoloLite, i.MX 6 SoloX, i.MX 6 Solo, i.MX 6 Solo, i.MX 6 Dual, i.MX 6 Quad, i.MX 6 DualPlus, i.MX 6 QuadPlus. There is only 1 GiB of RAM in the board, so please clarify regarding my question. Are all the boards suitable for the operation of a verified microkernel seL4 with full verification, or is only https://boundarydevices.com/product/bd-sl-i-mx6/ suitable board?

1 0

Inter-VM communication on seL4
by everton＠ssrc.tii.ae 29 Sep '21

29 Sep '21

Hello seL4-devs, I am working with seL4 running as a hypervisor with multiple VMs. I am aware of vchan (inactive) and VirtIO Net as mechanisms for inter-VM communication on top of seL4. However, I am looking to have a shared memory inter-VM communication between my VMs. Is there a well-maintained mechanism with shared memory and notifications for inter VM communication? I have been trying to create a CAmkES example with dataport and I found out this "seL4SharedDataWithCaps" CAmkES connector for connecting dataport interfaces (https://github.com/seL4/global-components/issues/8) connection seL4SharedDataWithCaps sharedMem(from vm0.dummy_port, to vm0.buff, to vm1.buff); The "to" side of the connection is supposed to give capabilities to both vmm0 and vmm1 (workaround proposed in the link above). How to use those capabilities to map "buff" into Linux guest address space? Ideally, I would like to access that "buff" from Linux kernel without VMM intervention. Thank you in advance. Best, Everton

2 1

ethernet pass-through using CAmkES VM on x86
by meshkat os 29 Sep '21

29 Sep '21

hi I am new to camkes VM on x86. I want to connect the guest to the host via the ethernet network. and I used this ( https://docs.sel4.systems/projects/camkes-vm/) tutorial to create pass-through in minimal example x86. run in qemu on ubuntu 17.10. but the guest os doesn't create an ethernet interface. I also tested zmq example this is qemu options: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 and minimal.camkes configs: configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0) vm0.simple_untyped23_pool = 20; vm0.heap_size = 0x2000000; vm0.guest_ram_mb = 128; vm0.kernel_cmdline = VM_GUEST_CMDLINE; vm0.kernel_image = "bzimage"; vm0.kernel_relocs = "bzimage"; vm0.initrd_image = "rootfs.cpio"; vm0.iospace_domain = 0x0f; vm0_config.pci_devices_iospace = 1; vm0_config.ioports = [ {"start":0x4080, "end":0x4090, "pci_device":0x1f, "name":"SATA"}, {"start":0x4090, "end":0x40a0, "pci_device":0x1f, "name":"SATA"}, {"start":0x40b0, "end":0x40b8, "pci_device":0x1f, "name":"SATA"}, {"start":0x40b8, "end":0x40c0, "pci_device":0x1f, "name":"SATA"}, {"start":0x40c8, "end":0x40cc, "pci_device":0x1f, "name":"SATA"}, {"start":0x40cc, "end":0x40d0, "pci_device":0x1f, "name":"SATA"}, {"start":0x3000, "end":0x3020, "pci_device":0, "name":"Ethernet5"}, ]; vm0_config.pci_devices = [ { "name":"SATA", "bus":0, "dev":0x1f, "fun":2, "irq":"SATA", "memory":[], }, { "name":"Ethernet5", "bus":5, "dev":0, "fun":0, "irq":"Ethernet5", "memory":[ {"paddr":0xc0500000, "size":0x20000, "page_bits":12}, {"paddr":0xc0520000, "size":0x4000, "page_bits":12}, ], }, ]; vm0_config.irqs = [ {"name":"SATA", "source":19, "level_trig":1, "active_low":1, "dest":11}, {"name":"Ethernet5", "source":0x11, "level_trig":1, "active_low":1, "dest":10}, ]; } thanks

4 4

seL4 Raspberry Pi 4B Support
by Drew Humphrey 29 Sep '21

29 Sep '21

Hi, I am doing a feasibility study to ascertain whether Linux can be deployed to a seL4 kernel running on a Pi 4B with 8GB of memory. I have seen that there is explicit support for the Pi 3B, and that Linux can be run in a virtual machine on top of seL4. But I did not see explicit support for a Pi 4B and the ability to have the Pi run the Linux VM. Please let me know if this would be possible. Thanks, Drew Humphrey

4 3

Mismatch in number of pages allocated
by Sid Agrawal 29 Sep '21

29 Sep '21

Hi sel4-dev, I was looking at the sel4utils/vspace <https://github.com/seL4/seL4_libs/tree/master/libsel4utils> library and noticed a mismatch in the number of pages allocated as per the two data structures which keep track of the address space. Below I have laid out my test setup, steps to reproduce and finally the exact questions. In my test setup(which is copied from sel4test system), the root task(driver) starts another process(test app) with its own address space using sel4utils_spawn_process_v.(inside basic_run_test). Then in the root task we do a walk of the child task's address space structures maintained by sel4utils/vspace library. The 2 structures I am walking are: - The linked list of reservations: source-code <https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4util…>: Here we traverse a linked list and count the number of pages which have been allocated based on the size of each reservation. - The tree which keeps the caps of pages mapped so far(sort of like the shadow page table). source-code <https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4util…>. Here we traverse the multi-level shadow page table hierarchy to count the pages the library has mapped. I find that the number of pages I get from the 2 walks are not equal. I understand that neither of the above are reflective of the true state of the address space as that is only known to the kernel. So, it is simply possible that in some code path, the library inserts an entry in to one of the structures and not the other. I have used Intel 32-bit platform to keep the page table structure simple for this query. Here is the code to walk the vspace(source code) <https://github.com/sid-agrawal/seL4_libs/blob/0d37c61f89dc335a5905f5625be31…> : int sel4utils_walk_vspace(vspace_t *vspace, vka_t *vka) { sel4utils_alloc_data_t *data = get_alloc_data(vspace); int index = 0; sel4utils_res_t *sel4_res = data->reservation_head; printf("===========Start of interesting output================\n"); printf("VSPACE_NUM_LEVELS %d\n", VSPACE_NUM_LEVELS); /* walk all the reservations */ printf("\nReservations from sel4utils_alloc_data->reservation_head:\n"); while (sel4_res != NULL) { long int sz = (sel4_res->end - sel4_res->start ) / (4 * 1024); printf("\t[%d] %p->%p %lu pages malloced(%u)\n", index, sel4_res->start, sel4_res->end, sz, sel4_res->malloced); index++; sel4_res = sel4_res->next; } int num_empty = 0; int num_reserved =0; int num_used =0; int i = 0; /* Walk all the page tables */ printf("\n\nIntel-32 Page Table Hierarcy from sel4utils_alloc_data->top_level->table \n"); if (data->top_level) { for (i = 0; i < BIT(VSPACE_LEVEL_BITS); i++) { if (data->top_level->table[i] == RESERVED) { num_reserved++; } else if (data->top_level->table[i] == EMPTY) { num_empty++; } else { num_used++; vspace_bottom_level_t *bottom_table = (vspace_bottom_level_t *)data->top_level->table[i]; int L2_num_empty = 0; int L2_num_reserved = 0; int L2_num_used = 0; int ii = 0; for (ii = 0; ii < BIT(VSPACE_LEVEL_BITS); ii++) { uintptr_t cap = bottom_table->cap[ii]; if (cap == RESERVED) { L2_num_reserved++; } else if (cap == EMPTY) { L2_num_empty++; } else { L2_num_used++; } } printf("PDE-Index(%d) \n\t" \ "NUM-PTE: %5d Empty: %5d \tReserved: %5d \tUsed: %5d\n", i, ii, L2_num_empty, L2_num_reserved, L2_num_used, ii); } } printf("===========Start of interesting output================\n"); } return index; } Test Environment: - The docker environment was setup using instruction from Using Docker for seL4 <https://docs.sel4.systems/projects/dockerfiles/>. - Qemu on Ubuntu 20.04 on 64 bit Intel machine Below is the steps to reproduce the issue: # Setup the project using a manifest repo. # The structure of the project is borrowed from sel4test. # The manifest points two repo's which are not original sel4 repos: # - seL4_libs: The new walker helper is here, based on fork of sel4/sel4_libs # - sel4-gpi: The test code is here. This is new repo. mkdir sel4-gpi-system cd sel4-gpi-system repo init -u https://github.com/sid-agrawal/sel4-gpi-manifest -b refs/tags/v3.0 repo sync container # Jump to the docker sel4 dev environment, omit if you do not care mkdir build cd build ../init-build.sh -DPLATFORM=ia32 -DSIMULATION=TRUE ninja && ./simulate # To exit Qemu Ctrl-A X The output from the test code is: ===========Start of interesting output================ VSPACE_NUM_LEVELS 2 Reservations from sel4utils_alloc_data->reservation_head: [0] 0x10001000->0x10012000 17 pages malloced(1) Intel-32 Page Table Hierarcy from sel4utils_alloc_data->top_level->table PDE-Index(32) NUM-PTE: 1024 Empty: 637 Reserved: 0 Used: 387 PDE-Index(64) NUM-PTE: 1024 Empty: 1005 Reserved: 1 Used: 18 ===========Start of interesting output================ The first part of the output shows the size of the reservation in number of 4KB pages which is 17 pages. We see that the vspace has only 1 reservation, which is 17 pages long and is malloced. This itself is a little odd; I was expecting multiple reservations for code, stack, ro-data etc. The second part of the output shows the page directory and table entries. Here we see that the 2 PDE are in use with a total of 405(18 + 387) PTEs used in total. So, my query is, why is there is a discrepancy in the number of pages used? - Does the library allocate a bunch of pages(387) which do not belong to any reservation? - As far as the single page difference of 17 Vs 18, I think that can be explained by the driver sharing a page with the test-app. Besides the above, I have a couple of more general questions about the user space virtual memory libraries in seL4. - Why does the library need to mimic the PT hierarchy in user space? - I am trying to implement fork in the sel4utils, mainly as an exercise. Is there a helper function to duplicate an address space(let's say without any COW)? Thanks for your time. If there is some additional info I should be providing while raising question on this forum do let me know. Best, Sid

1 0

"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 15 Sep '21

15 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 31 Aug '21

31 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 27 Aug '21

27 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 24 Aug '21

24 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 24 Aug '21

24 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

bingup the new platform not in Linux repository
by niewei1899＠163.com 20 Aug '21

20 Aug '21

about portint doc：(https://docs.sel4.systems/projects/sel4/porting) “You may need to add device nodes depending on what Linux uses and what is required by seL4. For example, in the port of the Rockpro64 a memory node and an extra timer node were needed so these had to be defined manually.” how can I get the required by seL4? have any doc about it?

1 0

smp camkes
by David Lorentz 19 Aug '21

19 Aug '21

Hi, I've been trying to extend one of the tutorial / example projects to run on more than one core with no success. After reading the camkes manual https://docs.sel4.systems/projects/camkes/manual.html#thread-cpu-affinity I assumed that you need to set core affinities for different components in your camkes file and set the KernelMaxNumNodes to a number greater than one. I tried this with the adder sample (as below) with no luck. Can anyone point me to some information on how to get smp to work, what hardware is supported and the like? configuration { adder.affinity = 1; client.affinity = 0; } Thanks David

1 0

VM support for iMX8MM/MQ dev boards
by Zippy Manaic 18 Aug '21

18 Aug '21

Hi, I have been attempting to follow some breadcrumbs to get vm_minimal app running on an IMX8 dev board. I am attempting to follow the commits by Sylvain but I think there may be a missing push to seL4/camkes-vm. Are there any plans to more formally support iMX8 platforms for VM development on seL4? Assuming I manage to get vm_minimal running on iMX8 what would be the odds of getting 2 VMs running on iMX8? Are there known limitations to the current CAmkES VM implementation that would cause me problems? Thanks, Zippy

1 0

seL4 Kernel: ARMv8.2 support
by Jorge Pereira 17 Aug '21

17 Aug '21

Hi all, Is the seL4 Kernel (with VE enabled) supporting versions of ARMv8 (e.g. ARMv8.2) other than the original one - v8.0? We'd like to port seL4 for a board that features ARMv8.2 CPUs. Is there any foreseeable roadblock? Thanks.

1 0

[Tutorial] Should the tutorial of seL4 be updated?
by Zheng Wenxin 10 Aug '21

10 Aug '21

It seems that the tutorial "CAmkES VM: Cross VM Connectors" has something missing. The part "Add modules to the guest" says that "There is a library in projects/camkes/vm-linux/camkes-linux-artifacts/camkes-linux-apps/camkes-connector-apps/libs containing Linux system call wrappers ...". But no folder named camkes/vm-linux and in camkes-vm-linux/camkes-linux-artifacts/camkes-linux-apps/camkes-connector-apps, no folder named libs. Is the tutorial should be updated?

1 0

seL4 how to access el3 secure world on ARM platfrom
by yadong.li 07 Aug '21

07 Aug '21

Hi： We want to create component driver who need to access ARM el3 secure world to read/write hardware register. But I found that seL4 did not offer capability to call smc function for component of native world. Which cap that already existed can offer the syscall or create new smc cap ? Is there some plan to support it ? Thank you very much.

2 1

some unexpected phenomenon about scheduling
by yadong.li 07 Aug '21

07 Aug '21

Hi: Recently, I found some unexpected phenomenon about scheduling on our project. My environment as follows: I run linux guest on seL4, Linux guest has 8 vcpu on 8 Arm PE from core0 ~ core7. WFI is not trap, seL4 is master kernel not mcs kernel I think seL4 idle task will not be run on core1, it will always run vcpu task. But the truth is the idle task will be run. I found when the maintenance and timer interrupt of Linux guest came, it will switch to idle, Because above interrupts handle will call handleFault, the sendIPC will set the ksCurThread(vcpu task) block on send, and the ksReadyQueuesL1Bitmap is empty. The idle task wille be run. But the recv task maybe run on core0, now core1 is in idle, is it reasonable? Thank you very much

2 1

Failure on a CAmkES-VM with more than 150MB RAM
by hamed_ganji＠aut.ac.ir 06 Aug '21

06 Aug '21

Hello, I have a problem on booting a CAmkES-VM with more than 150MB RAM. The following error appears when I set [vm0.guest_ram_mb = 256] in the camkes file of the minimal example of CAmkES-VM and boot the produced image on both QEMU and real hardware system: ------------------------------------------------------------ ... vka_alloc_object_at_maybe_dev@object.h:64 Failed to allocate object of size 4096, error 1 alloc_bios_memory@acpi.c:119 Failed to allocate frame for bios addr 0xe0000 main_continued@main.c:871 [Cond failed: error] Failed to init guest boot structure ------------------------------------------------------------ Please find the full output of the booting process in attachment file. I also examined the effect of other parameters like [vm0.simple_untyped23_pool] and [vm0.heap_size] but no difference was found. Any help/hint would be very appreciated. Best regards, Hamed Ganji

1 0

Where does rumprun mount /
by Ellis 04 Aug '21

04 Aug '21

Hello, I have been messing around with sel4 rumprun and I have been trying to put files onto the file system. Where does rumprun mount the root / ? Sincerely, Ellis

1 0

Operating Systems built on top of seL4
by Sidhartha Agrawal 02 Aug '21

02 Aug '21

Hello sel4-devs, I am a first-year graduate student at the University of British Columbia at their Systopia Lab <https://systopia.cs.ubc.ca/> working on operating systems research. My advisor is Prof. Margo Seltzer <https://www.seltzer.com/margo>. In a past life, I have worked as a software engineer at Oracle and Arista Networks. My research is on General Purpose Isolation Mechanism in the OS. We ask whether we really need to have N different isolation mechanisms or whether instead, we could develop a framework in which all these different mechanisms represent points on a continuum. Here is a write-up <https://sid-agrawal.ca/#research-projects> with some more details. I am using seL4 as the microkernel base to build my research idea. At this stage, I am not looking in to the formal verification aspect of seL4, but that might change once I have a better idea about the type of mechanism I want to build. I would also like to keep the changes in the kernel to be minimum and try to demonstrate my ideas using user space processes. I have tried out the tutorials on the seL4 website. Currently, I am wading through the different helper libraries in seL4/seL4_libs <https://github.com/seL4/seL4_libs>. As someone who is just starting with seL4 ecosystem, I had a few high-level questions: - Are there are example OSes built with seL4, which would be a good place to look at? Specifically, I am looking for components such as basic versions of a process-server, vm-server, pager, file-systems server. - I came across refOS <https://github.com/seL4/refos>, but wasn't sure if it is still being maintained. - Another option was Genode <https://genode.org/documentation/general-overview/index>. This seemed to be maintained by another community and has many layers of abstractions since it supports multiple kernel backends. I am looking forward to engaging with this community, learning about seL4 and making meaningful contributions. Best, Sid sid-agrawal.ca

8 28

Sel4 rumprun has issues compiling
by Vortex 01 Aug '21

01 Aug '21

Hello, I would like to bring this issue to the attention of the community. Sel4’s fork of the rumprun unikernel no longer compiles. Due to the usage of Werror flag, the compiler produces repeated warnings which in turn creates errors. It seems like the rump kernel was tested on an older version of gcc and because it is older, raises warnings and causes the build to fail on newer compilers. This is a similar issue to https://github.com/rumpkernel/rumprun/issues/82 I have tested rumprun in the sel4 docker container. My build logs are also attached to this email. Thank you for taking attention to this issue. Sincerely, Ellis

3 3

Docker for ARM?
by dave＠synergy.org 27 Jul '21

27 Jul '21

I recently moved and my x86-64 machines are in storage. Are there docker images for Debian ARM/32 or Raspbian I can use to build seL4 on my Raspberry Pi? It is my target platform. Thanks, Dave

2 1

Camkes and native tcp/ip and networking
by Amirreza Zarraby 27 Jul '21

27 Jul '21

Hello seL4 team, I am try trying to use camkes to write a simple firewall. I am wondering if you can direct me to any existing camkes project which uses tcp/ip and network driver that I can look into as starting point. There is a seL4 based webserver but it seems to use vm and Linux. Thank you for your time. - Amir

4 3

Jetson AGX Xavier board porting
by bobding＠msn.com 27 Jul '21

27 Jul '21

Has anyone ported to Nvidia AGX Xavier board?

2 1

camkes-vm-examples-manifest cma34cr_centos fails
by christinefragoso＠protonmail.com 27 Jul '21

27 Jul '21

Hello, I'm trying to run the cma34cr_centos application from camkes-vm-examples-manifest, but I get this error: "Kernel entry via Unknown syscall, word: 65". I've set up VMware as described at https://docs.sel4.systems/Hardware/VMware/. In camkes-vm-examples-manifest/cma34cr_centos_x86_build, I've built the kernel: ../init-build.sh -DCAMKES_VM_APP=cma34cr_centos Then I ran these commands: ninja sudo ./seL4vmw.py images/kernel-x86_64-pc99 images/capdl-loader-image-x86_64-pc99 vmrun -T player start $HOME/vmware/seL4/seL4.vmx while :; do socat -d -d UNIX-CONNECT:/tmp/vsock,forever PTY,link=/tmp/mytty done After VMware boots, I ran minicom in a separate terminal to see the serial output: minicom -D /tmp/mytty Here is the full log: Welcome to minicom 2.7.1 OPTIONS: I18n Compiled on Dec 23 2019, 02:06:26. Port /tmp/mytty, 08:47:50 Press CTRL-A Z for help on special keys Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xcf3000 end=0x3821bb8 size=0x2b2ebb8 name='' Parsing GRUB physical memory map Physical Memory Region from 0 size 9f800 type 1 Physical Memory Region from 9f800 size 800 type 2 Physical Memory Region from dc000 size 24000 type 2 Physical Memory Region from 100000 size bfde0000 type 1 Adding physical memory region 0x100000-0xbfee0000 Physical Memory Region from bfee0000 size 1f000 type 3 Physical Memory Region from bfeff000 size 1000 type 4 Physical Memory Region from bff00000 size 100000 type 1 Adding physical memory region 0xbff00000-0xc0000000 Physical Memory Region from f0000000 size 8000000 type 2 Physical Memory Region from fec00000 size 10000 type 2 Physical Memory Region from fee00000 size 1000 type 2 Physical Memory Region from fffe0000 size 20000 type 2 Physical Memory Region from 100000000 size 140000000 type 1 Adding physical memory region 0x100000000-0x240000000 Got VBE info in multiboot. Current video mode is 16703 ACPI: RSDP paddr=0xf6a00 ACPI: RSDP vaddr=0xf6a00 ACPI: RSDT paddr=0xbfeee733 ACPI: RSDT vaddr=0xbfeee733 Warning: Your kernel was not compiled for the current microarchitecture. Kernel loaded to: start=0x100000 end=0xc1f000 size=0xb1f000 entry=0x100300 ACPI: RSDT paddr=0xbfeee733 ACPI: RSDT vaddr=0xbfeee733 ACPI: FADT paddr=0xbfefef67 ACPI: FADT vaddr=0xbfefef67 ACPI: FADT flags=0x21 ACPI: 0 IOMMUs detected ACPI: MADT paddr=0xbfeee937 ACPI: MADT vaddr=0xbfeee937 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x2 ACPI: MADT_APIC apic_id=0x4 ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0x6 ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0x8 ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0xa ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0xc ACPI: Not recording this APIC, only support 2 ACPI: MADT_APIC apic_id=0xe ACPI: Not recording this APIC, only support 2 ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x5 ACPI: 2 CPU(s) detected ELF-loading userland images from boot modules: size=0x3fab000 v_entry=0x408828 v_start=0x400000 v_end=0x43ab000 p_start=0x3822000 p_end=0x77cd000 Moving loaded userland images to final location: from=0x3822000 to=0xc1f000 size=0x3fab000 Starting node #0 with APIC ID 0 Mapping kernel window is done Starting node #1 with APIC ID 2 Booting all finished, dropped to user space create_object@main.c:673 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0xb0000000 seL4 root server abort()ed Debug halt syscall from user thread 0xffffff823e027400 "rootserver" halting... Kernel entry via Unknown syscall, word: 65 Any idea what's wrong? I just want to get one x86 application with cross VM connectors working. The other x86 applications (optiplex9020, cma34cr_ubuntu, zmq_samples) in camkes-vm-examples-manifest don't work for other reasons.

2 1

Formally verified AES C code
by Hugo V.C. 20 Jul '21

20 Jul '21

Hi all, I don't want to use SSL/openssl in a project I'm working. Thus, I want to just use my own encryption at the app layer. As performance is not a problem (just very small data packets over a socket) I would like to have the most simple implementation possible of AES, preferably, formally verified. Is anyone aware of any public AES encrytion implementation in C that has been formally or semi-formally verified? Thank you!

5 10

Cannot reserve memory for camkes VM guest
by Alex Ling 17 Jul '21

17 Jul '21

Hi All, I'm trying to bring up camkes VM Linux guest on Firefly RK3399 board which is with a GICv3 ARMv8. I'm using the "rockpro64" target and my work is based on [1] and [2]. When I run the "capdl-loader-image-arm-rockpro64", there's error "Range not available at 0xfef10000, size 0x10000". Bootstrapping kernel Booting all finished, dropped to user space Undelivered IRQ: 132 Install gic v3 sel4utils_reserve_range_at_no_alloc@vspace.c:595 Range not available at 0xfef10000, size 0x10000 vm_reserve_memory_at@guest_memory.c:328 Failed to allocate vm reservation: Unable to create vspace reservation at address 0xfef10000 of size 65536 vm_install_vgic_v3@vgic_v3.c:87 Error installing vgic Assertion failed: !err (/mnt/data3/projects/rk3399/build/seL4/camkes-vm-app/projects/vm/components/VM_Arm/src/main.c: main_continued: 1098) Here's my projects/seL4_projects_libs/libsel4vmmplatsupport/plat_include/rockpro64/sel4vmmplatsupport/plat/devices.h content: #define GIC_VERSION_3 #define GIC_PADDR 0xfee00000 #define GIC_DIST_PADDR (GIC_PADDR + 0x00000000) #define GIC_DIST_SIZE 0x10000 #define GIC_REDIST_PADDR 0xfef00000 #define GIC_REDIST_SIZE 0xC0000 #define GIC_REDIST_SGI_PADDR (GIC_REDIST_PADDR + 0x00010000) #define GIC_REDIST_SGI_SIZE 0x10000 I think the problem is related to GIC_REDIST_SIZE. I set it to 0xC0000 according to the rockpro64 device tree file in kernel/tools/dts/rockpro64.dts interrupt-controller@fee00000 { compatible = "arm,gic-v3"; #interrupt-cells = < 0x04 >; #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; interrupt-controller; reg = < 0x00 0xfee00000 0x00 0x10000 0x00 0xfef00000 0x00 0xc0000 0x00 0xfff00000 0x00 0x10000 0x00 0xfff10000 0x00 0x10000 0x00 0xfff20000 0x00 0x10000 >; interrupts = < 0x01 0x09 0x04 0x00 >; phandle = < 0x01 >; I tried to reduce it to 0x10000 and it can boot to VM guest but the guest Linux will fail in gic_iterate_rdists() because it cannot read from GIC's GICR_TYPER register correctly. Did I miss anything? Any suggestion is highly appreciated. Thank you very much! [1] https://github.com/seL4/seL4/pull/378 [2] https://github.com/seL4/seL4_projects_libs/tree/sylvain/gicv3 Regards, Alex

2 2

Passing caps through CAmkES procedures?
by Austin Appleby 14 Jul '21

14 Jul '21

Hi, I've got what seems like a simple task that I can't quite figure out how to implement - I am sketching out a key-value-store component where the "values" can be quite large (tens or hundreds of K). I would like clients of the component to pass caps to their own buffers in and out of this component's API to minimize copying and temporary buffer allocation and ensure that multiple clients can't see each other's data. In plain seL4 this would be done via the client passing a cap in its seL4_Call(), but I don't see an equivalent for this in CAmkES. Is there a way of declaring this in the .camkes syntax? If not, is there a way to build this component outside of CAmkES and still allow it to interact with existing CAmkES components? -Austin Appleby @ Google

1 0

CI infrastructure outage
by Peter Chubb 09 Jul '21

09 Jul '21

Hi Folks, Our continuous integration testing infrastructure is being relocated from CSIRO to UNSW premises this weekend. Because Sydney is in COVID lockdown, and because we're reworking the system not to rely on commercial software we no longer have a licence for (Atlassian Bamboo), we will probably not have everything working again for two or three weeks. The upshot for you is that any pull request that needs extensive testing will not be merged for at least two weeks, possibly longer. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0

gic v2 vs gic v3
by Chris Koziarz 09 Jul '21

09 Jul '21

Hi all, I'm trying to port camkes-arm-vm to a different platform, that supports gic-v3 In the process, I hit a compilation error: Building C object kernel/CMakeFiles/kernel_all_pp_...rapper_temp_lib.dir/ kernel_all_pp_prune_wrapper_temp.c.obj FAILED: kernel/kernel_all_pp_prune_wrapper_temp.c In file included from /home/chris/camkes-tqma8xqp- vm/kernel/src/arch/arm/object/vcpu.c:15: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v2.h:23: error: "IRQ_MASK" redefined [-Werror] 23 #define IRQ_MASK MASK(10u) In file included from kernel/gen_headers/plat/platform_gen.h:23, from /home/chris/camkes-tqma8xqp-vm/kernel/include/plat/ default/plat/machine.h:8, from /home/chris/camkes-tqma8xqp- vm/kernel/include/machine.h:9, from /home/chris/camkes-tqma8xqp- vm/kernel/include/api/syscall.h:10, from /home/chris/camkes-tqma8xqp- vm/kernel/src/api/faults.c:10: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v3.h:30: note: this is the location of the previous definition 30 #define IRQ_MASK MASK(16u) which is an indicative that both gic_v3.h & gic_v2.h headers have been included, which is an error because said headers are not compatible: kernel/include/arch/arm/arch/machine/gic_v3.h:#define IRQ_MASK MASK(16u) kernel/include/arch/arm/arch/machine/gic_v2.h:#define IRQ_MASK MASK(10u) So my question is: how can I configure the build to avoid such a conflict? I can grepp the relevant configuration option in CMakeCache.txt: build_tqma8/CMakeCache.txt:CONFIGURE_INTERRUPT_CONTROLLER:INTERNAL=arch/machine/gic_v3.h but cannot see it in ccmake gui because it's "INTERNAL" What is the solution? - replace this option somehow to use gic_v2 and have my HW use gic v.2, or - change compilation options to use gic_v3 everywhere Thanks for any help, Chris.

4 5

Re: gic v2 vs gic v3
by Alex Ling 凌云 08 Jul '21

08 Jul '21

Hi All, What is the status of virtualization support on ARM SOCs with GICv3? According to section “FAQ and Implementation Notes” of [1], seems it is still under development. Any plan or progress on this? Thank you very much. [1] https://docs.sel4.systems/projects/camkes-arm-vm/ Regards, Alex

1 0

Re: Tutorial Problem
by Kent Mcleod 08 Jul '21

08 Jul '21

On Wed, Jun 30, 2021 at 11:53 AM Michael Neises <neisesmichael(a)gmail.com> wrote: > > Kent, > > > > I tried using those extra arguments and got the same error regarding kvm I reported a few minutes ago: > > > > ./simulate: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,+syscall,+lm,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 Could not access KVM kernel module: No such file or directory > > qemu-system-x86_64: failed to initialize KVM: No such file or directory > There are instructions on how to setup KVM and nested virtualization on the tutorial that I've pasted here: "Note if you are using QEMU it is important to ensure that your host machine has VT-x support and KVM (https://www.linux-kvm.org/page/Main_Page) installed. You also need to ensure you have enabled nested virtulisation with KVM guests as described here (https://www.linux-kvm.org/page/Nested_Guests)" A quick way to check if nested virtualization is enabled (and therefore supported) on your host is to run `cat /sys/module/kvm_intel/parameters/nested`. `Y` should be returned if it's enabled. It may be easier to run the image on an actual machine instead of in qemu. The images produced can be loaded by a multiboot loader such as grub or pxelinux. (https://docs.sel4.systems/Hardware/VMware/#add-grub2-option-to-run-sel4) has an example grub config.

4 7

seL4 Linux guest mmap() crashes the VM
by Hugo V.C. 02 Jul '21

02 Jul '21

Hi, my seL4 Linux VM box just crashed when trying to access a memory address. Basically I simply wanted to use "devmem" tool to just print the content of a specific address in memory and looked like seL4 was unable to handle the guest OS mmap() correctly. Below the console log: # ls /proc/283/maps /proc/283/maps # cat /proc/283/maps 00400000-00532000 r-xp 00000000 00:02 6023 /bin/lighttpd 00541000-00543000 r--p 00131000 00:02 6023 /bin/lighttpd 00543000-00546000 rw-p 00133000 00:02 6023 /bin/lighttpd 00546000-0054d000 rw-p 00000000 00:00 0 0bd0b000-0bd2d000 rw-p 00000000 00:00 0 [heap] 0bd2d000-0bd91000 rw-p 00000000 00:00 0 [heap] ffff82084000-ffff82085000 r--p 00000000 00:00 0 [vvar] ffff82085000-ffff82086000 r-xp 00000000 00:00 0 [vdso] ffffe6c58000-ffffe6c79000 rw-p 00000000 00:00 0 [stack] # devmem 0xffffe6c58000 8 _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0xffffe6c58000 map_page@mapping.c:68 Failed to map page at address 0xffffe6c58000 with cap 396187, error: 1 sel4utils_map_page_pd@vspace.c:153 Error mapping pages, bailing: 1 map_vm_memory_reservation@guest_memory.c:477 Failed to map address 0xe6c58000 into guest vm vspace vm_map_reservation@guest_memory.c:510 Failed to map vm reservation: Error when mapping into VM's vspace -------- Pagefault from [Linux]: read fault @ PC: 0x414c38 IPA: 0xffffe6c58000, FSR: 0x93020004 Context: x0: 0xffff9cfe6000 x1: 0x0 x2: 0x0 x3: 0x1 x4: 0x3 x5: 0xffffe6c58000 x6: 0x5 x7: 0x20 x8: 0xde x9: 0xffffe539cf54 x10: 0xffff9cfe8050 x11: 0x1 x12: 0x436 pc: 0x414c38 x14: 0xffffffff sp: 0xffffe539bb70 spsr: 0x60000000 x13: 0x1 x15: 0x3 x16: 0xffff9cf486c8 x17: 0x4c3870 x18: 0x0 x19: 0x8 x20: 0x0 x21: 0x4c3000 x22: 0xffffe539bd98 x23: 0xffffe6c58000 x24: 0x0 x25: 0x0 x26: 0x0 x27: 0x0 x28: 0x0 x29: 0xffffe539bc60 x30: 0x414bac m-------- main_continued@main.c:1134 Failed to run VM Halting... My three concerns here are: 1) Why this guest mmap() is crashing the VM? Memory address is valid (just guest user space process stack). 2) Is it possible to have some kind of "dump and reboot VM" when a VM and/or guest OS crashes? 3) Are there any plans to formally verify the seL4's VM camkes code? Thank you!

2 6

Camkes SerialServer and util_libs/libplatsupport with ODROID-C4
by Robert Reid 01 Jul '21

01 Jul '21

Hi everyone Summary - trying to get util_libs/libplatsupport going for a HardKernel ODROID-C4, using the camkes serialserver_polling app - but not having any luck with mapping the UART. I'd welcome any explanations of what you think is happening here. The background and my progress follows. I thought I'd dive into the seL4 world and do some experimenting. I thought a good place to start would be the UNSW AOS project (17 years after I first did it) - but with no more ODROID-C2, got a hold of an ODROID-C4 and figured that would be a good project in itself (and well timed with a Sydney lockdown). So - good news: The peripheral devices we need are all very similar to a C2, so by getting a new DTS file and updating a few addresses it starts off fairly happily. sel4-test builds and runs (All is well...); so does the camkes adder app; and with some mods to provide enough slots (maybe because it has 4GB rather than 2GB) I have got the AOS milestone 0 stub to run (including the uart initialisation). (More work to actually finish m0 and keep going, but a job for later) But then: I moved onto the util_libs / libplatsupport project to try and port over as much of the device settings as possible; and using the camkes app serialserver_polling, under the hood using SerialServer, I can't get the uart to initialiise (or more strictly can't get the uart address to map). chardev_map / ps_io_map fails, returning a vaddr of 0. I've added a bunch of debug prints to the process; and for comparison also run it on QEMU emulating a Sabre board. On odroidc4 hardware: ## Starting application at 0x01080000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A55 r1p0 paddr=[95e000..d5710f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at a86de8. Loaded DTB from a86de8. paddr=[23f000..24afff] ELF-loading image 'kernel' to 0 paddr=[0..23efff] vaddr=[ffffff8000000000..ffffff800023efff] virt_entry=ffffff8000000000 ELF-loading image 'capdl-loader' to 24b000 paddr=[24b000..563fff] vaddr=[400000..718fff] virt_entry=408e48 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space pre_init@serial.c:501 About to init port, io_ops=0x487cf0 ps_cdev_init@chardev.c:46 About to init_fn 3 ps_cdev_init@chardev.c:47 dev_defn[3].paddr: 0xff803000, size 1000 uart_init@serial.c:51 about to chardev_map: dev=0x473948, defn->id=3, defn->padd r=0xff803000 chardev_map@chardev.h:26 ops->io_mapper=0x487be0 &(ops->io_mapper)=0x442728 dev- >paddr=0xff803000 dev->size=0x1000 uart_init@serial.c:56 chardev_map mapped page_vaddr 0 plat_pre_init@plat.c:64 Failed to initialise character device plat_pre_init@plat.c:65 PS_SERIAL_DEFAULT: 3 On Sabre QEMU: ./simulate: qemu-system-arm -machine sabrelite -nographic -serial null -serial mon:stdio -m size=1024M -kernel images/capdl-loader-image- arm-imx6 ELF-loader started on CPU: ARM Ltd. Cortex-A9 r0p0 paddr=[106fc000..10aa98e3] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 107fe33c. Loaded DTB from 107fe33c. paddr=[1003d000..10047fff] ELF-loading image 'kernel' to 10000000 paddr=[10000000..1003cfff] vaddr=[e0000000..e003cfff] virt_entry=e0000000 ELF-loading image 'capdl-loader' to 10048000 paddr=[10048000..10300fff] vaddr=[10000..2c8fff] virt_entry=187f8 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. Booting all finished, dropped to user space pre_init@serial.c:501 About to init port, io_ops=0x69cf0 ps_cdev_init@chardev.c:45 About to init_fn 1 ps_cdev_init@chardev.c:46 dev_defn[1].paddr: 0x21e8000, size 1000 uart_init@serial.c:224 about to chardev_map: dev=0x7f8c8, defn->id=1, defn->paddr=0x21e8000 chardev_map@chardev.h:26 ops->io_mapper=0x69cf0 &(ops->io_mapper)=0x1f328 dev->paddr=0x1f654 dev->size=0x4ebc4 uart_init@serial.c:226 chardev_map mapped vaddr 0xbb000 pollcli: Hello Serial Server! pollcli: abc This has me confused - it's good it works, but I can't follow in the flow how the paddr gets changed from the value supplied to chardev_map (ie 0x21e80000 becomes 0x1f654), yet in that case it works. Or is it a complication of using QEMU? A similar kind of test with AOS on odroidc4 - particularly the success of "*uart_init@uart.c:35 Mapped uart paddr:ff803000 size:1000 vaddr:b0000000*" ## Starting application at 0x01080000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A55 r1p0 paddr=[88a000..c2b10f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 9f3068. Loaded DTB from 9f3068. paddr=[247000..252fff] ELF-loading image 'kernel' to 0 paddr=[0..246fff] vaddr=[ffffff8000000000..ffffff8000246fff] virt_entry=ffffff8000000000 ELF-loading image 'sos' to 253000 paddr=[253000..48cfff] vaddr=[400000..639fff] virt_entry=4172e0 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space SOS Starting... <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> uart_init@uart.c:35 Mapped uart paddr:ff803000 size:1000 vaddr:b0000000 SOS Started! test_cspace@tests.c:59 Test cspace run_tests@tests.c:174 Root CSpace test passed! test_cspace@tests.c:59 Test cspace run_tests@tests.c:182 Single level cspace test passed! test_cspace@tests.c:59 Test cspace cspace_alloc_slot@cspace.c:335 Cspace is full! run_tests@tests.c:195 Double level cspace test passed! run_tests@tests.c:199 DMA test passed! run_tests@tests.c:203 Frame table test passed! Network init dwmac.b0002000 Waiting for PHY auto negotiation to complete........ done Speed: 1000, full duplex Protocol ethernet registered (layer: 2). Protocol ipv4 registered (layer: 3). Protocol ipv6 registered (layer: 3). Protocol icmp4 registered (layer: 4). Protocol icmp6 registered (layer: 4). Protocol igmp registered (layer: 4). Protocol udp registered (layer: 4). Protocol tcp registered (layer: 4). Assigned ipv4 0.0.0.0 to device sos picotcp DHCP client: update link Assigned ipv4 192.168.200.125 to device sos picotcp DHCP client: renewal time (T1) 43200 DHCP client: rebinding time (T2) 75600 DHCP client: lease time 86400 DHCP client: netmask 255.255.255.0 DHCP client: gateway 192.168.200.4 Timer init Start first process Starting ttytest at 0x4001c8 SOS entering syscall loop aos: Error attempting syscall 29 task: Hello world, I'm tty_test! handle_syscall@main.c:128 Unknown syscall 1 <<seL4(CPU 0) [receiveIPC/148 T0xffffff803fff8400 "SOS:root" @407a48]: Reply obj ect already has unexecuted reply!>> In this case it has worked, sos_map_device works as expected (although the spurious interrupts are another task to figure out). But trying to understand what's really going on underneath ps_io_map and ultimately why libplatsupport won't work for me has got me confused. Any ideas would be appreciated. Regards Rob

2 4

camkes-vm-linux kernel example
by Hugo V.C. 01 Jul '21

01 Jul '21

Hi, just a simple question: why this tutorial: https://docs.sel4.systems/Tutorials/camkes-vm-linux.html shows this output: Welcome to Buildroot buildroot login: root Password: # grep poke /proc/devices # figure out the major number of our driver 244 poke # mknod /dev/poke c 244 0 # create the special file # echo > /dev/poke # write to the file [ 57.389643] hi -sh: write error: Bad address # the shell complains, but our module is being invoked! I'm not getting the shell complain error, just this: # grep poke /proc/devices 247 poke # mknod /dev/poke c 247 0 # echo > /dev/poke [ 138.946905] TOC TOC NEO... # FYI: my kernel is a custom compiled one but same version as the pre-compiled you provide: # uname -a Linux buildroot 4.9.189 #4 SMP Thu Jun 24 00:16:49 CEST 2021 aarch64 GNU/Linux Any hint? Cheers,

2 2

How will drivers work?
by Isaac Beckett 01 Jul '21

01 Jul '21

Hello! Operating system noob here, I understand that in most mainstream operating systems (Linux, BSDs, MacOS, Windows) drivers are part of the kernel. And in micro kernel operating systems like Minix and seL4, drivers are part of user space. But Minix is a lot closer to a traditional POSIX kernel, and seems to implement some of that (IE posix threads, IPC) in the kernel, which makes the environment for a driver programmer a bit more familiar. How do drivers work in seL4, then? How does a driver obtain permission for hardware access from the kernel? I imagine it works with a capability delegated by the root task, but how do you solve chicken and the egg type problems, like loading driver code, without driver code already loaded? Is it an initramfs like Linux/Unix? Also, what if seL4 is being used _as_ the firmware/bootloader? Obviously it can load the seL4 kernel and user space OS components from a file system to put them in the booting OS’ memory, but how does it load drivers for itself? I’m assuming there’s some low level platform specific code, but is that code verified or part of the proofs?

2 1

Re: Tutorial Problem
by Peter Chubb 30 Jun '21

30 Jun '21

>>>>> "Michael" == Michael Neises <neisesmichael(a)gmail.com> writes: Michael> Peter, When I try to remove vme from the -cpu line, I get the Michael> following error at simulation time: OK, so you need nested virtualisation. That's not supported in code-translation mode, only when you're using the KVM kernel module. The message you got was about the simulated CPU, not your host. If you can enable KVM, qemu will pass through your host to the simulation. Looks like you have the kernel packages installed, now you need to make sure that: 1, The version of qemu you're using supports KVM, and 2. you have permissions to use KVM. The first is easy. On Debian-derived systems (debian, ubuntu, mint, etc) sudo apt install qemu-kvm should do the trick. Similarly sudo yum install qemu-kvm on Redhat-derived systems. The second is a little harder. Do ls -l /dev/kvm You'll see something like crw-rw----+ 1 root kvm 10, 232 Jun 30 09:13 /dev/kvm if kvm is installed. The second username (in this case, 'kvm') is the group you need to be in. Do sudo useradd your-login kvm (replacing 'kvm' with the actual group /dev/kvm is in, and 'your-login' with you local login name.) qemu-system-x86_84 -enable-kvm should then work. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0

Tutorial Problem
by Michael Neises 30 Jun '21

30 Jun '21

Hello everyone, The tutorials provided here are failing to build for me: https://github.com/seL4/sel4-tutorials Here are the steps to reproduce the errors: git clone git@github.com:seL4/seL4-CAmkES-L4v-dockerfiles.git && git clone git@github.com:seL4/sel4-tutorials.git && make -C ./seL4-CAmkES-L4v-dockerfiles user HOST_DIR=$(pwd)\ followed by cd sel4-tutorials && mkdir build && cd build && ../init.py --plat pc99 --tut camkes-vm-linux Then I am met with the error: ERROR:root:Parent directory is not tutorials root directory which I can fix by changing this line to read "init.py": https://github.com/seL4/sel4-tutorials/blob/d040028999b83c6af2309785f746810… Trying again after this edit, I meet the following errors: loading initial cache file ../projects/sel4-tutorials/settings.cmake CMake Error: Error processing file: ../projects/sel4-tutorials/settings.cmake CMake Error: The source directory "/host/sel4-tutorials/build" does not appear to contain CMakeLists.txt. Specify --help for usage, or press the help button on the CMake GUI. Traceback (most recent call last): File "../init.py", line 90, in <module> sys.exit(main()) File "../init.py", line 78, in main result = common.init_directories(args.plat, args.tut, args.solution, File "/host/sel4-tutorials/common.py", line 101, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/host/sel4-tutorials/common.py", line 69, in _init_build_directory return sh.cmake(args + [tute_directory], _cwd=directory, _out=output, _err=output) File "/usr/local/lib/python3.8/dist-packages/sh.py", line 1520, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python3.8/dist-packages/sh.py", line 784, in __init__ self.wait() File "/usr/local/lib/python3.8/dist-packages/sh.py", line 841, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python3.8/dist-packages/sh.py", line 865, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/bin/cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DFORCE_IOMMU=ON -DTUTORIAL_DIR=build -C ../projects/sel4-tutorials/settings.cmake /host/sel4-tutorials/build STDOUT: STDERR: Either I'm missing something obvious or these instructions have fallen out of date. In any case I would be grateful for any advice. Best, Michael Neises

4 5

How to avoid seL4 passing packets to Linux VM guest
by Hugo V.C. 25 Jun '21

25 Jun '21

Hi, I wonder how to have seL4 host not passing network frames to Linux VM guest. I mean, I would like to have seL4 dealing with TCP/IP and processing packets at the host level but then I want to use a custom communication channel with the Linux guest. So, the very first step would be to stop forwarding network frames to the guest. Any hint where I can start experimenting with this? Cheers,

2 4

Some small details in kernel code and docs
by Mark Jones 24 Jun '21

24 Jun '21

Hi All, Here are a few minor details/questions about the kernel code & documentation. (I've confirmed that these are present in the new seL4-12.1.0 release.) 1) kernel/include/arch/x86/arch/32/mode/machine.h has the following definition (some code elided): static inline word_t FORCE_INLINE x86_read_fs_base_impl(void) { word_t base = 0; base &= ...; base &= ...; base &= ...; return base; } I'm pretty sure that the three &= operators here should be |= or else the result is always going to be zero. The same issue occurs in x86_read_gs_base_impl in the same file. Some follow-up questions: Can anyone say if this would have been detected if the PC99 (32-bit) platform had been verified? More generally, where can I find information about how ia32 segment registers are handled by the kernel? Why aren't they just stored/restored like other user-level registers on kernel entry/exit? Is there something that prevents user-level changes in the ES register, for example, from being observed in other threads? 2) A CNodeRotate will generate a FailedLookup error if the pivot slot either doesn't exist or contains a null capability. But, in the first case the "lookup failed for a source capability" field in the error message is 1, while in the second it is 0. Hardly a serious problem, but this does seem inconsistent. Is this intentional, or a mistake in the specification that has been carried over to the implementation? 3) Section "3.4 Lookup Failure Description" of the manual describes how capability lookup errors are represented in an IPC buffer. But it seems the layout information is incorrect. For example, Section 3.4.2 says that "Offset + 0" will contain seL4_MissingCapability while the number of bits left will be at "Offset + seL4_CapFault_BitsLeft", which is probably supposed to be equivalent to "Offset + 1". But, based on kernel/libsel4/include/sel4/shared_types.h, it would seem that this gives "Offset + 4". Sections 3.4.3 and 3.4.4 have similar problems. 4) On https://docs.sel4.systems/GettingStarted, in the section labeled "Fetching, Configuring and Building seL4test", there are missing line breaks between the commands in the text boxes for Steps 1 and 2, and there are some tags in the text box for Step 4 that probably should not be displayed. Best wishes, and thanks for any feedback! Mark

6 7

CAmkES ARM VM: SATA Passthrough
by Olof Holmberg 21 Jun '21

21 Jun '21

Hi, I ran into the issue of not being able to fit the whole rootfs in RAM (using a qemu-arm-virt device). Therefore I opted for booting the initramfs instead and from there switch root to the proper file system. The booting of the initramfs works fine but the /dev/sda device is not visible to the guest. For x86 (according to these instructions: https://docs.sel4.systems/projects/camkes-vm/) this seems to be done by passing through access to the SATA controller. But since the x86 device configuration is different to the ARM device configuration it requires a different config than the one shown in the instructions. I was wondering how you achieve this SATA passthrough for a ARM VM or if there are any tutorials, other projects or examples that shows how it is done? Best regards, Olof

2 1

Re: Devel Digest, Vol 104, Issue 8
by jonas.cl＠protonmail.com 14 Jun '21

14 Jun '21

Sent from ProtonMail, Swiss-based encrypted email. ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Monday, June 14, 2021 4:00 AM, <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via email, send a message with subject or > body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > Today's Topics: > > 1. sel4 camkes stability (mrshafiei(a)aut.ac.ir) > 2. sel4 camkes stability mechanisms for crash handling and thread failure > (mrshafiei(a)aut.ac.ir) > > > Message: 1 > Date: Sun, 13 Jun 2021 10:47:43 +0430 > From: mrshafiei(a)aut.ac.ir > Subject: [seL4] sel4 camkes stability > To: Siwei.Zhuang(a)data61.csiro.au, devel(a)sel4.systems > Message-ID: 1623565063345060169(a)aut.ac.ir > > Content-Type: text/plain; charset="utf-8" > > Hi Siwei. > I have some problem with my sel4 project, as you know, I'm work on my master project and develop a project on sel4 (camkes) which provide filesystem interfaces, and use ethernet and lwip network stack. This section is ok but sometimes my project crashed and my threads failed. I think that you should start by getting core files from all the crashes. This will point to why the threads fail. I haven't done that for projects running seL4 on hardware, but it is easy to connect gdb to an image running in qemu. I'm sure someone here can point you in the right direction on how to catch core-dump files from hardware. You can of course also implement a watchdog, but start with solving the crashes. /Jonas Claesson > In another words, I wrote my > components and its work correctly but some times (rarely) my threads > crashes and I couldn't find problem. So i decide to use a service like > watch dog timer for garanty all of threads work and when one of therm > failed or crashed, this mechanism detect it and start another thread or > reset the system. > A simple solution can implement is use some thread controlling > (implement WDT in user mode). But I want to know is there in camkes or > sel4 any mechanism for this need? a mechanism for garanti stability and > system availability? > can any body help me? > Is there anybody which confront with this need? > > -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- > > This email was Anti Virus checked by Security Gateway. > > ------------------------------------------------------- > > Message: 2 > Date: Sun, 13 Jun 2021 10:50:18 +0430 > From: mrshafiei(a)aut.ac.ir > Subject: [seL4] sel4 camkes stability mechanisms for crash handling > and thread failure > To: devel(a)sel4.systems > Message-ID: 1623565218534753237(a)aut.ac.ir > > Content-Type: text/plain; charset="utf-8" > > Hi there. > I have some problem with my sel4 project, as > you know, I'm work on my master project and develop a project on sel4 > (camkes) which provide filesystem interfaces, and use ethernet and lwip > network stack. This section is ok but sometimes my project crashed and > my threads failed. > In another words, I wrote my > components and its work correctly but some times (rarely) my threads > crashes and I couldn't find problem. So i decide to use a service like > watch dog timer for garanty all of threads work and when one of therm > failed or crashed, this mechanism detect it and start another thread or > reset the system. > A simple solution can implement is use some thread controlling > (implement WDT in user mode). But I want to know is there in camkes or > sel4 any mechanism for this need? a mechanism for garanti stability and > system availability? > can any body help me? > Is there anybody which confront with this need? > > -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- > > This email was Anti Virus checked by Security Gateway. > > ------------------------------------------------------- > > Subject: Digest Footer > > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems > > > --------------------------------------------------------------------------------------------------- > > End of Devel Digest, Vol 104, Issue 8

1 0

MMC wait after second command in intialization with mmc_init
by MOHAMAD REZA SHAFIEI 13 Jun '21

13 Jun '21

hi there . i'm work on mmc storage with sel4. i wrote a simple app that use mmc an here is that : ////////////////////////////////////////////////////////////////////// static int count = 0; ps_io_ops_t io_ops = {0}; struct netif* net_if; mmc_card_t mmc_card = 0; sdio_host_dev_t sdio_host_dev; int mmc_found = 0; void mmc_irq_handle(ps_irq_t* irq) { printf("mmc irq handle .... \n"); if(!mmc_found){ mmc_irq_acknowledge(irq); // printf("mmc not found yet :)\n"); sdio_host_dev.handle_irq(&sdio_host_dev,irq->irq.number); return ; } mmc_irq_acknowledge(irq); mmc_handle_irq(mmc_card,irq->irq.number); } int run(void) { notification = timer_notification(); int err = camkes_io_ops(&io_ops); if (err != 0) { ZF_LOGF("Can not init ops : %d\n", err); }; printf("initialize sdhc1 ...\n"); err = sdio_init(SDHC1, &io_ops, &sdio_host_dev); // while card not present check while(sdio_host_dev.reset(&sdio_host_dev) == -1){ delay(1000); } printf("before mmc_init\n"); mmc_init(&sdio_host_dev, &io_ops, &mmc_card); mmc_found = 1; printf("after mmc_init\n"); if (!err) { printf("SDHC1 inited successfully.\n"); } else { printf("SDHC1 initizatino failed!: %d", err); } while (true) { printf(".\n"); delay(1000); } return 0; //////////////////////////////////////////////// its work but in mmc_init after going to mmc_reset , first command sent but in second command (ie MMC_SEND_EXT_CSD ) wait for ever... can any body help me? best regards -- This email was Anti Virus checked by Security Gateway.

2 1

lighttpd as non root user in sel4webserver demo
by Hugo V.C. 13 Jun '21

13 Jun '21

Hi, I was trying to run lighttpd as non root user in " https://github.com/seL4/sel4webserver" demo and realized it didn't allowed me no matter if I configured /etc/passwd, /etc/group and /etc/shadow and /etc/lighttpd.conf correctly. As I don't have debug tools in this Linux VM to look what's going on I decided to directly modify the lighttpd source code to bypass some native code of the web server and hardcode my own user/group. Looks like it works and I now have lighttpd running with it's own user: # ps -ef PID USER COMMAND 1 root init (...) 60 root /sbin/syslogd -n 64 root /sbin/klogd -n 108 lighttpd lighttpd -f /etc/lighttpd.conf 110 root /sbin/getty -L tty1 0 vt100 (...) I also changed the ownership of the /run/site tree to be owned by root. The changes I did in the source code are basically to bypass "getgrnam()" and "getpwnam()" syscalls as I suspect for some reason (musl libc guilty??) and manually set the setgid value before the chroot. I know this is a very dirty hack... but it works for me. My question is if anyone thinks this can be useful to others I can create a pull request with the changes. I think that even if this is a demo, it is not nice to run lighttpd as root, even for a static website. Of course the "right"/elegant way of solving this would be not to change lighttpd source code... but I was unable to do that way. Let me know your opinions. Cheers,

1 0

Camkes-vm-linux on
by Hugo V.C. 12 Jun '21

12 Jun '21

Hi, I'm trying the camkes-vm-linux tutorial and can't run it in qemu despite having nested guests enabled: hugo@dev:~/seL4/sel4-tutorials-manifest/camkes-vm-linux_build$ cat /sys/module/kvm_intel/parameters/nested Y --------- hugo@dev:~/seL4/sel4-tutorials-manifest/camkes-vm-linux_build$ sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=split --mem-size 2G --extra-cpu-opts "+vmx" --extra-qemu-args="-enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0" ./simulate: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,+syscall,+lm,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 qemu-system-x86_64: warning: host doesn't support requested feature: CPUID.80000001H:EDX.pdpe1gb [bit 26] qemu-system-x86_64: warning: host doesn't support requested feature: MSR(48FH).vmx-exit-load-perf-global-ctrl [bit 12] qemu-system-x86_64: warning: host doesn't support requested feature: MSR(490H).vmx-entry-load-perf-global-ctrl [bit 13] qemu-system-x86_64: Host doesn't support requested features ./simulate: QEMU failed; resetting terminal in 5 seconds--interrupt to abort --------- any tutorial to build/boot it natively on x86_64? Thanks,

2 1

Clean repo init
by Hugo V.C. 11 Jun '21

11 Jun '21

Hi, I'm trying to start a new "clean" repo init in my "/seL4/sel4webserver" directory so I deleted everything there, then I executed: repo forall -c "git reset --hard HEAD" repo forall -c "git clean -df" the I executed: repo init -u https://github.com/SEL4PROJ/sel4webserver-manifest.git repo sync but when I go to the "/projects/webserver/lighttpd" directory and check the content of local "lighttpd.sh" I see different (old) content than what you can see via web interface here: https://github.com/seL4/sel4webserver/blob/master/lighttpd/lighttpd.sh Specifically, via web interface I can see the recent commit: https://github.com/seL4/sel4webserver/commit/6a98bdcb2be6ffc693325bbb48df9d… but in my local copy of the file I can't see the changes. Is it due to come kind of cache issue of Git...? Does it require some time to be synced what you see via web interface and what you get downloaded via CLI? Am I doing something wrong? Thank you in advance and sorry for this newbie like question. Hugo

3 3

Proving there exists a valid execution of a function
by Ben Fiedler 11 Jun '21

11 Jun '21

Hi seL4 devs, I'm not sure whether this list is the right spot to ask about AutoCorres issues, but I gather you have some experience with that :-) I'm currently working on proving that some CAmkES component behaves well wrt some higher- level specification. I want to prove this by simulation: Each step of my concrete CAmkES code corresponds to a step of some abstract machine. I've proven the behavioural lemmas as Hoare-triples using the validNF framework, and now want to lift the AutoCorres-generated executions to my higher-level representation. I'm having issues with this however. Concretely, I want to be able to extract some resulting state after e.g. execution function f. For example: I have the following triple: {| P |} f {| Q |}! Now given a state s such that P s is satisfied, I want to obtain some resulting state s' such that Q' _ s' holds. This is easy enough, as Isabelle has Hilbert's choice operator: fun get_next_state where "get_next_state f s = SOME s'. s' : (snd ` fst (f s))" Here is my problem: The choice operator only works when selecting from a non-empty set. I have a feeling that since I've shown that {P} f {Q} is a non-failing and valid hoare-triple this should somehow follow, but it doesn't. There is an easy counter-example: {| top |} select {} {| toptop |} This is a valid triple, however there are no valid executions for `select {}`. I have a feeling that this is the only counterexample though, since all other potential sources of empty executions are covered (namely nonterminating while loops, as they must always terminate in the validNF framework). If `select A` included a guard that A is non-empty, then I believe one could show that vaildNF P f Q implies exs_valid P f Q, although I'm not sure on this. I've looked into the exs_valid framework, which proves exactly what I want. However, I have two issues with this: 1. I have already proven all the invariants I wanted in the validNF framework, and repeating these proofs seems redundant to me. 2. The exs_valid framework has very little utilities provided for use with the wp tool, which makes working with it more tedious than the validNF framework. Another avenue I've looked at is using termination proofs from the SIMPL code: The AutoCorres ac_corres lemmas derived for my functions guarantee termination of the concrete SIMPL code if the abstract version does not fail, which I have proven. Since, as far as I understand it, the SIMPL layer has no problematic `select`-equivalent, termination should be sufficient to guarantee that a following state actually exists, and somehow lifting that guarantee to the AutoCorres layer. I haven't had success with this though. Any help/pointers is appreciated. Thanks a lot in advance! Cheers, Ben

1 1

Increase Initrd Max Size Beyond DTB Address Limitation
by Olof Holmberg 10 Jun '21

10 Jun '21

Hi, I was wondering if there is a way to increase the RAM size of the Initrd in the qemu-arm-virt VM to more than the initially allowed which seems to be around 250MB. These are my current settings for the VM RAM: #define VM_RAM_OFFSET 0x00000000 #define VM_INITRD_MAX_SIZE 0x9000000 // 150 MB #define VM_RAM_BASE 0x40000000 #define VM_RAM_SIZE 0x20000000 #define VM_DTB_ADDR 0x4F000000 // VM0_RAM_BASE + 0xF000000 #define VM_INITRD_ADDR 0x46000000 // VM0_DTB_ADDR - VM_INITRD_MAX_SIZE And what I would want is something like this: #define VM_RAM_OFFSET 0x00000000 #define VM_INITRD_MAX_SIZE 0x20000000 // 500 MB #define VM_RAM_BASE 0x40000000 #define VM_RAM_SIZE 0x30000000 #define VM_DTB_ADDR 0x6F000000 // VM0_RAM_BASE + 0xF000000 #define VM_INITRD_ADDR 0x4F000000 // VM0_DTB_ADDR - VM_INITRD_MAX_SIZE VM_DTB_ADDR should probably be 0x4F000000. If I interpreted it correctly it means that the VM_INITRD_ADDR will be below the VM_RAM_BASE_ADDR and therefore outside of the allocated memory for the VM. But I assume that the comments regarding the address of the DTB that it is not possible to have a larger size of Initrd than the difference between VM_DTB_ADDR and the VM_RAM_BASE allows for. I have tested with some different configurations and it either results in the boot hanging after touching the pages for the VM or results in a page error during the touching of pages. It however seems to work with having the VM_INITRD_MAX_SIZE larger than what could fit between the base and Initrd address but I assume that it would result in an error should the actual loaded initramfs require the whole allocated space. What would be the correct way to achieve this if it is even possible? I assume that it might not even be possible if the addresses that has to be allocated for the larger Initrd is already used and allocated for other things. Best regards, Olof

1 0

Running vm_multi on TK1 and TX2
by Mike Clark 10 Jun '21

10 Jun '21

The camkes-vm-examples readme mentions that the Nvidia TX2 should support multiple VMs but it is untested. If you try to build the vm_multi app for TX2 you just get an error that the platform is unsupported. Has anyone tried vm_multi on TX2? Do you have a working devices.camkes that you can share? On the TK1 board, the readme says multiple VMs is unsupported, but in the Notes it says that Multi-VM is untested. Could multi-vm work for TK1? Mike

1 0

Bug when compling in release mode
by Ben Fiedler 09 Jun '21

09 Jun '21

Hello everyone, I've recently found an interesting bug that only occurs when compiling in release mode. Use of the ZF_LOG library (for normal log output) leads to syscalls being made when the capdl-loader runs. These are invoked via musllibc's __stdio_write, which relies on __sysinfo being set correctly for syscalls to work. When compiling with RELEASE=OFF this works fine, however when compiling with RELEASE=ON, __sysinfo is not set (yet?), and subsequently leads to an illegal prefetch exception when __stdio_write tries to invoke a syscall. Setting __sysinfo to sel4_vsyscall using gdb during runtime fixes this. I don't really know the correct place to fix this in the code, but I hope that you can provide some hints on where to fix this bug. Thanks a lot for your help! Cheers, Ben

2 2

Pull request of S91lighttpd
by Hugo V.C. 08 Jun '21

08 Jun '21

Hi, I'm trying to make a pull request as I want to make a very simple (yet useful) change to S91lighttpd file. I wonder where I can find this file in Git as I can find it locally in my build directory: build/overlay/etc/init.d/S91lighttpd but can not find it anywhere else in Git. I assume it is part of some prebuilt file system (overlay?) but still I can't find where this file system is in Git. Any help will be appreciated. Hugo

2 2

Status of the seL4 RISC-V platform Rocketchip
by Axel Heider 07 Jun '21

07 Jun '21

Hi, I'm wondering about the state of the seL4 RISC-V platform "Rocketchip", is anybody actively using this? At the seL4 hardware status page https://docs.sel4.systems/Hardware/rocketchip.html there is not much, and the repo https://github.com/ucb-bar/fpga-zynq has been abandoned. It points to https://github.com/sifive/freedom which has also been abandoned recently. So I wonder, is this platform effectively dead and should be removed? Axel

1 0

watch dog timer and stability mechanisms in sel4 and camkes
by MOHAMAD REZA SHAFIEI 05 Jun '21

05 Jun '21

Hi there. i'm working on my master project and try to implement a system which act as a storage system (a simple sample). so i write my components and its work correctly but some times (rarely) my threads crashes and I couldn't find problem. So i decide to use a service like watch dog timer for garanti all of threads work and when one thread failed and crashed, this mechanism detect it and start another thread or reset the system. My project is on sle4 and camkes framework, a simple solution can implement by some thread controlling (implement WDT in user mode). But I want to know is there in camkes or sel4 any mechanism for this need? a mechanism for garanti stability and system availability? can any body help me? Is there anybody which confront with this need? -- This email was Anti Virus checked by Security Gateway.

1 0

libsel4utils: load_segment memory leak bug
by wzt wzt 05 Jun '21

05 Jun '21

hello: i found a bug memory leak bug in libsel4utils/src/elf.c static int load_segment(vspace_t *loadee_vspace, vspace_t *loader_vspace, vka_t *loadee_vka, vka_t *loader_vka, const char *src, size_t file_size, int num_regions, sel4utils_elf_region_t regions[num_regions], int region_index) { seL4_CPtr loader_slot; cspacepath_t loader_frame_cap; error = vka_cspace_alloc(loader_vka, &loader_slot); [1] while (pos < segment_size && error == seL4_NoError) { reservation_t reservation; if (loadee_vaddr < region.reservation_vstart) { if ((region_index - 1) < 0) { ZF_LOGE("Invalid regions: bad elf file."); return 1; [2] } } if [2] happned, it not free the prev alloc memory, and then it's memory will be leaked. i think the correct way is invoke vka_cspace_free() before return.

3 2

Mapping VM Kernel Memory
by Michael Neises 05 Jun '21

05 Jun '21

Hello everyone, I have a question about some code I'm using from the seL4 repositories. I have a follow-up question about whether a certain memory mapping strategy is feasible. I'm looking at this kernel module: https://github.com/seL4/camkes-vm-linux/blob/master/camkes-linux-artifacts/… and at this user-space app: https://github.com/seL4/camkes-vm-linux/blob/master/camkes-linux-artifacts/… In short, there is shared memory between a camkes component and the vm-linux. I can tell that the shared memory region is given by accessing /dev/uio0. However, it's not clear to me what exactly this memory region is. As I simulate the kernel, I find this: [ 0.000000] Virtual kernel memory layout: [ 0.000000] modules : 0xffff000000000000 - 0xffff000008000000 ( 128 MB) [ 0.000000] vmalloc : 0xffff000008000000 - 0xffff7dffbfff0000 (129022 GB) [ 0.000000] .text : 0xffff000008080000 - 0xffff0000087d0000 ( 7488 KB) [ 0.000000] .rodata : 0xffff0000087d0000 - 0xffff000008a50000 ( 2560 KB) [ 0.000000] .init : 0xffff000008a50000 - 0xffff000008e00000 ( 3776 KB) [ 0.000000] .data : 0xffff000008e00000 - 0xffff000008f31200 ( 1221 KB) [ 0.000000] .bss : 0xffff000008f31200 - 0xffff000008fb9034 ( 544 KB) [ 0.000000] fixed : 0xffff7dfffe7fb000 - 0xffff7dfffec00000 ( 4116 KB) [ 0.000000] PCI I/O : 0xffff7dfffee00000 - 0xffff7dffffe00000 ( 16 MB) [ 0.000000] vmemmap : 0xffff7e0000000000 - 0xffff800000000000 ( 2048 GB maximum) [ 0.000000] 0xffff7e0000000000 - 0xffff7e0000200040 ( 2 MB actual) [ 0.000000] memory : 0xffff800000000000 - 0xffff800008001000 ( 128 MB) My belief is that /dev/uio0 points to the section here labeled "memory." Is that right? My goal is to perform memory introspection on vm-linux kernel modules. To that end, I think I want to look at the section labeled "modules." Is that possible? Best, Michael Neises

1 0

QEMU simulation: Passing drive to CAmkES ARM VM
by Olof Holmberg 04 Jun '21

04 Jun '21

Hi, I am currently booting a initramfs as the VM so that I later would be able to switch root to a filesystem disk that allows for larger storage and has other software installed that I want inside the VM. I have started the simulate script with a few variants of the following line (Passing the virtio device was a guess since the virtio-net device is supported for networking for the VM. I have also tried to pass only the drive part but it has the same result.): sudo ./simulate --extra-qemu-args="-device virtio-blk-pci,drive=drive0 -drive file=filesystem/testimage,format=raw,if=none,id=drive0" However there are no devices appearing in /dev/ that seem to be the drive passed to qemu such as sdaX or vdaX. There is no output from running "fdisk -l" either. So therefore I wonder if this kind of passthrough is supported by seL4? I have tried to find documentation that relates passing a disk to the VM in seL4 but have not found anything yet. This was done for the qemu-arm-virt platform if that has some significance regarding platform support. Best regards, Olof

2 2

Running ninja twice fails in https://github.com/seL4/sel4webserver
by skydivebcn＠gmail.com 04 Jun '21

04 Jun '21

Hi, I have noticed I'm never unable to run "ninja" for a second time and I'm required to rm -rf all the contents of "build" directory, and run "../init-build.sh" again before running ninja again. If I try to simpley run "ninja" twice the error I get is: (...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated (many times...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /home/hugo/seL4/sel4webserver/build/docsite-prefix/src/docsite/_plugins/include_absolute.rb:71: warning: Using the last argument as keyword parameters is deprecated done in 10.04 seconds. Auto-regeneration: disabled. Use --watch to enable. ninja: build stopped: subcommand failed. Any hint on what could be happening? Anyone else having same issue? I'm doing something wrong?

3 5

VGA pass-through using CAmkES VM on x86
by Nicholas Pahl 03 Jun '21

03 Jun '21

Hello all, I am working out of a CAmkES VM manifest and have a function build running on an x86 platform. I have successfully pass-through various PCIe devices (Ethernet, Sata, USB) to a RHEL8 VM. I am attempting to pass-through the VGA controller in the same way as the other PCIe devices, but I am running into errors. I am assuming VGA pass-through requires more effort than just passing the PCIe device through. If anyone has any tips for VGA pass-through or an example CAmkES project that would be greatly appreciated. Also, if anyone has VESA framebuffer pass-through working I would also be interested. I have tried using LibSel4VMMPlatsupportVESAFrameBuffer but have not had any success getting a VM to use it. The card I am trying to pass-through is a Radeon HD 3450. The kernel log's call stack indicates that it is getting into radeon initialization functions, so it does see the VGA controller on the bus. The log seems to be failing to retrieve info from the BIOS. Below is a log of the kernel panic. [ 2.472635] BUG: unable to handle kernel paging request at ffffc90000548480 [ 2.472635] PGD 1013a067 P4D 1013a067 PUD 1013b067 PMD 6fdb8067 PTE 0 [ 2.472635] Oops: 0000 [#1] SMP PTI [ 2.472635] CPU: 0 PID: 349 Comm: systemd-udevd Not tainted 4.18.0-305.el8.x86_64 #1 [ 2.472635] RIP: 0010:radeon_card_posted+0x147/0x200 [radeon] [ 2.472635] Code: 48 8b 83 e8 01 00 00 48 89 c1 83 fa 38 74 53 83 fa 26 0f 87 09 ff ff ff 83 fa 11 76 4d 8b 90 80 60 00 00 48 8b 83 e8 01 00 00 <8b> 80 80 68 00 00 09 d0 a8 01 74 9f 5b b8 01 00 00 00 5d 41 5c c3 [ 2.472635] RSP: 0018:ffffc900005f7960 EFLAGS: 00010202 [ 2.472635] RAX: ffffc90000541c00 RBX: ffff888014950000 RCX: ffffc90000541c00 [ 2.472635] RDX: 0000000016dd1440 RSI: 0000000000000296 RDI: ffff888014950000 [ 2.472635] RBP: ffffc900005f79d8 R08: 0000000000000002 R09: 0000000000000000 [ 2.472635] R10: ffffc900005f79c8 R11: ffffc90000541000 R12: 0000000000000000 [ 2.472635] R13: ffff888014951d90 R14: 0000000000000000 R15: ffff888014950000 [ 2.472635] FS: 00007fe597ad8180(0000) GS:ffff88806fc00000(0000) knlGS:0000000000000000 [ 2.472635] CS: 0010 DS: 0000 ES: 0000 CR0: 0000000080050033 [ 2.472635] CR2: ffffc90000548480 CR3: 0000000016444000 CR4: 00000000000006b0 [ 2.472635] Call Trace: [ 2.472635] igp_read_bios_from_vram+0x18/0xa0 [radeon] [ 2.472635] radeon_get_bios+0x2be/0xf10 [radeon] [ 2.472635] ? __debugfs_create_file+0xc1/0x120 [ 2.472635] ? __debugfs_create_file+0xd5/0x120 [ 2.472635] ? mutex_lock+0xe/0x30 [ 2.472635] ? drm_debugfs_create_files+0x104/0x120 [drm] [ 2.472635] r600_init+0x2b/0x5c0 [radeon] [ 2.472635] radeon_device_init+0x5e7/0xb70 [radeon] [ 2.472635] radeon_driver_load_kms+0x8d/0x240 [radeon] [ 2.472635] drm_dev_register+0xc6/0x1b0 [drm] [ 2.472635] radeon_pci_probe+0x12a/0x1d0 [radeon] [ 2.472635] ? __pm_runtime_resume+0x54/0x70 [ 2.472635] local_pci_probe+0x41/0x90 [ 2.472635] pci_device_probe+0x105/0x1c0 [ 2.472635] really_probe+0x255/0x4a0 [ 2.472635] driver_probe_device+0x49/0xc0 [ 2.472635] device_driver_attach+0x50/0x60 [ 2.472635] __driver_attach+0x61/0x130 [ 2.472635] ? device_driver_attach+0x60/0x60 [ 2.472635] bus_for_each_dev+0x77/0xc0 [ 2.472635] ? klist_add_tail+0x3b/0x70 [ 2.472635] bus_add_driver+0x14d/0x1e0 [ 2.472635] ? 0xffffffffc03fd000 [ 2.472635] driver_register+0x6b/0xb0 [ 2.472635] ? 0xffffffffc03fd000 [ 2.472635] do_one_initcall+0x46/0x1c3 [ 2.472635] ? do_init_module+0x22/0x220 [ 2.472635] ? kmem_cache_alloc_trace+0x131/0x270 [ 2.472635] do_init_module+0x5a/0x220 [ 2.472635] load_module+0x14c5/0x17f0 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __do_sys_init_module+0x13b/0x180 [ 2.472635] __do_sys_init_module+0x13b/0x180 [ 2.472635] do_syscall_64+0x5b/0x1a0 [ 2.472635] entry_SYSCALL_64_after_hwframe+0x65/0xca [ 2.472635] RIP: 0033:0x7fe5966b680e [ 2.472635] Code: 48 8b 0d 7d 16 2c 00 f7 d8 64 89 01 48 83 c8 ff c3 66 2e 0f 1f 84 00 00 00 00 00 90 f3 0f 1e fa 49 89 ca b8 af 00 00 00 0f 05 <48> 3d 01 f0 ff ff 73 01 c3 48 8b 0d 4a 16 2c 00 f7 d8 64 89 01 48 [ 2.472635] RSP: 002b:00007ffc53efb408 EFLAGS: 00000246 ORIG_RAX: 00000000000000af [ 2.472635] RAX: ffffffffffffffda RBX: 00005626ca9314d0 RCX: 00007fe5966b680e [ 2.472635] RDX: 00007fe59722486d RSI: 00000000002c4878 RDI: 00005626cb200450 [ 2.472635] RBP: 00007fe59722486d R08: 00005626ca91501a R09: 0000000000000005 [ 2.472635] R10: 00005626ca915010 R11: 0000000000000246 R12: 00005626cb200450 [ 2.472635] R13: 00005626ca92d120 R14: 0000000000020000 R15: 0000000000000000 [ 2.472635] Modules linked in: radeon(+) i2c_algo_bit drm_kms_helper syscopyarea sysfillrect sysimgblt fb_sys_fops ttm drm ahci libahci e1000e(+) libata crc32c_intel dm_mirror dm_region_hash dm_log dm_mod fuse [ 2.472635] CR2: ffffc90000548480 [ 2.472635] ---[ end trace a2f824fed053010d ]--- [ 2.472635] RIP: 0010:radeon_card_posted+0x147/0x200 [radeon] [ 2.472635] Code: 48 8b 83 e8 01 00 00 48 89 c1 83 fa 38 74 53 83 fa 26 0f 87 09 ff ff ff 83 fa 11 76 4d 8b 90 80 60 00 00 48 8b 83 e8 01 00 00 <8b> 80 80 68 00 00 09 d0 a8 01 74 9f 5b b8 01 00 00 00 5d 41 5c c3 [ 2.472635] RSP: 0018:ffffc900005f7960 EFLAGS: 00010202 [ 2.472635] RAX: ffffc90000541c00 RBX: ffff888014950000 RCX: ffffc90000541c00 [ 2.472635] RDX: 0000000016dd1440 RSI: 0000000000000296 RDI: ffff888014950000 [ 2.472635] RBP: ffffc900005f79d8 R08: 0000000000000002 R09: 0000000000000000 [ 2.472635] R10: ffffc900005f79c8 R11: ffffc90000541000 R12: 0000000000000000 [ 2.472635] R13: ffff888014951d90 R14: 0000000000000000 R15: ffff888014950000 [ 2.472635] FS: 00007fe597ad8180(0000) GS:ffff88806fc00000(0000) knlGS:0000000000000000 [ 2.472635] CS: 0010 DS: 0000 ES: 0000 CR0: 0000000080050033 [ 2.472635] CR2: ffffc90000548480 CR3: 0000000016444000 CR4: 00000000000006b0 [ 2.472635] Kernel panic - not syncing: Fatal exception [ 2.472635] Kernel Offset: disabled [ 2.472635] ---[ end Kernel panic - not syncing: Fatal exception ]---

1 0

Pass Ethernet device to CAmkES ARM VM when using QEMU
by Olof Holmberg 03 Jun '21

03 Jun '21

Hi, I am currently trying to pass a device for ethernet access through qemu to the vm. However there seems to be some issue since the device is not passed through correctly. I have looked at some resources for guidance on how to solve it: https://github.com/seL4/sel4webserver (webserver example) https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/message/X34TX… (old devel thread) And the important parts for this to work seems to be untyped_mmios for the vm (in devices.camkes for qemu-arm-virt): vm0.untyped_mmios = [ "0x8040000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) /* TODO: QEMU PCI addresses could change - ideally need to decode from pcie node */ "0x10040000:17", // QEMU PCI MMIO "0x3eff0000:16", // QEMU PCI IO ports "0x40000000:29", // Linux kernel memory regions ]; And passing the device to QEMU in the simulation script: $ sudo ./simulate --extra-qemu-args="-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01" However when listing the devices with "ip a" on the VM it does not show an eth0 device: # ip a 1: lo: <LOOPBACK,UP,LOWER_UP> mtu 65536 qdisc noqueue qlen 1 link/loopback 00:00:00:00:00:00 brd 00:00:00:00:00:00 inet 127.0.0.1/8 scope host lo valid_lft forever preferred_lft forever inet6 ::1/128 scope host valid_lft forever preferred_lft forever 2: tunl0@NONE: <NOARP> mtu 1480 qdisc noop qlen 1 link/ipip 0.0.0.0 brd 0.0.0.0 3: ip6tnl0@NONE: <NOARP> mtu 1452 qdisc noop qlen 1 link/tunnel6 00:00:00:00:00:00:00:00:00:00:00:00:00:00:00:00 brd 00:00:00:00:00:00:00:00:00:00:00:00:00:00:00:00 But on the host the device that is passed to qemu can be seen: $ ip link show tap0 6: tap0: <BROADCAST,MULTICAST> mtu 1500 qdisc noop state DOWN mode DEFAULT group default qlen 1000 link/ether 62:43:43:54:2d:e6 brd ff:ff:ff:ff:ff:ff I am not sure if I missed something or if it is the QEMU addresses for the pci region that are not correct. Is there any output during boot or build that could give insight in what went wrong when it tries to passthrough the device? Also are there are any resources or guidelines on how to decode the pcie node? (Since I assume this has to be done inside the vm with the limited selection of commands available). Best regards, Olof

1 1

Blocking and unblocking under the MCS kernel
by Robert Kaiser 02 Jun '21

02 Jun '21

Hi all, I'm working on the SOS example of the AOS course, trying to adapt code that used to work under the non-MCS kernel to the now used MCS kernel. So far, this mostly works. However, I'm having problems in resuming a thread that is blocked in an IPC Call operation. In simple cases where the server can reply immediately, the thread is successfully unblocked, simply by replying to the reply object as with the reply capability in the non-MCS kernel. However, if the server does not respond immediately, (i.e. it leaves the calling thread in blocked state, serves some other requests and/or notifications in the meantime, then comes back to reply), replying to the reply object silently fails to unblock the thread for some reason. In the non-MCS kernel, it was necessary in these cases to save the reply capability in a cspace. Therefore I tried to similarly copy/move the reply object to a thread-specific cspace slot, but that doesn't help. I'm sure I'm missing something very basic here. Can anybody point me to the right direction? Best, Robert -- Robert Kaiser Technische Informatik Hochschule RheinMain Wiesbaden Rüsselsheim Computer Engineering RheinMain University of Applied Sciences robert.kaiser(a)hs-rm.de http://www.cs.hs-rm.de/~kaiser tel:(+49)611-9495-1292 fax:(+49)611-9495-1210 Postal Address: Robert Kaiser, Hochschule RheinMain, FB DCSM/Informatik Unter den Eichen 5, 65195 Wiesbaden, Germany

2 2

Easy way to edit VM guest file system
by skydivebcn＠gmail.com 02 Jun '21

02 Jun '21

Hi, I'm learning about this project: https://github.com/seL4/sel4webserver and would like to edit the guest filesystem. Digging around I found some cpio files that looks to me like may be the right place (output_overlay_rootfs.cpio, rootfs.cpio) but I'm not sure. So, as far I understand in theory I can just edit them and the execute "ninja" again. Before going that way, can anyone confirm this is the easiest/right way? Thanks,

3 2

CAmkES Tutorial, check_deps.py - what does good look like?
by Roderick Chapman 02 Jun '21

02 Jun '21

The first CAmkES tutorial points me at the "Usage" section of the CAmkES manual, which tells me to run "./tools/check_deps.py" to see if I have "the appropriate dependencies installed" but I have no idea what that means... What does good look like? I assume I'm supposed to run that from within the Docker container? If I do that, I get the output below, but I have no idea if that's right. I would expect the Docker container to "Pass" this test with flying colours... so I think I might have screwed up somewhere... Can anyone advise please? Thanks, Rod --- rchapman@in-container:/host/sel4-tutorials-manifest/projects/camkes-tool$ tools/check_deps.py Dependencies of CAmkES runner jinja2 (Python templating module)... Not found plyplus (Python parsing module)... Not found ply (Python parsing module)... Not found elftools (Python ELF parsing module)... Not found orderedset (Python OrderedSet module (orderedset))... Not found six (Python 2/3 compatibility layer)... Found sqlite3 (Python SQLite module)... Found pyfdt (Python flattened device tree parser)... Not found You will not be able to build/run this component Dependencies of CAmkES test suite expect (automation utility)... Found pylint (Python linter)... Found qemu-system-arm (ARM emulator)... Found qemu-system-i386 (IA32 emulator)... Found pycparser (Python C parsing module)... Not found gcc (C compiler)... Found spin (model checker)... Found sha256sum (file hashing utility)... Found You will not be able to build/run this component Dependencies of CapDL translator stack (Haskell version manager)... Found Dependencies of seL4 gcc (C compiler)... Found tempita (Python templating module)... Not found xmllint (XML validator)... Found bash (shell)... Found make (GNU Make build tool)... Found cpio (CPIO file system tool)... Found You will not be able to build/run this component Suggestions: c-parser (NICTA C-to-Simpl parser): you will need this installed if you want to validate code for verification clang-format (Clang code reformatter): installing this will reflow generated C code to make it more readable VBoxManage (VirtualBox administration tool): you will need this installed if you want to build VMWare images mformat (formatting tool for MSDOS disks): you will need this installed if you want to build QEMU images for IA32 figleaf (code coverage tool for Python): you will need this installed if you want to measure code coverage within CAmkES python-coverage (code coverage tool for Python): you will need this installed if you want to measure code coverage within CAmkES syslinux (Linux bootloader tool): you will need this installed if you want to build QEMU images for IA32 mpartition (partitioning tool for MSDOS disks): you will need this installed if you want to build QEMU images for IA32 pandoc (document format translator): you will need this if you want to build the CAmkES documentation mcopy (copying tool for MSDOS disks): you will need this installed if you want to build QEMU images for IA32 sponge (input coalescer from moreutils): installing this will give a marginal improvement in compilation times

2 1

Running ninja twice fails in https://github.com/seL4/sel4webserver
by skydivebcn＠gmail.com 02 Jun '21

02 Jun '21

Hi, I have noticed I'm never unable to run "ninja" for a second time and I'm required to rm -rf all the contents of "build" directory, and run "../init-build.sh" again before running ninja again. If I try to simpley run "ninja" twice the error I get is: (...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated (many times...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /home/hugo/seL4/sel4webserver/build/docsite-prefix/src/docsite/_plugins/include_absolute.rb:71: warning: Using the last argument as keyword parameters is deprecated done in 10.04 seconds. Auto-regeneration: disabled. Use --watch to enable. ninja: build stopped: subcommand failed. Any hint on what could be happening? Anyone else having same issue? I'm doing something wrong?

1 0

sel4webserver on qemu
by Hugo V.C. 31 May '21

31 May '21

Hi, I just did a commit: https://github.com/hugusmaximus/sel4webserver/blob/master/README.md so people can test this project without having to use a Odroid-XU4 (myself I had this problem...). Notice that I worked on this repository because in the below tutorial: https://docs.sel4.systems/Tutorials/camkes-vm-linux.html I was failing all the time at running in qemu the x86_64 image. Not sure what was happening there, I fixed many things but still not working, maybe because my laptop is somewhat old (Latitude E6410), and even if VT-x is supported for some reason I was unable to make it work (fixed BIOS disabling trusted execution, had OS nested guests supported, etc). As I think having "easy things to play" is key for people to test seL4 stuff, I think it would be nice to make extra effort to have things working on user available equipment (x86_64, qemu, etc). Having said that, I excuse myself in advance for any mistakes in the pull request process as this is the first time in my life doing this, so any suggestion and corrections will be welcome. Last but not least important I'm very happy to have a working Linux guest on a seL4 running on my laptop as this opens to me a big door for tests so I can build prototypes and test many things hoping that as soon as possible I will have some developer doing this job and building native apps for seL4 to interact with an (isolated) guest. Cheers,

2 2

Troubles with hello-world tutorial
by Roderick Chapman 30 May '21

30 May '21

Hello everyone, I am a newbie with seL4, and trying to get the first hello-world tutorial to build and run. I am a bit stuck on a few issues. 1. I had to add the Python "sh" module before the "init" script would run. 2. It is not clear if the "init" script should be run on my main Linux VM, or within the Docker container. 3. The instructions here https://docs.sel4.systems/Tutorials/hello-world.html and https://docs.sel4.systems/Tutorials/ appear to be contradictory, and neither actually works. It appears that the correct sequence of commands is: 3.1. Start the docker container in the directory above sel4-tutorials-manifest 3.2. In the container: cd sel4-tutorials-manifest mkdir hello-world cd hello-world ../init --plat pc99 --tut hello-world cd ../hello-world_build ninja ./simulate Does that look right? The build finishes with "[181/181] objcopy kernel into bootable elf" although https://docs.sel4.systems/Tutorials/hello-world.html says it should be "[150/150] objcopy kernel into bootable elf" Is that still OK? Should I raise an Issue in GitHub to get the documentation pages updated? All the best, Rod Chapman, Director, Protean Code Limited

8 19

ARM64: Handle SError in user-space instead of halting the kernel
by Indan Zupancic 27 May '21

27 May '21

Hello, By default any SError interrupt will halt the kernel. SErrors may be caused by e.g. writes to read-only device registers or ECC errors. With this patch SErrors can instead be reported as a VM data fault for the currently running task. Because SError is asynchronous it is not assured that the faulting task caused the error. With ARMv8.2 there is a new RAS feature which solves the SError problem for common cases: This patch does not use that, our hardware is v8.0, we need another solution for the SError problem. We would rather log the SError and continue than halt the whole system. As SError is easily triggered by device drivers, halting the whole system would make user-space device drivers not much more reliable than in-kernel ones. I do not know if VMs can also cause SErrors in seL4. However, that seems likely, in which case guest OSes can also halt the whole system. One thing I'm not sure about: SError is edge-triggered, while handleVMFaultEvent() does a MCS_DO_IF_BUDGET check. Does this means that if the current task has no budget, the SError IRQ will be lost? Or are pending faults saved by the schedule code? For us missing the SError would be better than halting the kernel, so it doesn't really matter, but I would like to know. I have an Atlassian account, but it seems you can't attach patches there, so I'm not sure how else to send this patch, other than creating a Github account. What is the preferred way to submit patches as an outsider? Best regards, Indan

4 5

Running seL4Test for RISCV with QEMU
by basho1600＠pm.me 13 May '21

13 May '21

Working on Ubuntu, I have built the seL4Test project for RISCV64. I think. At least, there were no build errors. I have qemu-system-riscv64 installed. But when I get to the ./simulate command, all I get is an echo of "Unsupported platform or architecture for simulation". I configured this test as follows: ../init-build.sh -DPLATFORM=hifive -DRELEASE=FALSE -DSIMULATION=TRUE After the 'ninja' command completes, in the images/ directory there is a 6.6MB file named sel4test-driver-image-riscv-hifive which I am guessing is the resulting image to run, though qemu is not impressed by it, saying that the image format is not specified. Maybe I am just not finding the instructions on how to run this, or what 'simulate' WOULD have contained, had things been working as I expect. Or the complete qemu command line to run it.

2 1

Generating CAmkES glue-spec and glue-proofs
by Ben Fiedler 11 May '21

11 May '21

Hi everyone, I'm having troubles generating the CAmkES glue component specification and proofs from our source. I can and have successfully generated the ADL/CDL spec and implementations using the documented CMake parameters. Grepping around the docs I've found references to a 'camkes.sh' script, but neither the project tree nor the files generated during build contain it. One candidate reason could be that we set up our build environment strangely: We currently check out seL4/camkes-manifest and then symlink our component into the 'projects/global-components' subtree of the seL4. This works for generating bootable images, but I haven't found out how to generate the glue spec yet. Why we have set it up this way I don't know, and I suspect that there is a right way TM that we have overlooked/not found in the documentation. I appreciate any help in this regard. Thanks and have a nice day! Cheers, Ben

4 6

Multiple ARM VMs with different CAmkES component configurations
by Olof Holmberg 11 May '21

11 May '21

Hi, I am currently performing research for my master thesis which involves seL4 and ideally retrofitting a SDN controller application for it. As a part of retrofitting applications for seL4 the suggested way is the incremental cyber retrofit approach wich involves dividing subsystems of the application onto several VMs that each runs in a VMM. Therefore I was wondering if it is currently possible to run several VMs on the ARM architecture that has different component configurations in CAmkES? (ARM is mostly preferable for the simple simulation in QEMU when building for qemu-arm-virt, so switching architecture is an option if this is not achievable) I noted that the macros for VMs on x86 and ARM were different when defining components: x86: /* VM and per VM componenents */ #define VM_PER_VM_COMPONENTS(num) \ component Init##num vm##num; \ /**/ ARM: #define VM_COMPONENT_DEF(num) \ component VM vm##num; \ And to clarify using the vm-examples where in the optiplex9020.camkes there are two VMs that are configured differently: component Init0 { dataport Buf(STRING_REVERSE_BUFSIZE) dp1; dataport Buf(STRING_REVERSE_BUFSIZE) dp2; emits Ready ready; consumes Done done; has mutex cross_vm_event_mutex; VM_INIT_DEF() } component Init1 { VM_INIT_DEF() } But in the ARM vm_multi.camkes there is only one VM component that is used for all three VMs: component VM { VM_INIT_DEF() maybe uses VirtQueueDev recv1; maybe uses VirtQueueDrv send1; maybe uses VirtQueueDev recv2; maybe uses VirtQueueDrv send2; attribute vswitch_mapping vswitch_layout[] = []; attribute string vswitch_mac_address = ""; } So it is at least it is not as simple as defining Init##num components for ARM since currently only one VM component is allowed in the macros. Do you have a recommended way that could achieve a CAmkES structure that allows for multiple differently configured VMs for ARM without altering the macros? If it is not possible at the time I assume that switching to x86 is the easiest alternative to achive this? Best regards, Olof

2 2

CAmkES Access to TCBs
by John Shackleton 06 May '21

06 May '21

I am attempting to develop a userland scheduler to manage the release times and deadlines of other threads executing in the system. I would like to use CAmkES as much as possible, since it abstracts away many messy and error-prone details. Question: How do we specify in CAmkES that a scheduler component has access to TCBs of other CAmkES components? Thanks, -John

1 0

Reducing memory footprint - RISC-V
by porter.188＠osu.edu 19 Apr '21

19 Apr '21

I'm trying to build a low memory footprint of RISC-V based seL4. I'm using QEMU/spike for now. In seL4 12.0 I can modify spike.dts to 8.5 MB of memory 0x00880000. 42 memory@80000000 { 43 device_type = "memory"; 44 reg = <0x00000000 0x80000000 0x00000000 0x00880000>; 45 }; This is the smallest value that builds, lower than this I get the error: [0/1] Re-running CMake... -- Found GCC with prefix riscv64-unknown-linux-gnu- STATUS,KernelDTSList: tools/dts/spike.dts -- /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... STATUS,platform_yaml: /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml -- Detecting cached version of: musllibc -- Found valid cache entry for musllibc -- Configuring done -- Generating done -- Build files have been written to: /mnt/data/femur_12.0/build [18/36] Generating gen_headers/image_start_addr.h FAILED: elfloader-tool/gen_headers/image_start_addr.h cd /mnt/data/femur_12.0/build/elfloader-tool && sh -c "/mnt/data/femur_12.0/tools/elfloader-tool/../cmake-tool/helpers/shoehorn.py /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml /mnt/data/femur_12.0/build/elfloader-tool/archive.o > /mnt/data/femur_12.0/build/elfloader-tool/gen_headers//image_start_addr.h" shoehorn: fatal error: ELF-loader image "/mnt/data/femur_12.0/build/elfloader-tool/archive.o" of size 0x107548 does not fit within any memory region described in "{'devices': [{'end': 2147483648, 'start': 0}, {'end': 549755809792, 'start': 2155872256}], 'memory': [{'end': 2155872256, 'start': 2149580800}]}" ninja: build stopped: subcommand failed. What do I need to modify to get to < 2 MB? Thanks!

4 8

seL4 Crowdsourcing Portal
by Gernot Heiser 15 Apr '21

15 Apr '21

Dear seL4 community, It is a pleasure to announce that seL4 now has a crowdsourcing portal, using the Linux Foundation’s LFX platform. Please help making seL4 stronger by donating, and encouraging others to do the same! https://crowdfunding.lfx.linuxfoundation.org/projects/e94c998c-bac2-4224-b0… Gernot

1 0

Choosing correct hardware platform for CAmkES-arm-vmm Cross VM connector support
by Zohra Charania 15 Apr '21

15 Apr '21

Hi everyone, I am a PhD student. For my research, I want to use sel4 and developa system based on it. The idea is to use the arm based multi VM and cross VM communication ability of sel4 and provide a secure and isolated environment for the various applications running on the system. I was reading through the sel4 tutorials and documentation to find out which hardware would be suitable for this. I started learning sel4 with Raspberry Pi 3, but as Rpi3 does not have GICv2 or GICv3, I am not sure how do I develop the CAmkES-arm-vmm, multi VM and cross VM connector on it. As I wish to develop an application i.e a system architecture using sel4, itwould be good to have a device that provides me the starting point of having a multi VM and Cross VM communication. I read in the documentation that we can use Nvidia TK1-SOM from Colorado engineering to develop CAmkES-arm-vmm. But if I see the table here: _https://docs.sel4.systems/projects/camkes-arm-vm/_ , it says that CrossVM and Multi VM support is unsupported and in notes it says untested. According to the table, this is true for TK1, TX1 and TX2. Could someone please clarify what does this mean? Does it mean that we cannot have these features for these hardware or is it that they are not tested? It will be a great help to get this information, as then I can purchase the correct hardware and advance my work. I am new to micro-kernel community, so I apologize if I have missed anything obvious and would be glad to receive guidance and advice. Hoping for a kind response. Thank you. Sincerely, Zohra

1 0

[seL4 Announce] Operating System based on seL4.
by Gernot Heiser 12 Apr '21

12 Apr '21

<comment> The below message was posted to announce(a)sel4.systems. It was inappropriate for that list, but got though due to a configuration error (now fixed). I’m reposting it here as it would be appropriate for this list. Feel free to respond here. </comment> Hello, Which operating systems are based on seL4 Microkernel? Any home usage? Thanks.

2 1

hello world difficulty
by Royce Mitchell III 09 Apr '21

09 Apr '21

I feel like an idiot for having to ask for help so early, but I'm trying to get started with the hello world tutorial and ran into a problem very quickly. First off I want to say thank you for all the work that's been put into the tutorils. The amount of information in them is quite daunting, but considering the subject matter it's actually very accessible all things considered. I have a Debian 10 linux VM that I'm using for testing. I'm okay building a VM dedicated solely to seL4 development if that's necessary, but I'm assuming it's not. FYI I had some difficulty with the prerequisites instructions regarding Debian. This may be the source of the problem I'm having but I'm not sure how to resolve it. Your setup instructions said to refer to the docker requirements but when I went there I couldn't find anything on that page that indicated what exactly I was supposed to install. All that being said, here is a capture from my terminal which I'm hoping illustrates the problem I'm having specifically: rmitchell@ou812:~/sel4-tutorials-manifest$ ./init --tut hello-world Traceback (most recent call last): File "./init", line 16, in <module> import common File "/home/rmitchell/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 16, in <module> import sh ModuleNotFoundError: No module named 'sh' rmitchell@ou812:~/sel4-tutorials-manifest$ python Python 3.9.1 (default, Mar 19 2021, 01:08:36) [GCC 8.3.0] on linux Type "help", "copyright", "credits" or "license" for more information. >>> import sh >>> sh.__version__ '1.14.1' >>> exit() As you can see from my example above, I have Python 3.9.1 installed and it is the default python interpreter on my system. The "sh" module is installed and accessible from Python's interactive interpreter, yet when the common.py file tries to import it, it complains that it can't find the 'sh' module. FYI sh is installed both at the system and user levels. I'll try digging into your source and see if I can figure out what the issue is. I'll share my findings if I figure it out before you guys point out my mistakes. Thanks! Royce Mitchell, IT Consultant ITAS Solutions royce3(a)itas-solutions.com There are three hard problems in computer science: naming things, and off-by-one errors.

3 6

seL4 service discovery question
by Royce Mitchell III 08 Apr '21

08 Apr '21

Hi all, I've been passively following seL4 for several years. I've been reading the documentation, tutorials, watching YouTube videos. The concepts behind capabilities and other types of kernel objects are starting to sink in but there's one piece of understanding that's eluding me. If I just haven't stumbled across it yet in the documentation, then pointing me in the right direction would be greatly appreciated. Given: * An ethernet driver named "e1000" and 2 devices "eth0" and "eth1" controlled by that driver. * A "tcp" service that would implement that network protocol. * A higher level service named "network" that implemented some kind of networking abstraction for us. How would: 1) the "network" service advertise its services as available via IPC? 2) an application locate this "network" service to be able to IPC with it? I assume the mechanisms here would also apply to interactions between services as well. I picked the "network" service in this example only because it would be the boundary between application and OS services. I'm guessing that maybe this is purely an OS design decision and not the purvue of the kernel itself. Perhaps init could launch a "service manager" process that would be responsible for starting up services and drivers for example and this "service manager" could provide an IPC endpoint back to init (or whomever) to use for IPC discovery. Then, whenever a new process is started, it is provided with the IPC discovery endpoint information that it is to inherit. If my assumptions are correct or close, or even dead wrong, would someone be willing to share some pseudo-code on what this could/should look like in seL4? If a central service manager is needed to glue the core OS together, does it represent a single point of failure and how would the OS recover if it crashes and loses it's database of available services without having to rebuild and restart all drivers and services? (I'm not saying that's a bad thing, just trying to wrap my head around how this particular part of seL4 works) Thanks, Royce Mitchell, IT Consultant ITAS Solutions royce3(a)itas-solutions.com There are three hard problems in computer science: naming things, and off-by-one errors.

6 14

Small question about copiing threads
by Сергей Волкович 07 Apr '21

07 Apr '21

Hello. My name is Serhgey Volkovich. Currently i trying to write my own posix compilant os subset. But i cannot understand some momments such what happen with main process memory if i create new thread with same pointer as it have main, and second process will try to change something in own memory. Will it change memory of main process?

1 0

About the BuildSystem of seL4
by Jerry Zhou 29 Mar '21

29 Mar '21

Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry

2 2

seL4 as bootloader
by Isaac Beckett 29 Mar '21

29 Mar '21

The Linux kernel has support via the EFISTUB module to be loaded directly as an EFI bootloader, which if I recall correctly, also allows it to chainload another OS and be used as a fully-fledged multiboot bootloader. Is it practical to do something similar with seL4? Obviously on non-UEFI platforms it'd be entirely different code, but still.

2 1

About the BuildSystem of seL4
by zhouchunhua＠lixiang.com 26 Mar '21

26 Mar '21

Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry

1 0

About the BuildSystem of seL4
by Jerry Zhou 26 Mar '21

26 Mar '21

Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry

1 0

some confuse about Camkes and AOS sel4
by yadong.li 25 Mar '21

25 Mar '21

hi: I am try to understand the designing philosophy of seL4 kernel base on CAmkES, I didn't find a global memory server in this system But the AOS may be have memory server,even though I am not familiar with AOS now, I have three question: 1. what is the purpose of the existing of CAmkES and AOS meanwhile ? (static and dynamic ) 2. which one (AOS or CAmkES) will be vigorously developed by the seL4 community and fund later. 3. Is a good idea to provide global memory server in CAmkES system? I found usually CAmkES alloc untyped pool Statically for componet in .camkes file. Thank you very much

1 0

Pull requests now directly merged on GitHub
by Gerwin Klein 25 Mar '21

25 Mar '21

The next step in the making contributions easier is now complete: Pull requests for repositories in the seL4 GitHub org can now be merged on GitHub directly, without the loop thought Data61's CI infrastructure. Hopefully this will make merging pull requests faster and less painful. The exception for now are repositories with manifests (such as sel4test-manifest), because parts of these manifests are generated automatically. We're working on moving these as well. The testing and verification regime is the same as before, including extensive hardware tests and proofs, but the results and logs should now be visible directly on GitHub. Happy merging :-) Cheers, Gerwin

1 0

AMD-V Support
by ndaughety13＠gmail.com 24 Mar '21

24 Mar '21

I found "Your host machine has to have a CPU that supports Vt-x virtualization (for Intel CPUs), or AMD-V (for AMD CPUs, but that wasn’t tested)" at https://docs.sel4.systems/projects/camkes-vm/. In context, my understanding is that seL4 should work with AMD-V but it doesn't work on my AMD system. I also do not see any mention of it anywhere else -- not even in the source (could not find amd-v counter part to vtx in grep search of source). Noting that it has not been tested, could this be a build configuration problem or has support not actually been implemented? ...or am I missing something?

1 0

Introduction Ben Fiedler
by Ben Fiedler 19 Mar '21

19 Mar '21

Hello seL4-devs, I'm currently working on a CS MSc thesis at ETH Zurich supervised by David Cock, working on verified low-level system components using seL4 and CAmkES, which I'll be doing until August. I haven't worked with seL4 or CAmkES before, but I have some rudimentary Isabelle/ITP experience from my BSc thesis (mainly typing sledgehammer ;) ). During the course of my thesis I will probably have some questions which I'll post here, and hopefully I can contribute to improving the tooling around seL4+CAmkES verification. Nice to meet you all! Cheers, Ben

2 1

Re: Creating process from not root process
by Seo Yeon Hwang 05 Mar '21

05 Mar '21

Hello, Sorry for bringing this old post up, but could anyone let me know the answer of this post? I’m quite new to seL4 and I’ve been following tutorials and modifying it, and I have the exact same question as this post. Basically, how can I create a process from non-root process? Thanks a lot! Seoyeon Hwang

2 1

Picotcp and Lwip issues on OdroidC2
by ogosinkem＠gmail.com 03 Mar '21

03 Mar '21

Hi, I'm currently trying to include either the picotcp or lwip library into an application in order to connect to or show a connection to a network. As such I have added some lines to some of my files. CMakeLists.txt: DeclareCAmkESComponent(Client SOURCES components/Client/src/main.c LIBS lwip picotcp) hello_world.camkes: component Client{ uses Ethdriver eth_drv; has mutex lwip; control;} When trying to build I get a long error message which boils down to: /usr/lib/gcc-cross/aarch64-linux-gnu/7/../../../../aarch64-linux-gnu/bin/ld: cannot find -llwip /usr/lib/gcc-cross/aarch64-linux-gnu/7/../../../../aarch64-linux-gnu/bin/ld: cannot find -lpicotcp collect2: error: ld returned 1 exit status [258/316] Building C object CMakeFiles/ethdriver.instance.bin.dir/ethdriver/seL4SingleThreadedComponent.template.c.obj ninja: build stopped: subcommand failed. How to I go about solving this issue? Thanks, Nkem

1 0

Ethernet device module for odroidc2
by ogosinkem＠gmail.com 24 Feb '21

24 Feb '21

I have been trying to use the ethernet driver for the UNSW Asdvanced Operating Systems course but I still get these messages: find_compatible_driver_module@io.c:434 No suitable driver was found for path /soc/ethernet@c9410000, ignoring server_init@ethdriver.c:382 Unable to find an ethernet device I thought that I had to copy the driver to the utils lib folder and provide a preprocessor macro as someone else had suggested but I may be missing a few other things. Best, Nkem

3 6

Sporadic Server Implementation Details
by msudvarg＠wustl.edu 11 Feb '21

11 Feb '21

Hi all, I hope this is the right forum to be posting this question. I've reached out to Anna Lyons, the first author on the EuroSys 2018 "Scheduling Context Capabilities" paper (https://ts.data61.csiro.au/publications/csiro_full_text//Lyons_MAH_18.pdf) but I do not know if her listed email address is still active. I want to ask for more clarification on the sporadic server implementation in seL4. My interpretation of how the Lyons et al. paper describes the implementation is different than my understanding of the sporadic server definition as described by Sprunt et al. in 1989 (https://link.springer.com/article/10.1007/BF02341920) However, looking at the seL4 kernel source code, it seems that the actual implementation follows very closely with the improved POSIX sporadic server mechanism described by Stanovic et al. in 2010 (https://www.cs.fsu.edu/~awang/papers/rtas2010.pdf) In particular, the Lyons et al. paper states that when a thread is preempted at time t, a replenishment is scheduled for time t + T. My understanding of the sporadic server is that if a thread becomes active at time t, the replenishment is scheduled for time t + T. In other words, the replenishment is scheduled one period from when the thread begins execution, not when it ends execution. Further, a thread becomes active when it becomes unblocked (i.e. returns from a blocking system call, or is activated by the release of an aperiodic task that it handles). In other words, a thread that is preempted by a higher-priority thread is not considered to have become inactive, according to the sporadic server definition. This seems to be the case in both the Sprunt and Stanovic papers. I think the distinction is significant in a system (like seL4) where only a finite number of replenishments are tracked. Determining what number of replenishments each thread’s server must track is much easier if only voluntary yielding of the processor, and not preemption by higher-priority threads, triggers a replenishment. Can somebody explain to me in more detail how the sporadic server has been implemented in seL4? Like I said, from my reading of the kernel source, it seems that it has been implemented according to the improved POSIX sporadic server detailed by Stanovic, but I’m not certain that I’ve identified all conditions that cause a replenishment to be scheduled.

3 2

Use sel4 and mmc for storage but sdhc driver wait for SDHC_PRES_STATE_CIHB | SDHC_PRES_STATE_CDIHB
by MOHAMAD REZA SHAFIEI 10 Feb '21

10 Feb '21

hi there ... i'm working on mmc in sel4 for storage memory. i port your code for i.mx7 (modify registers and all need for that). so when i init mmc with calling mmc_init, sdhc driver wait at sdhc.c@249 and in this line: while (readl(host->base + PRES_STATE) & (SDHC_PRES_STATE_CIHB | SDHC_PRES_STATE_CDIHB)); indeed sdhc driver send function (sdhc_next_cmd(..)) send first command in mmc_reset (): which is : struct mmc_cmd cmd = {.data = NULL}; cmd.index = MMC_GO_IDLE_STATE; cmd.arg = 0; cmd.rsp_type = MMC_RSP_TYPE_NONE; printf("2-1\n"); host_send_command(card, &cmd, NULL, NULL); and status= 65 returned whicm means this command sent completely. so when program continue to send another command (still in mmc_reset) which is : /* TODO: review this command. */ struct mmc_cmd cmd2 = {.data = NULL}; ps_mdelay(10); cmd2.index = MMC_SEND_EXT_CSD; cmd2.arg = 0x1AA; cmd2.rsp_type = MMC_RSP_TYPE_R1; printf("2-2\n"); host_send_command(card, &cmd2, NULL, NULL); status which returned with sdhc send command in sdhc driver is 0. but this worked too. and when program execution continue to call mmc_voltage_validation(..) sdhc driver wait in while (readl(host->base + PRES_STATE) & (SDHC_PRES_STATE_CIHB | SDHC_PRES_STATE_CDIHB)); ... I don't have any idea why this happened .. can you help me? I didn't modify any code in sdhc.c or mmc.c ... my app for using mmc is here: #include <autoconf.h> #include <camkes.h> #include <camkes/io.h> #include <camkes/sync.h> #include <stdio.h> #include <utils/util.h> #include "string.h" //sdio test #include <sdhc/mmc.h> #include <sdhc/plat/sdio.h> #include <sdhc/sdio.h> #define max(x, y) (((x) >= (y)) ? (x) : (y)) //build config // #define TEST_FILESYSTEM 0 #ifdef CONFIG_64BIT #define BITS_PER_LONG 64 #else #define BITS_PER_LONG 32 #endif /* CONFIG_64BIT */ #define IMX7_GPIO1_BASE_ADDR ((uint32_t)NULL) #define IMX7_GPIO4_BASE_ADDR ((uint32_t)NULL) #define IMX7_SPI_BASE_ADDR ((uint32_t)NULL) #define IMX7_CTL_MUX_BASE_ADDR ((uint32_t)NULL) /** * we have two keyboard driver () */ bool STDKBD = true; #define IMX7_CTL_MUX_GPIO1_09 (0x18) seL4_CPtr timer_notification(void); seL4_CPtr notification; static void delay(uint64_t ms) { seL4_Word badge; /* test a relative timeout */ uint64_t t1 = timer_time(); // printf("Cur time: %"PRIu64"\n", t1); timer_oneshot_relative(0, ms * NS_IN_MS); seL4_Wait(notification, &badge); // printf("Badge: %x\n", badge); t1 = timer_time(); // printf("Cur time: %"PRIu64"\n", t1); } /* * Required for the camkes_sys_clock_gettime() in sys_clock.c of libsel4camkes. */ int clk_get_time(void) { uint64_t time_in_ms = timer_time() / NS_IN_MS; return (time_in_ms & 0xFFFFFFFF); } static int count = 0; ps_io_ops_t io_ops = {0}; struct netif* net_if; mmc_card_t mmc_card = 0; sdio_host_dev_t sdio_host_dev; int mmc_found = 0; void mmc_irq_handle(ps_irq_t* irq) { printf("mmc irq handle .... \n"); if(!mmc_found){ // printf("mmc not found yet :)\n"); // mmc_init handle this self // sdio_host_dev.handle_irq(&sdio_host_dev,irq->irq.number); mmc_irq_acknowledge(irq); return ; } // sdio_host.handle_irq(&sdio_host, irq); mmc_handle_irq(mmc_card,irq->irq.number); mmc_irq_acknowledge(irq); } int run(void) { notification = timer_notification(); int err = camkes_io_ops(&io_ops); if (err != 0) { ZF_LOGF("Can not init ops : %d\n", err); }; printf("initialize sdhc1 ...\n"); err = sdio_init(SDHC1, &io_ops, &sdio_host_dev); // while card not present check while(sdio_host_dev.reset(&sdio_host_dev) == -1){ delay(1000); } printf("before mmc_init\n"); mmc_init(&sdio_host_dev, &io_ops, &mmc_card); mmc_found = 1; printf("after mmc_init\n"); if (!err) { printf("SDHC1 inited successfully.\n"); // sdhc_ls(); } else { printf("SDHC1 initizatino failed!: %d", err); } // sdio_host_dev.reset(&sdio_host_dev); // mmc_init(&sdio_host_dev, &io_ops, mmc_card); // sdio_host_dev.handle_irq =mmc_handle_irq_func; while (true) { printf(".\n"); delay(1000); } return 0; } best regards.. shafie -- This email was Anti Virus checked by Security Gateway.

1 0

Public seL4 TSC meeting on Fri, 12 Feb
by Gerwin Klein 08 Feb '21

08 Feb '21

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: Fri 12 Feb 2021 15:30-17:00 Sydney time (5:30am in Berlin, 8:30pm in San Francisco). This is the continuation of the meeting last week. The meeting is by Zoom, and you can register here: https://unsw.zoom.us/meeting/register/tZcqf--prz8jGNdE-zpwZXIBsbdYlN3fQn1Y Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: Discussion points - when/how should Committer/Admin role change for people who have left D61 and had the role based on org membership - endorsement process for training and products Vote on: - Platform Owner proposal Discuss, potentially vote on RFC proposals: - https://sel4.atlassian.net/browse/RFC-6 - https://sel4.atlassian.net/browse/RFC-5 - https://sel4.atlassian.net/browse/RFC-4 If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.htmld

1 0

Public TSC meeting on Fri, 29 Jan
by Gerwin Klein 08 Feb '21

08 Feb '21

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: Fri 29 Jan 2021 15:30-17:00 Sydney time (5:30am in Berlin, 8:30pm in San Francisco). The meeting is by Zoom, and you can register here: https://unsw.zoom.us/meeting/register/tZ0ocO6hrDwiGtTYlzULbKeTK8ybYJyCC7_p Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. Sorry about the very early time for Europe, but there are no time slots that work for the US, Australia, and Europe at the same time. We are planning to swap between better times for Europe and the US for the next meetings. The TSC is the body that decides on the technical direction of seL4: https://sel4.systems/Foundation/TSC/ The agenda for the meeting so far is: - updates from the TSC chair and committees: - seL4 public Jira - Jira + GitHub sync - reviewers who have joined - more GitHub tests - discussion points: - do we have too many different forums? - bug/issue classification (Jira is now public, we shouldn't call everything a bug) - more in-tree docs - test infrastructure - extend RFC process slightly? (see https://sel4.atlassian.net/browse/RFC-6?focusedCommentId=14886& ) - when/how should Committer/Admin role change for people who have left D61 and had the role based on org membership - endorsement process for training and products - vote on: - Platform Owner proposal - discuss, potentially vote on RFC proposals: - https://sel4.atlassian.net/browse/RFC-4 - https://sel4.atlassian.net/browse/RFC-5 - https://sel4.atlassian.net/browse/RFC-6 This is probably already too much for 90min and we may have to prioritise, but we will see how far we get. If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

2 5