March 2020 - Devel - lists.sel4.systems

Would verifying ARM64 be any more difficult than verifying ARM32 was?
by Demi M. Obenour 19 Mar '20

19 Mar '20

Would verifying seL4 on ARM64 be any more difficult than verifying seL4 on ARM32 was? What about other architectures like POWER9? I hope I am not asking too many questions; I am just a curious outsider who hopes they can use seL4 someday. Sincerely, Demi

4 3

CAmkES, Virtual Machines and Multicore Guarantees
by Turner, Ben 18 Mar '20

18 Mar '20

Hi, In the seL4 FAQ section it states: "Multicore is presently supported on x64 and Arm v7 (32-bit) and v8 (64-bit). Verification of the multicore kernel is in progress (but presently as an unfunded background activity)." Considering only seL4 ----------------------------- My interpretation of this is that given a single seL4 application running on a device, it is not possible to currently guarantee the protections seL4 provides if the application invokes multiple threads across more than 1 core. Is this correct? Considering CAmkES ---------------------------- I would also like to know how CAmkES affects this. For example, looking at the vm_multi app for the exynos5422 in the camkes-arm-vm repository, what would the effect be of assigning unique CPU affinities to each of the VM components? Do the guarantees still hold in this situation? Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

5 4

Configuring pinmux in am335x (beaglebone) can't be done from user mode
by Stephen Sherratt 18 Mar '20

18 Mar '20

Hi all, I've been experimenting with seL4 running on a Ninjablocks (https://www.engadget.com/2013/05/01/ninja-blocks/) that I had lying around. Inside there is a beaglebone, with a custom shield (or cape) containing a microcontroller (atmega328p), some LEDs and a radio. The beaglebone (which normally runs linux) sends json-encoded commands over a serial connection to the on-cape microcontroller, which runs firmware that decodes these commands and controls the LEDs and radio. The complication is that the am335x pins connected to the custom shield are multiplexed, and don't connect to a uart device by default (they are gpio pins by default). The "Control Module" in the am335x can be used to configure pin multiplexing, but it can't be written to in user-mode. From the am335x manual (http://www.ti.com/lit/ug/spruh73q/spruh73q.pdf, page 1449): "Note: For writingto the controlmoduleregisters,the MPUwill need to be in privileged modeof operationand writes will not work fromusermode." To test that the rest of my app works I added the control module to the beaglebone device tree overlay and hacked the kernel to configure the relevant pins to connect to the uart device during boot: https://github.com/stevebob/seL4/commit/4295035ac7fd720fb531b7e0893f1f1191e… And now I have a little rootserver that can control the colours of LEDs on the shield: https://github.com/stevebob/sel4ninja/blob/master/apps/hello-ninja/src/main… What would be the right way of configuring the control module in a seL4-based system, given that it has to happen in kernel mode? To configure the uart pins when running linux on the board, I had to add the following to the device tree: scm@0 { ... pinmux@800 { ... pinmux_uart0_pins { // <-- this was already here pinctrl-single,pins = <0x170 0x30 0x174 0x00>; phandle = <0x20>; }; pinmux_uart1_pins { // <-- I had to add this pinctrl-single,pins = <0x180 0x30 0x184 0x00>; phandle = <0x60>; }; The (seL4) kernel build system already has basic support for interpreting device trees. Would a reasonable solution to my problem be extending this support with a minimal statically-generated control module driver that configures pinmux during boot based on the device tree? There would still be a problem where each board could only have a single pinmux config (as specified by that board's device tree). It seems like an easy fix for this would be a config variable passed to the build system (similar to -DPLATFORM) that overrides the default device tree file. That way projects that want non-standard pinmux configs could bring their own device trees. Cheers, Steve

2 1

seL4 design principles
by Heiser, Gernot (Data61, Kensington NSW) 15 Mar '20

15 Mar '20

I’ve just posted a blog that tries to explain why de do things the way we de in seL4, and why we don’t do some other things, such as hardware abstraction. I hope this helps people understand better which kind of kernel changes are acceptable and which aren’t, and why the API isn’t designed for ease of use. https://microkerneldude.wordpress.com/2020/03/11/sel4-design-principles/ Gernot

3 4

intel-vtd.c::vtd_get_n_paging looks so suspicious
by laokz 15 Mar '20

15 Mar '20

Hello all, kernel/src/plat/pc99/machine/intel-vtd.c::vtd_get_n_paging() confused me a lot. Wish to get any help. This func intends to calculate paging pages needed for all RMRRs. The following code 'filter the identical regions by pci bus id', and use them to figure out the final result. ``` for (word_t i = 1; i < rmrr_list->num; i++) { if (vtd_get_root_index(rmrr_list->entries[i].device) != vtd_get_root_index(filtered.entries[filtered.num - 1].device) && rmrr_list->entries[i].base != filtered.entries[filtered.num - 1].base && rmrr_list->entries[i].limit != filtered.entries[filtered.num - 1].limit) { filtered.entries[filtered.num] = rmrr_list->entries[i]; filtered.num++; } } ``` But vtd_map_reserved_page() says, every different devices(with diff bus-dev- func ID) have their own paging structures. Then why do filter here like this , yet the logic looks so confusing. And on line 313, it counts pages according to the specified level address bits. ``` size += get_n_paging(region, 32 - (VTD_PT_INDEX_BITS * i + seL4_PageBits)); ``` So what does 32 mean? Maybe a typo? Thanks, laokz

2 2

Using sel4.xml/sel4arch.xml to generate custom bindings
by Alexandre Mutel 12 Mar '20

12 Mar '20

Hello, I would like to use the sel4.xml API description files to generate custom bindings for a prototype language to interact directly with seL4 without going through libsel4 C API. I assume that the structure of these files could change, which I'm willing to accept, but wanted to know if these files are here to stay in the future? I understand also that I will still have to parse libsel4 C headers to recover the full API which I'm fine with too. Do you see any trouble following this approach or would you recommend something else?

2 1

May be an error in "alloc_free_io_port_range" of projects/seL4_projects_libs/libsel4vmmplatsupport/src/ioports.c
by yadong.li 12 Mar '20

12 Mar '20

Hi: background: I run virtio_net and virt_con in the lastest version, it is run OK, but I try to add another virito blk, I meet run error below: "Unhandled offset of 0x400 of size 4, reading Assertion failed: !"panic" (/home/yadong.li/seL4_vm_11/sel4_horizon/camkes-arm-vm/projects/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_in: 71)" I add print on my enviornmen, found: ********************start[0x1000], end[0x1400] /*net*/ ********************start[0x1400], end[0x1800] /*con*/ ********************start[0x1800], end[0x1c00] /*blk*/ ---------------------------virtio_con_io_in, con = 0x55f3238, offset = 0x400[0x1800:0x1400] port_no:1800 should belong "blk", but it recongnize as belong "con"(con may be not use the offset 0 feature), the boundary may be have some problem the function: static int alloc_free_io_port_range(vmm_io_port_list_t *io_list, ioport_range_t *io_range) { uint16_t free_port_addr = io_list->alloc_addr; if (free_port_addr + io_range->size < free_port_addr) { /* Possible overflow */ return -1; } io_list->alloc_addr += io_range->size; io_range->start = free_port_addr; io_range->end = free_port_addr + io_range->size; return 0; } I think "io_range->end = free_port_addr + io_range->size;" should change to "io_range->end = free_port_addr + io_range->size - 1;" ? Thank you very much!

2 1

Booting on a Jetson TK1 board.
by Travis Wheatley 12 Mar '20

12 Mar '20

Hello all, I am spinning up on sel4 and having difficulty booting a kernel on a Jetson TK1 board. I have successfully downloaded the cmakes repo and can build the x86 version of the code and run it as a simulation. I can also successfully build the TK1 version by changing the -DARCHETECTURE argument passed to init-build.sh to “tk1”. This results in a single image file named “capdl-loader-image-arm-tk1” to show up in my images folder (as opposed to both a kernel image and “userland” image that get created in the x86 version). So… I put that image on an SD card, plug it into the TK1, boot to a uboot prompt, and load the image using the command “fatload mmc 1 0x82000000 <filename>”. I can use “md” to see that the image is actually loaded properly. However, when I type “go 0x82000000” I see no output what so ever going out of the serial port. What I expect to see is similar output to what was displayed in the x86 simulation. I posted the question to the IRC channel yesterday and someone suggested using bootm or bootelf. No luck with either of these. So… hoping someone here might be able to give me a clue. — Travis

2 4