November 2018 - Devel - lists.sel4.systems

Re: [seL4] seL4 10.1.0 and camkes-3.6.0
by jonas.cl＠protonmail.com 16 Nov '18

16 Nov '18

Hi, Today I created a few pull-requests on seL4 repos to build x86-64 with clang: - https://github.com/seL4/seL4/pull/105 - https://github.com/seL4/musllibc/pull/4 - https://github.com/seL4/seL4_tools/pull/19 /Jonas ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Wednesday, November 14, 2018 5:28 PM, <devel-request(a)sel4.systems> wrote: > Message: 3 > Date: Wed, 14 Nov 2018 16:28:17 +0000 > From: Andy Helten andy.helten(a)goctsi.com > To: "Matthew.Brecknell(a)data61.csiro.au" > Matthew.Brecknell(a)data61.csiro.au, "devel(a)sel4.systems" > > <devel(a)sel4.systems> > > > Subject: Re: [seL4] seL4 10.1.0 and camkes-3.6.0 > Message-ID: > DM6PR17MB2314D1EF141DD6DD6A4779BE92C30(a)DM6PR17MB2314.namprd17.prod.outlook.com > > Content-Type: text/plain; charset="utf-8" > > Disclaimer: I've never compiled sel4 nor executed sel4 and, at this point, am just a follower of this mailing list (with tentative plans to use sel4 "someday") > > Regarding the issue that was fixed here, my first thought was "why did the compiler not complain?". My next thought was "maybe sel4 doesn't enable all warnings in their builds or they ignore the warnings!" But surely a kernel that focuses on security would enable all compiler warnings and fix them immediately as they are introduced. > > Turns out it doesn't matter what sel4 builds are doing, the gcc compiler has a bug that prevents warnings for several of these common "might be used uninitialized" cases. See here: > > https://gcc.gnu.org/bugzilla/show_bug.cgi?id=18501 > > It also appears this bug will not be fixed! An alternative for some projects, though maybe not sel4, is to also compile their code with clang, which does catch these uninitialized cases. If sel4 can use clang to catch these types of mistakes earlier, in a compiler warning, it might save a lengthy validation procedure to catch the error (if it gets caught at all). > > Just thought folks might be interested in this gcc bug -- I certainly wasn't aware of it. > > Andy > > -----Original Message----- > From: Devel devel-bounces(a)sel4.systems On Behalf Of Matthew.Brecknell(a)data61.csiro.au > Sent: Thursday, November 8, 2018 7:22 PM > To: devel(a)sel4.systems > Subject: Re: [seL4] seL4 10.1.0 and camkes-3.6.0 > > Hi, > > Now that the fix for this issue has made it through our integration pipeline, I can explain what happened, since some of you might be interested. The fix is here: > > https://github.com/seL4/seL4/commit/d12bb374ab47d2b13f438969d2eb5dde1021af84 > > At line 56, the target variable was originally declared uninitialised. > If the loop at lines 57 to 64 executes at least once, then the variable is initialised at line 58. But if the loop does not execute, then the variable would remain uninitialised when it is used at line 65. This would be the case if infer_cpu_gic_id was ever called with nirqs <= 0. > This is not a problem in the released kernel, becuase infer_cpu_gic_id is only ever called once in dist_init, with 32 <= nirqs <= 1024. > > However, the binary translation validation test that failed does not do the inter-procedural analysis that would be necessary to realise this. > When looking at infer_cpu_gic_id, the analysis allows nirqs to take any value. It considers that the loop might not execute, and therefore target might be uninitialised when it is used at line 65. The dataflow model that is produced by the analysis cannot model such undefined behaviour, and so the test fails. With the fix, the variable is never uninitialised, so the analysis does not run into this problem. > > In summary, the fix you see here keeps our proofs happy, but it does not increase the safety of the kernel. This function, as it is actually used, was already safe. > > In terms of our development process, this kind of failure in the binary translation validation is quite rare and difficult to predict. And since our proofs take quite a long time to run, we don't always insist that our kernel developers run the proofs for changes in boot code, which is currently unverified except for binary translation validation. We accept that these failures will occasionally happen, and we deal with them when they do. The functions dist_init and infer_cpu_gic_id are boot-only code, so this was one of those rare failures. > > Of course, we should insist on running all the tests for versions we intend to formally release, and we will for future releases. > > Best regards, > Matt > > From: Brecknell, Matthew (Data61, Kensington NSW) > Sent: Thursday, 8 November 2018 11:25 AM > To: devel(a)sel4.systems > Cc: Mcleod, Kent (Data61, Kensington NSW) > Subject: Re: seL4 10.1.0 and camkes-3.6.0 > > Hi, > > Due to an oversight on my part, seL4 10.1.0 was released without passing the full verification test suite. > > We have no reason to believe that there is any problem in the verified parts of this seL4 version. > > The test that failed is part of the binary translation validation, which produces a dataflow graph from the Isabelle/HOL model of the C code, and then attempts to automatically prove a refinement relation between the C and that dataflow graph. The failure occurred in boot code, which in any case is currently not verified. The failure does not mean that there is any problem with the C code. Most likely, it just means that some new code uses some C idiom which is currently not handled by the automatic translation process. > > All other components of the verification test suite pass, including security proofs and functional correctness proofs for the Isabelle/HOL model of the C code. > > Nevertheless, we intend to rectify this failure as soon as possible, and we'll make further announcements when we understand what happened. > > I want to reiterate that this was entirely my fault, and was not at all Kent's fault. > > Best regards, > Matt > > From: Devel devel-bounces(a)sel4.systems on behalf of Kent.Mcleod(a)data61.csiro.au Kent.Mcleod(a)data61.csiro.au > Sent: Thursday, 8 November 2018 8:44 AM > To: devel(a)sel4.systems > Subject: [seL4] seL4 10.1.0 and camkes-3.6.0 > > See an online copy of the release notes at: > https://docs.sel4.systems/sel4_release/seL4_10.1.0 > https://docs.sel4.systems/camkes_release/Camkes_3.6.0 > > 10.1.0 2018-11-07: SOURCE COMPATIBLE > > Changes > > -------- > > - structures in the boot info are not declared 'packed' > - these were previously packed (in the GCC attribute sense) > - some field lengths are tweaked to avoid padding > - this is a source-compatible change > - ARM platforms can now set the trigger of an IRQ Handler capability > - seL4_IRQControl_GetTrigger allows users to obtain an IRQ Handler capability > and set the trigger (edge or level) in the interrupt controller. > > - Initial support for NVIDIA Jetson TX2 (ARMv8a, Cortex A57) > - AARCH64 support added for raspberry pi 3 platform. > - Code generation now use jinja2 instead of tempita. > - AARCH32 HYP support added for running multiple ARM VMs > - AARCH32 HYP VCPU registers updated. > - A new invocation for setting TLSBase on all platforms. > - seL4_TCB_SetTLSBase > - Kbuild/Kconfig/Makefile build system removed. > > camkes-3.6.0 2018-11-07 > Using seL4 version 10.1.0 > > Changes > > -------- > > - AARCH64 is now supported. > - CakeML components are now supported. > - Added `query` type to Camkes ADL to allow for querying plugins for component configuration values. > - Components can now make dtb queries to parse device information from dts files. > - Component definitions for serial and timer added on exynos5422, exynos5410, pc99. > - Preliminary support for Isabelle verification of generated capDL. > - See cdl-refine-tests/README for more information > - Simplify and refactor the alignment and section linking policy for generated Camkes binaries. > - Dataports are now required to declare their size in the ADL. > - Templates now use seL4_IRQHandler instead of seL4_IRQControl, which is consistent with the seL4 API. > - This change is BREAKING. > - Remove Kbuild based build system. > - Remove caches that optimised the Kbuild build system, which are not required with the new Cmake build system. > - Added virtqueue infrastructure to libsel4camkes, which allows virtio style queues between components. > > > Upgrade Notes > > -------------- > > - Any dataport definitions that did not specify a size must be updated to use a size. > - Any template that used seL4_IRQControl must be updated to use seL4_IRQHandler. > - Projects must now use the new Cmake based build system. > > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > -------------------------------------------------------------------------------- > > Subject: Digest Footer > > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > --------------------------------------------------------------------------------- > > End of Devel Digest, Vol 54, Issue 12

2 1

seL4 10.1.0 and camkes-3.6.0
by Kent.Mcleod＠data61.csiro.au 15 Nov '18

15 Nov '18

See an online copy of the release notes at: <https://docs.sel4.systems/sel4_release/seL4_10.1.0> <https://docs.sel4.systems/camkes_release/Camkes_3.6.0> 10.1.0 2018-11-07: SOURCE COMPATIBLE ## Changes * structures in the boot info are not declared 'packed' - these were previously packed (in the GCC attribute sense) - some field lengths are tweaked to avoid padding - this is a source-compatible change * ARM platforms can now set the trigger of an IRQ Handler capability - seL4_IRQControl_GetTrigger allows users to obtain an IRQ Handler capability and set the trigger (edge or level) in the interrupt controller. * Initial support for NVIDIA Jetson TX2 (ARMv8a, Cortex A57) * AARCH64 support added for raspberry pi 3 platform. * Code generation now use jinja2 instead of tempita. * AARCH32 HYP support added for running multiple ARM VMs * AARCH32 HYP VCPU registers updated. * A new invocation for setting TLSBase on all platforms. - seL4_TCB_SetTLSBase * Kbuild/Kconfig/Makefile build system removed. ---- camkes-3.6.0 2018-11-07 Using seL4 version 10.1.0 ## Changes * AARCH64 is now supported. * CakeML components are now supported. * Added `query` type to Camkes ADL to allow for querying plugins for component configuration values. * Components can now make dtb queries to parse device information from dts files. * Component definitions for serial and timer added on exynos5422, exynos5410, pc99. * Preliminary support for Isabelle verification of generated capDL. - See cdl-refine-tests/README for more information * Simplify and refactor the alignment and section linking policy for generated Camkes binaries. * Dataports are now required to declare their size in the ADL. * Templates now use seL4_IRQHandler instead of seL4_IRQControl, which is consistent with the seL4 API. - This change is BREAKING. * Remove Kbuild based build system. * Remove caches that optimised the Kbuild build system, which are not required with the new Cmake build system. * Added virtqueue infrastructure to libsel4camkes, which allows virtio style queues between components. ## Upgrade Notes * Any dataport definitions that did not specify a size must be updated to use a size. * Any template that used seL4_IRQControl must be updated to use seL4_IRQHandler. * Projects must now use the new Cmake based build system.

4 4

Data61 Seeking Research Scientist
by Gerwin.Klein＠data61.csiro.au 14 Nov '18

14 Nov '18

Data61 Seeking Research Scientist ================================= We are looking for a full-time research scientist in formal verification to join us, the Trustworthy Systems group, at Data61, CSIRO. 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. Our vision is a world in which computer users can choose all three: correct, secure, and fast. We believe that most current approaches to building systems are fundamentally flawed. We aim to demonstrate a better way. Our approach is rooted in foundational, formal verification using theorem provers (e.g., Isabelle, HOL4), and high-performance system design. If you find this vision appealing, and have ideas about how to pursue it, we want to hear from you. Our team brings together a unique combination of expertise in systems, security, formal verification, and programming languages. We are the creators of seL4, the world's first operating system microkernel with a machine-checked proof (in Isabelle/HOL). seL4 boasts both extreme performance and foundational binary-level correctness and security proofs. We are also involved in CakeML, the most realistic verified compiler for a functional programming language, and a promising approach to scaling full verification up to applications code. We are building on these successes in various directions, including concurrency (formal reasoning and implementation), timing (real-time guarantees and timing channels), and whole-system verification using component systems (e.g., CAmKES) and code+proof co-generation. We publish in top conferences, and are involved in multiple international research collaborations. You will have the opportunity to teach at UNSW should you wish to take it. We have a flexible, friendly, and intellectually stimulating work environment. 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. The salary range for this position (plus superannuation) is - Research Scientist: 97k-105k - Senior Research Scientist: 111k-130k depending on experience and qualifications. Apply online here: https://jobs.csiro.au/job/Sydney%2C-NSW-Research-ScientistSenior-Research-S… Your application should include a cover letter, CV, short research statement, and contact information for two references. This round of applications closes on 15 January 2019. For any questions on this position, please contact June.Andronick(a)data61.csiro.au

1 0

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 송대영 09 Nov '18

09 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 08 Nov '18

08 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 08 Nov '18

08 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 07 Nov '18

07 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 07 Nov '18

07 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