- Devel - lists.sel4.systems

Data61 Seeking Proof Engineers
by Gerwin.Klein＠data61.csiro.au 14 Nov '18

14 Nov '18

Data61 Seeking Proof Engineers ============================== We are are hiring again! If only there were a place where I could prove theorems for money, change the world, and have fun while doing it... Sounds too good to exist? In the Trustworthy Systems team at Data61 that's what we do for a living. We are the creators of seL4, the world's first fully formally verified operating system kernel with extreme performance and strong security & correctness proofs. Our highly international team is located on the UNSW campus, close to the beautiful beaches of sunny Sydney, Australia, one of the world's most liveable cities. We are looking for multiple motivated proof engineers who want to join our team in Sydney, move things forward, and have global impact. You would - work on industrial-scale formal proofs in Isabelle/HOL - develop formally verified infrastructure for building secure systems on top of seL4 - contribute to improved proof automation and reasoning techniques - apply formal proof to real-world systems and tools To apply for this position, you should possess a significant subset of the following skills. - functional programming in a language like Haskell, ML, or OCaml - first-order or higher-order formal logic - basic experience in C - ability and desire to quickly learn new techniques - undergraduate degree in Computer Science, Mathematics, or similar - ability and desire to work in a larger team We are hiring at two levels, so if you are more qualified or experienced than the above would suggest, you can come in as a senior proof engineer. If you additionally have experience - in software verification with an interactive theorem prover such as Isabelle/HOL, HOL4, or Coq, and/or - with operating systems and microkernels you should definitely apply! If you have the right skills and background, we can provide training on the job. Continual learning is a central component of everything we do. You will work with a unique world-leading combination of OS and formal methods experts, students at undergraduate and PhD level, engineers, and researchers from 5 continents, speaking over 15 languages. Trustworthy Systems is a fun, creative, and welcoming workplace with flexible hours & work arrangements. We value diversity in all forms and welcome applications from people of all ages, including people with disabilities, and those who identify as LGBTIQ. See https://ts.data61.csiro.au/diversity/ for more information. Salary ranges, in AUD (plus superannuation): - Junior Proof Engineer: 73k-93k - Senior Proof Engineer: 97k-105k depending on experience and qualifications. Apply online at the following link for the Proof Engineer positions: - https://jobs.csiro.au/job/Sydney%2C-NSW-Proof-Engineer/518443000/ - https://jobs.csiro.au/job/Sydney%2C-NSW-DATA-61/518441000/ Your application should include a cover letter, CV, undergraduate transcript (if applicable), and contact information for two references. This round of applications closes on 17 December 2018. For any questions on these positions, please contact Rafal.Kolanski(a)data61.csiro.au or June.Andronick(a)data61.csiro.au The seL4 code and proof are open source. Check them out at https://seL4.systems More information about Data61's Trustworthy Systems team at https://ts.data61.csiro.au There are additional proof engineering positions available on the Cogent project. Cogent is a language we designed to ease the verification of systems components around seL4. For expressions of interest, see contact details on https://ts.data61.csiro.au/projects/TS/cogent.pml Looking to do a PhD? Data61 and UNSW (https://www.unsw.edu.au/) offer scholarships! See https://ts.data61.csiro.au/students/research.pml for details.

1 0

Scheduling of vCPUs on x86
by Alexander Boettcher 10 Nov '18

10 Nov '18

Hello, the time spend by a vCPU TCB (tcbTimeSlice) seems to be not accounted/updated by the seL4 kernel on a timer ticks, which leads to starvation of other TCBs running on the same or lower priority level. In one of our test setups, if once a vCPU runs and doesn't give up its timeslice willful (e.g. guest goes in while loop and thereby not causing a VM exit to be handled by the VMM), all other TCBs (normal threads and vCPUs) on the same timeslice are not considered to be scheduled again, since tcbTimeSlice of the vCPU stays full forever. Following patch seems to fix the issue. Can you please have a look and verify that it is correct ? Or should it be solved on another place in the kernel differently. Just out of curiosity, why is a separate thread state in the scheduler for x86 (CONFIG_VFX) required that is not needed for scheduling of a vCPU on ARM ? I didn't expect the scheduler thread states to be different between hardware architectures in seL4. Cheers, -- Alexander Boettcher Genode Labs https://www.genode-labs.com - https://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

5 8

sel4bench IPC questions
by 송대영 08 Nov '18

08 Nov '18

HI, I have a question about sel4bench IPC. Thanks for the reply. 1. Making seL4_IPCBuffer and mapping into the thread is necessary? I think that sending short messages don't need seL4_IPCBuffer, is it right? 2. This is seL4_Call annotation in benchmark_param. /* Call fastpath between client and server in the different address space */ But I can't understand how to measure seL4_Call function performance. [Client thread] [Server thread] seL4_Call seL4_ReplyRecv(I'm not sure) 1) client send message. 2) server receive message. 3) server send message. 4) client receive message. seL4_Call performance in sel4bench excluding overhead , is it right? = 1) + 2) + 3) + 4) - 3) - 4) 3. This is seL4_Send annotation in benchmark_param. /* Send slowpath (no fastpath for send) same prio client-server, different address space */ But client_prio(seL4_MaxPrio - 1) and server_prio(seL4_MaxPrio - 2) is different.

2 1

Support for QNX-like booting from an XIP filesystem image
by Andrew Warkentin 07 Nov '18

07 Nov '18

For UX/RT <https://gitlab.com/uxrt/>, the seL4-based OS I am writing, I have patched seL4 to support for booting from an in-memory execute-in-place filesystem image that contains the kernel and all user-mode programs required to mount the root filesystem (similar to that of QNX, but with more of the functionality in the bootloader rather than the root server). The existing seL4 boot process may be OK for static embedded systems that are always cross-compiled, but UX/RT is going to be a dynamic general-purpose OS with a boot image that will include files from multiple separately-installed packages and will possibly be customized to the system it is installed on. Requiring any image filesystem to be linked into the root server makes updating boot images more complex than being able to use a simple filesystem builder to make an image containing the kernel, root server, and everything else that is required (the main special considerations being placing the kernel and root server at fixed physical addresses and padding the image to allow for bss sections, which are easy enough). Also, I want it to be easy to manually boot UX/RT images, so you can just type something like "boot (hd0,0)/uxrt.boot" (much like manually booting NetBSD, OpenBSD, or most older Unices), and the bootloader will automatically load the kernel and all required modules from within the image as opposed to having to type a lot of boilerplate to load the kernel and root server (and anything else that may be required). In addition I don't think that the root server should need to have any support for parsing image filesystems and should be able to obtain all the files required for early boot from the MBI. I am using Multiboot2 with a few custom tags added and a few extra requirements regarding placement of modules. I currently have an in-memory loader that implements my variant of Multiboot2, and eventually want to implement a full disk-based bootloader. I have also implemented a page-oriented in-memory filesystem called XRFS (originally based on Linux romfs) with support for placing files at fixed addresses. The in-memory loader was parsing the filesystem and using a script to locate the modules within the image, although I have decided that it is overkill to do that, and it would allow the loader to be simpler if the filesystem image has its own MBH separate from that of the kernel (the magic number will be different from the kernel MBH as well), with tags for the kernel and each module, so that the loader's existing MBH-parsing code can be used to locate files in the image. As far as my kernel patches go, they extend the existing Multiboot2 code and do not interfere with the existing boot code. Right now they are x86-only, but I am planning to add Multiboot2 support to other architectures eventually as well. They do not introduce any dependency on my filesystem format in the kernel (it does know that there is an FS image and that there are modules contained within it, and assumes that modules are contiguous). Relocation of the root task is disabled when an FS image is present, since it will already be placed in a usable location in the image. Kernel-level ELF loading of modules is also disabled when using my Multiboot2 extensions, since my loader is capable of parsing ELF modules, loading them, and passing information on module sections and addresses to the kernel through tags. The part of the image containing the kernel is inaccessible to the root task for obvious reasons, so an additional requirement is that the kernel is the first file in the image, followed by the root server, and then all other files (XRFS is structured to allow the remainder of the image to be read even though the beginning is inaccessible). There is also support for passing the MBI through to the root task, which requires that the MBI is allocated immediately after the end of the filesystem image (a new structure is added to the bootinfo to provide the root server with the address of the MBI). >From what I've said, would there be any problems with including my patches in the mainline seL4 repository? Only the boot code is modified. Loading the root server works, but I haven't yet tested the MBI passthrough, so I am not quite ready to submit anything (currently I am working on converting my bootloader from parsing the filesystem itself to parsing an MBH in the FS image, like I said before).

2 3

Non CAmkES VM on x86
by Chris Guikema 07 Nov '18

07 Nov '18

DornerWorks is looking at working with the CAmkES-VM. In previous work with ARM, we've only used a non-camkes VMM, since the hypervisor pieces were more important (and 64-bit ARM CAmkES hadn't been developed). Out of curiosity, has Data61 ever worked with a non-CAmkES VM on x86 similar to how the old ARM VMM worked? If so, is that something that could be released? Thanks, Chris Guikema

2 1

seL4 on Heterogeneous Processing Architectures (Zynq UltraScale+ MPSoCs)
by Blam Kiwi 06 Nov '18

06 Nov '18

I am investigating the use of seL4 on heterogeneous architectures such as the Zynq UltraScale+ MPSoCs. I have a non-trivial use-case I'm investigating that involves utilising both the Cortex-R5 cores and Core-A53 cores for different applications. I'm rather new to seL4 development so I'm a bit stuck and need some advice. It's easiest if I just list my requirements and assumptions for my architecture design: a) I am targeting the Zynq US+ platform and wish to use seL4 as the OS Kernel to manage system resources and run virtual machines. b) I require the use of the Cortex R5 cores in DCLS mode for trusted code with high fault tolerance requirements. c) I require the use of the Cortex A53 cores for running unsafe Linux VMs. d) It's my understanding that seL4 lacks 64-bit multicore support for its own scheduler, but VMs running on seL4 could be provided with access to all the cores? (Eg: Linux) e) It's my understanding that seL4 lacks heterogeneous task scheduling, and cannot manage both the Cortex R5 and Cortex A53 cores. This leads me to make the following architectural conclusions: [1] It's not possible to boot an seL4 kernel on one processor and have it manage the other. [2] Use TrustZone to create vCPUs for the Cortex R5 and A53 modules and boot an seL4 kernel on each. [3] Some domain specific protocol is required for the CPU modules to communicate and share resources. Any help or advice would be appreciated. Regards, Robbie

4 4

Passing Network Resource to Linux VM in TK1-SOM
by Daniel Wang 06 Nov '18

06 Nov '18

Hi all, I got a question, how can I pass the network communication to Linux virtual machine? Following the work of seL4-ARM-VMM with TK1-SOM board, i run seL4 as the microvisor that hosts the buildroot Linux as a user-land process, I was able to mount the MMC storage in the virtual machine, but I cannot get the NIC works. I’m wondering has anyone tried it that can give me some hint? Best Regards -Daniel Wang

2 2

run docker on sel4
by Jia He 06 Nov '18

06 Nov '18

Hi all I am new comer to sel4 community. I knew a little bit virtualisation infrastructe(kvm/qemu), but I know little about sel4/docker. I am investigating the proper implemenatation for running docker on sel4 on arm64. There might several ways I can figure out.Any suggestions are welcome :-) 1. run linux on sel4 vmm (camkes_vm) and run docker on linux. This might be the easiest way. It might have worked well on X86 2. porting l4linux to sel4. Don't know whether it is feasible? 3. run docker as sel4 service without linux. On this way, golang and its library should be ported to sel4. Some missed syscalls which are needed by docker should be implemenated. Is there any other ways or anything else to make the implatation more feasible? --- Cheers, Justin

3 2

seL4 IPC and SMP question.
by 송대영 05 Nov '18

05 Nov '18

HI, I have a question about IPC and SMP. I ran sel4bench on sabre lite(i.mx6, arm v7). 1. I want to confirm performance difference between Lazy Scheduling and Beno Scheduling. Can I configure scheduler? 2. Can you explain the difference when thread state is "ThreadState_Running" and "ThreadState_Restart"? 3. I tried "SMP Benchmark" but I can't understand what this benchmark exactly means. What "Cycles" means in this benchmark? smp : This is an intra-core ipc round-trip benchmark to check overhead of the kernel synchronization on ipc throughput. 4. I try to measure IPC performance with SMP is on. I used "seL4_TCB_SetAffinity" function so server executed in Core1 and client executed Core2. But performance results are too excessive. seL4_Call(same vspace, ipc length is 0)' result is 129331186 cycles. Are these results are available?

3 2

Booting seL4test on x86 hardware
by Alex Pavey 30 Oct '18

30 Oct '18

Hello, We are having issues being able to get the seL4test userland image to boot on x86 hardware. We have attempted to boot with syslinux off a USB, with PXELINUX, and with grub and see the same userland image loading issue across boot methods. Build steps: - Following https://docs.sel4.systems/Hardware/IA32 - Using "-DPLATFORM=x86_64" o Does not appear to boot (no serial output) - Using "-DPLATFORM=ia32" o Kernel boots but is unable to load userland image The manifest commit hash is: 01c11cfcd881c1da5b7520162fae40f6eae1c16b Hardware: - DELL Optiplex 980 with an Intel Core i7 860 processor We are seeing the following serial output: SYSLINUX 6.03 20171017 Copyright (C) 1994-2014 H. Peter Anvin et al Loading sel4kernel... ok Loading rootserver... ok Boot config: parsing cmdline 'sel4kernel' Boot config: console_port = 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0x1d6000 end=0x4abdf4 size=0x2d5df4 name='rootserver' Parsing GRUB physical memory map Physical Memory Region from 0 size 9e400 type 1 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size df5cfc00 type 1 Adding physical memory region 0x100000-0x1fc00000 Physical Memory Region from df6cfc00 size 54000 type 4 Physical Memory Region from df723c00 size 2000 type 3 Physical Memory Region from df725c00 size 8da400 type 2 Physical Memory Region from f8000000 size 4000000 type 2 Physical Memory Region from fed00000 size 400 type 2 Physical Memory Region from fed20000 size 80000 type 2 Physical Memory Region from fec00000 size 100000 type 2 Physical Memory Region from fee00000 size 100000 type 2 Physical Memory Region from ffb00000 size 500000 type 2 Physical memory region not addressable Physical memory region not addressable Multiboot gave us no video information ACPI: RSDP paddr=0xfec00 ACPI: RSDP vaddr=0xdfcfec00 ACPI: RSDT paddr=0xfc790 ACPI: RSDT vaddr=0xdfcfc790 ***WARNING*** SKIM window not enabled, this machine is probably vulernable to Meltdown (https://www.meltdownattack.com) consider enabling Kernel loaded to: start=0x100000 end=0x13a000 size=0x3a000 entry=0x100076 ACPI: RSDT paddr=0xfc790 ACPI: RSDT vaddr=0xdfcfc790 ACPI: FADT paddr=0xfc85c ACPI: FADT vaddr=0xdfcfc85c ACPI: FADT flags=0xa5 ACPI: DMAR paddr=0xfcdde ACPI: DMAR vaddr=0xdfcfcdde ACPI: IOMMU host address width: 36 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0 ACPI: 1 IOMMUs detected ACPI: MADT paddr=0xfc9c4 ACPI: MADT vaddr=0xdfcfc9c4 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x2 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x4 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x6 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x1 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x3 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x5 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x7 ACPI: Not recording this APIC, only support 1 ACPI: MADT_IOAPIC ioapic_id=8 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: BOOT MODULE: 0x1d6000: 0x0 0x1d6010: 0x0 0x1d6020: 0x0 0x1d6030: 0x0 0x1d6040: 0x0 0x1d6050: 0x0 0x1d6060: 0x0 0x1d6070: 0x0 0x1d6080: 0x0 0x1d6090: 0x0 0x1d60a0: 0x0 Boot module does not contain a valid ELF image seL4 called fail at /host/sel4test/kernel/src/arch/x86/kernel/boot_sys.c:813 in function boot_sys, saying "boot_sys failed for some reason :(" halting... Kernel entry via Interrupt, irq 0 Thanks, Alex

3 4