- Devel - lists.sel4.systems

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