- Devel - lists.sel4.systems

CAmkES: dataports larger than 4k
by Fabrizio Bertocci 01 Nov '21

01 Nov '21

Is it possible to use dataports that are larger than 4k? I tried with both typed dataports and "Buf" dataport but I can't find a way to do it. In the hello-camkes-2 tutorial, I tried to add a configuration for my dataports in the main assembly file to increase its size like this: // Typed dataport name: 'd_image' // Buf dataport name: 'd' configuration { echo.d_size=65536; // Buf dataport echo.d_image_size=65536; // Typed dataport } unfortunately that doesn't seem to do anything as d_get_size() keep returning 4k, and for the typed dataport, the build system triggers the static assert "typeof(from_0_d_image_data) size greater than dataport size" Thanks, Fabrizio

2 1

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