- Devel - lists.sel4.systems

BeagleBone and CAmkES app picoserver
by KAP Benjamin 06 May '19

06 May '19

Hello I am trying to compile the CAmkES app picoserver for the BeagleBone Black but I do encounter some errors which I cannot manage to solve. Steps: - I repo synced the latest camkes-manifest which was added support for the BeagleBone - added am335x implementations to the Ethdriver global-component - created subfolder and issued ../init-build.sh -DPLATFORM=am335x -DSIMULATION=0 -DAARCH32=1 -DCAMKES_APP=picoserver - ninja Errors: [1/48] Building C object projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj FAILED: projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj ccache /usr/bin/arm-linux-gnueabi-gcc --sysroot=/host/PICO -DHAVE_AUTOCONF -I../projects/util_libs/libethdrivers/src/plat/am335x/cpsw -I../projects/util_libs/libethdrivers/include -I../projects/util_libs/libethdrivers/plat_include/am335x -I../projects/util_libs/libethdrivers/arch_include/arm -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/camkes-tool/libsel4camkes/gen_config -Iprojects/capdl/capdl-loader-app/gen_config -Iprojects/projects_libs/libusbdrivers/gen_config -Iprojects/rumprun/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/seL4_projects_libs/libsel4arm-vmm/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -Iprojects/util_libs/libpicotcp/gen_config -Iprojects/musllibc/build-temp/stage/include -I../projects/util_libs/libplatsupport/include -I../projects/util_libs/libplatsupport/plat_include/am335x -I../projects/util_libs/libplatsupport/arch_include/arm -I../projects/util_libs/libutils/include -I../projects/util_libs/libutils/arch_include/arm -Iprojects/util_libs/libpicotcp/picotcp_external/picotcp/build/include -march=armv7-a -marm -D__KERNEL_32__ -g -nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mfloat-abi=softfp -std=gnu11 -MD -MT projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj -MF projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj.d -o projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj -c ../projects/util_libs/libethdrivers/src/plat/am335x/cpsw/cpswif.c In file included from ../projects/util_libs/libethdrivers/src/plat/am335x/cpsw/cpswif.c:47:0: ../projects/util_libs/libethdrivers/src/plat/am335x/cpsw/../lwiplib.h:46:22: fatal error: lwip/opt.h: No such file or directory #include <lwip/opt.h> ^ compilation terminated. [2/48] Performing build step for 'parse_capdl_tool' make: Nothing to be done for 'all'. [3/48] Building C object projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj FAILED: projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj ccache /usr/bin/arm-linux-gnueabi-gcc --sysroot=/host/PICO -DHAVE_AUTOCONF -I../projects/util_libs/libethdrivers/src/plat/am335x/cpsw -I../projects/util_libs/libethdrivers/include -I../projects/util_libs/libethdrivers/plat_include/am335x -I../projects/util_libs/libethdrivers/arch_include/arm -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/camkes-tool/libsel4camkes/gen_config -Iprojects/capdl/capdl-loader-app/gen_config -Iprojects/projects_libs/libusbdrivers/gen_config -Iprojects/rumprun/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/seL4_projects_libs/libsel4arm-vmm/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -Iprojects/util_libs/libpicotcp/gen_config -Iprojects/musllibc/build-temp/stage/include -I../projects/util_libs/libplatsupport/include -I../projects/util_libs/libplatsupport/plat_include/am335x -I../projects/util_libs/libplatsupport/arch_include/arm -I../projects/util_libs/libutils/include -I../projects/util_libs/libutils/arch_include/arm -Iprojects/util_libs/libpicotcp/picotcp_external/picotcp/build/include -march=armv7-a -marm -D__KERNEL_32__ -g -nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mfloat-abi=softfp -std=gnu11 -MD -MT projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj -MF projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj.d -o projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj -c ../projects/util_libs/libethdrivers/src/plat/am335x/beaglebone.c ../projects/util_libs/libethdrivers/src/plat/am335x/beaglebone.c:17:24: fatal error: lwip/netif.h: No such file or directory #include <lwip/netif.h> ^ compilation terminated. ninja: build stopped: subcommand failed. Any help is very much appreciated. Best regards, Benjamin P.S. The file projects/util_libs/libplatsupport/plat_include/am335x/platsupport/plat/timer.h contains the static UNUSED timer_properties_t dmt_properties which caused errors on compilation too. (I deleted the lines since they arent used anyways)

2 1

Undefined Reference iommu dma
by KAP Benjamin 26 Apr '19

26 Apr '19

Hello I have a linking problem in the picoserver CAmkES-application which was added 2 days ago. Steps I did: 1) repo init -u https://github.com/seL4/camkes-manifest.git 2) repo sync 3) start docker container 4) (in new subfolder) ../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=1 -DCAMKES_APP=picoserver (side note: aborts because picotcp folder is missing in projects folder, but that's easy fixed) 5) ninja Error: [5/16] Linking C executable projects/camkes/ethdriver.instance.bin FAILED: projects/camkes/ethdriver.instance.bin : && ccache /usr/bin/gcc --sysroot=/host/test -m64 -march=nehalem -D__KERNEL_64__ -g -march=nehalem -D__KERNEL_64__ -Wl,-m -Wl,elf_x86_64 -static -nostdlib -z max-page-size=0x1000 -static -nostdlib -u _camkes_start -e _camkes_start -Wl,--script=/host/test/projects/camkes/ethdriver/linker.lds /host/test/lib/crt1.o /host/test/lib/crti.o /usr/lib/gcc/x86_64-linux-gnu/6/crtbegin.o projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/ethdriver.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/common.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/82574.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/camkes.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/camkes.simple.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/camkes.environment.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/EthDriver_seL4HardwareMMIO_0.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/irq_seL4HardwareInterrupt_0.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/client_seL4Ethdriver_0.c.obj -lgcc -lgcc_eh libsel4/libsel4.a projects/camkes-tool/libsel4camkes/libsel4camkes.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/util_libs/libutils/libutils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libethdrivers/libethdrivers.a projects/projects_libs/libvirtqueue/libvirtqueue.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4debug/libsel4debug.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4vka/libsel4vka.a libsel4/libsel4.a projects/util_libs/libplatsupport/libplatsupport.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a projects/util_libs/libpicotcp/picotcp_external/picotcp/build//lib/libpicotcp.a -lgcc -lgcc_eh libsel4/libsel4.a projects/camkes-tool/libsel4camkes/libsel4camkes.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/util_libs/libutils/libutils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libethdrivers/libethdrivers.a projects/projects_libs/libvirtqueue/libvirtqueue.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4debug/libsel4debug.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4vka/libsel4vka.a libsel4/libsel4.a projects/util_libs/libplatsupport/libplatsupport.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a projects/util_libs/libpicotcp/picotcp_external/picotcp/build//lib/libpicotcp.a /usr/lib/gcc/x86_64-linux-gnu/6/crtend.o /host/test/lib/crtn.o -o projects/camkes/ethdriver.instance.bin && : /usr/bin/ld: projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/common.c.obj: in function `camkes_iommu_dma_alloc': /host/test/../projects/global-components/components/Ethdriver/src/plat/pc99/common.c:48: undefined reference to `sel4utils_iommu_dma_alloc_iospace' /usr/bin/ld: projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/common.c.obj: in function `pc99_eth_setup': /host/test/../projects/global-components/components/Ethdriver/src/plat/pc99/common.c:71: undefined reference to `simple_get_iospace' /usr/bin/ld: /host/test/../projects/global-components/components/Ethdriver/src/plat/pc99/common.c:88: undefined reference to `sel4utils_make_iommu_dma_alloc' I checked all the files in the Ethdriver component and for me it seems that all should be fine, thus I cannot find/see the error (or the missing configuration). (The only file I edited was picoserver.camkes but that is irrelevant.) Any help/hint would be very appreciated. Best regards, Benjamin

1 1

seL4 process memory utilization
by Leonid Meyerovich 26 Apr '19

26 Apr '19

Hello, Is there any way in seL4 (library function?) to check free heap memory? Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

4 5

Interested in Contributing to SeL4
by Aditya Upadhyay 26 Mar '19

26 Mar '19

Hi Developers, This is Aditya Upadhyay, would like to contribute in SeL4 microkernel. I am trying to figure out any open projects on wiki page of SeL4 Systems. One project that is related to POSIX Compliance. I can see here: https://docs.sel4.systems/SuggestedProjects.html but I am still figuring out the stuff to contribute. Any Valuable suggestions would be appreciated. Would you like to point any blogs related to SeL4? I have some experience of contributing the code in Open Source Organisation Newlib-Cygwin. I was working on POSIX Compliance for RTEMS as a part of Google Summer of Code 2017 Students internship. To stick to Open Source, I am mentoring RTEMS Google Summer of Code Project this year also. I have always learned from mentoring and contributing to open source. I have deep understanding of Linux Operating System Internals and Monolithic Kernels as well. I am also looking for Research Internship in Distributed Systems especially in Microkernel and Microhypervisor field. I am open for any research oriented projects in this field. Regards, Aditya Upadhyay

3 2

Re: [seL4] Devel Digest, Vol 58, Issue 5
by KIM MK 26 Mar '19

26 Mar '19

Okay! Aditya, Let’s research together :) BR, MK Sent from my iPhone > On 26 Mar 2019, at 6:43 AM, "devel-request(a)sel4.systems" <devel-request(a)sel4.systems> wrote: > > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Re: some questions about camkes-manifest > (Anna.Lyons(a)data61.csiro.au) > 2. Interested in Contributing to SeL4 (Aditya Upadhyay) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Mon, 25 Mar 2019 02:23:22 +0000 > From: <Anna.Lyons(a)data61.csiro.au> > To: <yadong.li(a)horizon.ai>, <devel(a)sel4.systems> > Subject: Re: [seL4] some questions about camkes-manifest > Message-ID: <1553480602203.73891(a)data61.csiro.au> > Content-Type: text/plain; charset="iso-8859-1" > > Hi, > > > 1. You can find the library in https://github.com/SEL4PROJ/projects_libs? > > 2. Sorry, we do not have any public demos that use this library. It has mainly been used in experimental contexts. > > > Cheers > > Anna. > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: <http://sel4.systems/pipermail/devel/attachments/20190325/580f5330/attachmen…> > > ------------------------------ > > Message: 2 > Date: Mon, 25 Mar 2019 22:01:09 +0530 > From: Aditya Upadhyay <aditya.sidd.upadhyay(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Interested in Contributing to SeL4 > Message-ID: > <CAP7bF08qCr2dxd=WwbRwKuJP8ZqNc1RswNJbsfnyZ5Dxg1rjCg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Hi Developers, > > This is Aditya Upadhyay, would like to contribute in SeL4 microkernel. > > I am trying to figure out any open projects on wiki page of SeL4 Systems. > One project that is related to POSIX Compliance. I can see here: > https://docs.sel4.systems/SuggestedProjects.html > but I am still figuring out the stuff to contribute. Any Valuable > suggestions would be appreciated. Would you like to point any blogs related > to SeL4? > > I have some experience of contributing the code in Open Source Organisation > Newlib-Cygwin. I was working on POSIX Compliance for RTEMS as a part of > Google Summer of Code 2017 Students internship. > > To stick to Open Source, I am mentoring RTEMS Google Summer of Code Project > this year also. I have always learned from mentoring and contributing to > open source. > > I have deep understanding of Linux Operating System Internals and > Monolithic Kernels as well. I am also looking for Research Internship in > Distributed Systems especially in Microkernel and Microhypervisor field. I > am open for any research oriented projects in this field. > > Regards, > Aditya Upadhyay > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: <http://sel4.systems/pipermail/devel/attachments/20190325/3cbbe26b/attachmen…> > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 58, Issue 5 > ************************************

1 0

speed up sel4
by Sreenadh S 26 Mar '19

26 Mar '19

When running sel4 in my processor it is taking too long to get this line "vka_alloc_object_at_maybe_dev@object.h:65 Failed to allocate object of size 268435456, error 1" Is there any options to reduce allocation object size? Or any other methods to speed up Regards, Sreenadh S CDAC, Trivandrum, India

2 1

some questions about camkes-manifest
by yadong.li 25 Mar '19

25 Mar '19

hi, I have some questions about camkes-manifest 1、I find the libsdhcdrivers in /projects/projects_libs of the project. But where can I find the superset of these libs by git? I can't find the maintenance branch about libsdhcdrivers (like 'seL4_libs' ) in https://github.com/seL4 2、I can't find who use the function of libsdhcdrivers, what is the plan of the lib ? Is there some demo using sdhc ? Thank you very much

2 1

Hello. Nice to meet you. I’m MK
by KIM MK 11 Mar '19

11 Mar '19

Hello Micro kernel develper I’m MK. Nice to meet u. I’ll research and commit ARMv8 and virtualization in Sel4 你好。谢谢。 반갑습니다 Thank you BR， MK Sent from my iPhone

1 0

How to (and how not to) use seL4 IPC
by Gernot.Heiser＠data61.csiro.au 11 Mar '19

11 Mar '19

Folks might be interested in this blog: https://microkerneldude.wordpress.com/2019/03/07/how-to-and-how-not-to-use-… Gernot

2 3

ENTROPY 2019: Second Call for Papers
by Toby.Murray＠data61.csiro.au 20 Feb '19

20 Feb '19

NEW: two more invited speakers ********************************************************************** Second Call for papers — ENTROPY 2019 ENabling TRust through Os Proofs … and beYond Second International workshop on the use of theorem provers for modelling and verification at the hardware-software interface https://protect-au.mimecast.com/s/h5JtCjZroMFQkjkKFW-1Th?domain=entropy2019… Co-located with EuroS&P'19, KTH, Stockholm, June 2019 ********************************************************************** INVITED SPEAKERS Dominique Bolignano, Prove & Run Gernot Heiser, University of New South Wales Frank Piessens, KU Leuven Peter Sewell, University of Cambridge IMPORTANT DATES Paper submission: March 11 2019 Author notification: April 10, 2019 Camera-ready versions: April 22, 2019 (strict) Workshop: 16 June 2019 AIM AND SCOPE Low level software such as kernels and drivers, along with the hardware this software runs on, is critical for application security. In contrast with user applications, OS kernel software runs in privileged CPU mode and is thus highly critical. Large projects such as seL4, VeriSoft, CertiKoS and Prosper have invested considerable resources in developing formally verified systems such as hypervisors and microkernels, supplying proofs that they satisfy critical properties. Such proofs are delicate in terms of the scale and complexity of real systems, the models used in performing the proof search, and the relations between the two, which recent vulnerabilities such as Spectre and Meltdown have shown to be a highly non-trivial issue. The purpose of this workshop is to share, compare and disseminate best practices, tools and methodologies to verify OS kernels, also setting the stage for future steps in the direction of fully verified systems, dealing with issues related to modelling, model validation, and large proof maintenance through system evolution. On one hand, we need to make low-level proofs more scalable, modular and cost-effective. On the other hand, once certified systems are available, preservation and maintenance of their proofs of validity become key questions. The goal of the ENTROPY workshop is to provide a forum for researchers and practitioners in this space, linking operating systems, formal methods, and hardware architecture, interested in system design as well as machine verified mathematical proofs using proof assistants such as Coq, Isabelle and HOL4. This will be the second edition of the ENTROPY workshop series. The first workshop was organised by the Pip Development Team at University of Lille in 2018. TOPICS OF INTEREST Specific topics include, but are not limited to: * Verified kernels and hypervisors * Verified security architectures and models * Tools and frameworks for hardware security analysis * Tools and frameworks for security analysis * Formal hardware models and model validation techniques * Theorem prover based tools and frameworks for verification of low level code * Combinations of static analysis and theorem proving * Theories and techniques for compositional security analysis * Case studies and industrial experience reports * Proof maintenance techniques and problems * Compositional models and verification techniques * Proof oriented design The aim of the workshop is to stimulate innovation and active exchange of ideas, so position papers, work-in-progress and industrial experience submissions are welcome. SUBMISSION AND PUBLICATION There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (10 pages, references included, IEEE format) 2. Short papers, position papers, industry experience reports, work-in-progress submissions (4 pages, references included, IEEE format) All papers should be in English and describe original work that has not been published or submitted elsewhere. The submission category should be clearly indicated. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in IEEE Xplore in a companion volume to the regular EuroS&P proceedings. For formatting and submission instructions see https://protect-au.mimecast.com/s/h5JtCjZroMFQkjkKFW-1Th?domain=entropy2019…. PROGRAM CHAIRS Mads Dam, KTH Royal Institute of Technology David Nowak, CNRS and University of Lille PROGRAM COMMITTEE Christoph Baumann, Ericsson AB Gustavo Betarte, Univ. de la República, Uruguay David Cock, ETH Zurich Mads Dam, KTH Royal Institute of Technology (chair) Anthony Fox, ARM Deepak Garg, MPI Saarbrucken Ronghui Gu, Columbia University Samuel Hym, Univ. Lille Thomas Jensen, INRIA and Univ. Rennes Toby Murray, Univ. Melbourne David Nowak, CNRS & Univ. Lille (chair) Vicente Sanchez-Leighton, Orange Labs Thomas Sewell, Chalmers

1 0

Re: [seL4] port SeL4 to renesas rcar-H3 development board
by Diego Alejandro Parra Guzman 20 Feb '19

20 Feb '19

Hi guys !!! Thank you for your quick replay. I'm try to port Sel4 kernel to the* renesas H3 ULCB* board with two clusters (ARM57),(ARM53) each one with 4 cores I just have couple of questions regarding with the elf loader in sel4-tools: there is some files in* elfloader-tool/plat/** those are intended to initialize the CPU and the UART on the platform. In there, there is a function written in assembly called *core_entry_head* and a function *init_cpus*implemented in smp.c file. *Could you please explain me a little bit what is the purpose of these functions ? * In the case of *init_cpus* where is suppose to be that information? I means, I should reference the ARM57 or ARM53 cpu manual or maybe to the boot section in the SoC manual. from the other hand the *renesas H3 ULCB* doesn't have a physical UART port. Instead, it has an Serial Communication Interface with FIFO (SCIF) that can be configure properly to be compatible with *UART* interfaces. The point is that I'm using this interface in order to implement the * __fputc()* function following the one implemented in sys_fput.c file. Unfortunately, I don't understand why in your implementation there is not an initialization for the *UART. could you tell me why not?* Thank you. best regards On Sat, 16 Feb 2019 at 06:57, Diego Alejandro Parra Guzman < daparrag(a)correo.udistrital.edu.co> wrote: > Hi guys !!! > > Thank you for your quick replay. > > I'm try to port Sel4 kernel to the* renesas H3 ULCB* board with two > clusters (ARM57),(ARM53) each one with 4 cores > > I just have couple of questions regarding with the elf loader in > sel4-tools: > > there is some files in* elfloader-tool/plat/** those are intended to > initialize the CPU and the UART on the platform. In there, there is a > function written in assembly called *core_entry_head* and a function > *init_cpus*implemented in smp.c file. > *Could you please explain me a little bit what is the purpose of these > functions ? * > > In the case of *init_cpus* where is suppose to be that information? I > means, I should reference the ARM57 or ARM53 cpu manual or maybe to the > boot section in the SoC manual. > > > from the other hand the *renesas H3 ULCB* doesn't have a physical UART > port. Instead, it has an Serial Communication Interface with FIFO (SCIF) > that can be configure properly to be compatible with *UART* interfaces. > The point is that I'm using this interface in order to implement the > * __fputc()* function following the one implemented in sys_fput.c file. > Unfortunately, I don't understand why in your implementation there is > not an initialization for the *UART. could you tell me why not?* > > Thank you. > > best regards > > On Wed, 13 Feb 2019 at 15:21, Diego Alejandro Parra Guzman < > daparrag(a)correo.udistrital.edu.co> wrote: > >> >> Hi, >> >> I'm new with seL4 kernel and I would like to port it to the ARM-based >> renesas rcar-H3 board >> >> I would like to ask of you have a development manual that i can follow >> with some basics about how to do it? >> >> I followed the tutorials and so one. But I will appreciate if you have >> something guidelines to start. >> >> Thank you >> >> BR >> Diego. >> -- >> Diego Alejandro Parra Guzmán >> Estudiante de ingeniería electrónica >> Universidad distrital FJC >> > > > -- > Diego Alejandro Parra Guzmán > Estudiante de ingeniería electrónica > Universidad distrital FJC > -- Diego Alejandro Parra Guzmán Estudiante de ingeniería electrónica Universidad distrital FJC

2 3

sel4 at Developers Conference 2019
by Jheengut Pritvi 14 Feb '19

14 Feb '19

Hi, I have been following and keeping track of the development of sel4 for more than 3 years. Unfortunately, I have not been able to install sel4 on my odroid U3 and it also has been a long time that I have built and run sel4. I am also part of the organising team of the Developers Conference since 2015 and this year is the fifth edition held in the Voila hotel and Flying Dodo in Bagatelle in the Republic of Mauritius. This year, I have a session about sel4. https://sessionize.com/s/jheengut/an_introduction_to_the_sel4_microke/21360 I would be highly pleased to have a piece of your opinion on this matter. Cheers Pritvi Jheengut

1 0

port SeL4 to renesas rcar-H3 development board
by Diego Alejandro Parra Guzman 14 Feb '19

14 Feb '19

Hi, I'm new with seL4 kernel and I would like to port it to the ARM-based renesas rcar-H3 board I would like to ask of you have a development manual that i can follow with some basics about how to do it? I followed the tutorials and so one. But I will appreciate if you have something guidelines to start. Thank you BR Diego. -- Diego Alejandro Parra Guzmán Estudiante de ingeniería electrónica Universidad distrital FJC

4 3

Poll for Separation Kernel (microkernel) CC Protection Profile
by Holger Blasum 21 Jan '19

21 Jan '19

Hello seL4 devel, microkernel-based systems can be used as separation kernels[*] for security. At the moment there is a poll on input for a Common Criteria for Information Technology Security (CC) separation kernel protection profile draft, organized by a certMILS.eu colleague from Rostock Univ, at https://evasys.uni-rostock.de/evasys/online.php?p=ccuf-sk-wg The idea is to have a base protection profile (PP) that all players can agree with and to specify additional functionality as add-ons to the PP (e.g., in the form of PP modules). The questionnaire is an opportunity to provide early feedback. Note that there are no mandatory questions, i.e. you can freely move around / you can leave any question unanswered - the only condition for your feedback be submitted to the collection system is that you go to the last page and use the submit button there. We invite feedback via that poll by end of this week. If, beyond the questionnaire, you want to join the Common Criteria User's Forum separation kernel working group, or anyone would like to have more time, just let me know by answering to this email. [*] https://en.wikipedia.org/wiki/Multiple_Independent_Levels_of_Security Best, -- Holger Blasum, SYSGO

1 1

seL4 Training and ARMv8 virtualization release
by Robert VanVossen 19 Jan '19

19 Jan '19

All, We at DornerWorks wanted to let the seL4 community know about some seL4 training opportunities that we will be providing on behalf of the seL4 Center of Excellence (CoE). First, we will be providing an introductory webinar that provides an overview and explains the basics of seL4. Webinar: Intro to seL4 Thursday, February 7 11 a.m. EST Register Now: https://dornerworks.clickmeeting.com/intro-to-sel4/register Second, a more advanced two day training will take place on March 7th. This is a paid training that will provide information on seL4, libraries, CAmkES, the proof, and supported platforms. The training will also have hands-on labs that will include configuring CAmkES applications, debugging seL4 applications with GDB, and writing an HTTP server application to serve as a real life example. You can see more information and sign up here: https://www.sae.org/learn/content/c1874/ Finally, we wanted to let people know about our release of our ARMv8 virtualization feature. We recently received approval to release these features to the public. We have a press release providing additional details, a link to the code, and user instructions: https://dornerworks.com/news/new-commits-to-open-source-sel4. Currently, the release is on the DornerWorks github and based on an earlier version of seL4 and its libraries. We are working with Data61 to update to the latest versions and then mainline into the Data61 repositories. This may take some time as we integrate our ARMv8 virtualization code with Data61's ARMv8 virtualization code. Cheers, Robbie VanVossen DornerWorks, Ltd.

1 0

ENTROPY 2019: Call for Papers
by Toby Murray 13 Jan '19

13 Jan '19

************************************************************************** Call for papers — ENTROPY 2019 ENabling TRust through Os Proofs … and beYond Second International workshop on the use of theorem provers for modelling and verification at the hardware-software interface Co-located with EuroS&P'19, KTH, Stockholm, June 2019 ************************************************************************** AIM AND SCOPE Low level software such as kernels and drivers, along with the hardware this software runs on, is critical for application security. In contrast with user applications, OS kernel software runs in privileged CPU mode and is thus highly critical. Large projects such as seL4, VeriSoft, CertiKoS and Prosper have invested considerable resources in developing formally verified systems such as hypervisors and microkernels, supplying proofs that they satisfy critical properties. Such proofs are delicate in terms of the scale and complexity of real systems, the models used in performing the proof search, and the relations between the two, which recent vulnerabilities such as Spectre and Meltdown have shown to be a highly non-trivial issue. The purpose of this workshop is to share, compare and disseminate best practices, tools and methodologies to verify OS kernels, also setting the stage for future steps in the direction of fully verified systems, dealing with issues related to modelling, model validation, and large proof maintenance through system evolution. On one hand, we need to make low-level proofs more scalable, modular and cost-effective. On the other hand, once certified systems are available, preservation and maintenance of their proofs of validity become key questions. The goal of the ENTROPY workshop is to provide a forum for researchers and practitioners in this space, linking operating systems, formal methods, and hardware architecture, interested in system design as well as machine verified mathematical proofs using proof assistants such as Coq, Isabelle and HOL4. This will be the second edition of the ENTROPY workshop series. The first workshop was organised by the Pip Development Team at University of Lille in 2018. TOPICS OF INTEREST Specific topics include, but are not limited to: * Verified kernels and hypervisors * Verified security architectures and models * Tools and frameworks for hardware security analysis * Tools and frameworks for security analysis * Formal hardware models and model validation techniques * Theorem prover based tools and frameworks for verification of low level code * Combinations of static analysis and theorem proving * Theories and techniques for compositional security analysis * Case studies and industrial experience reports * Proof maintenance techniques and problems * Compositional models and verification techniques * Proof oriented design The aim of the workshop is to stimulate innovation and active exchange of ideas, so position papers, work-in-progress and industrial experience submissions are welcome. INVITED SPEAKERS (to be extended) Frank Piessens, KU Leuven Peter Sewell, Univ. Cambridge IMPORTANT DATES Paper submission: March 11 2019 Author notification: April 10, 2019 Camera-ready versions: April 22, 2019 (strict) Workshop: 16 June 2019 SUBMISSION AND PUBLICATION There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (8 pages, references included, IEEE format) 2. Short papers, position papers, industry experience reports, work-in-progress submissions: (4 pages, references included, IEEE format) All papers should be in English and describe original work that has not been published or submitted elsewhere. The submission category should be clearly indicated. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in IEEE Xplore in a companion volume to the regular EuroS&P proceedings. For formatting and submission instructions see https://entropy2019.sciencesconf.org. PROGRAM CHAIRS Mads Dam, KTH Royal Institute of Technology David Nowak, CNRS and University of Lille PROGRAM COMMITTEE Christoph Baumann, Ericsson AB Gustavo Betarte, Univ. de la República, Uruguay David Cock, ETH Zurich Mads Dam, KTH Royal Institute of Technology (chair) Anthony Fox, ARM Deepak Garg, MPI Saarbrucken Ronghui Gu, Columbia University Samuel Hym, Univ. Lille Thomas Jensen, INRIA and Univ. Rennes Toby Murray, Univ. Melbourne David Nowak, CNRS & Univ. Lille (chair) Vicente Sanchez-Leighton, Orange Labs Thomas Sewell, Chalmers -- Toby Murray, DPhil (University of Oxford) Senior Lecturer, School of Computing and Information Systems University of Melbourne http://people.eng.unimelb.edu.au/tobym/ toby.murray(a)unimelb.edu.au

1 0

Running 2 VM Linux on Camkes
by Amit Goyal 09 Jan '19

09 Jan '19

Hi, I am using Ubuntu 16.04 on 64 Bit, i7 machine and following CAmkES x86 VM instructions available at: https://docs.sel4.systems/CAmkESVM I am able to successfully run single guest vm. I am now trying to run 2 guest vms at the same time. For this, I changed a) minimal.camkes as follows: -------------------------------------------------------------------------------------------------------------------------------- #ifdef HAVE_AUTOCONF #include <autoconf.h> #endif import <VM/vm.camkes>; #include <configurations/vm.h> #define VM_GUEST_CMDLINE "earlyprintk=ttyS0,115200 console=ttyS0,115200 i8042.nokbd=y i8042.nomux=y \ i8042.noaux=y io_delay=udelay noisapnp pci=nomsi debug root=/dev/mem" component Init0 { VM_INIT_DEF() } component Init1 { VM_INIT_DEF() } assembly { composition { VM_COMPOSITION_DEF() VM_PER_VM_COMP_DEF(0) VM_PER_VM_COMP_DEF(1) } configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0) VM_PER_VM_CONFIG_DEF(1) 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; vm1.simple_untyped23_pool = 20; vm1.heap_size = 0x2000000; vm1.guest_ram_mb = 128; vm1.kernel_cmdline = VM_GUEST_CMDLINE; vm1.kernel_image = "bzimage"; vm1.kernel_relocs = "bzimage"; vm1.initrd_image = "rootfs.cpio"; vm1.iospace_domain = 0x0f; } } --------------------------------------------------------------------------------------------------------------------------------- b) CMakeLists.txt as follows: --------------------------------------------------------------------------------------------------------------------------------- cmake_minimum_required(VERSION 3.8.2) project(minimal) # Include CAmkES VM helper functions include("../../vm/camkes_vm_helpers.cmake") include("../../vm-linux/vm-linux-helpers.cmake") # Declare VM component: Init0 DeclareCAmkESVM(Init0) DeclareCAmkESVM(Init1) # Get Default Linux VM files GetDefaultLinuxKernelFile(kernel_file) GetDefaultLinuxRootfsFile(rootfs_file) # Decompress Linux Kernel image and add to file server DecompressLinuxKernel(extract_linux_kernel decompressed_kernel ${kernel_file}) AddToFileServer("bzimage" ${decompressed_kernel} DEPENDS extract_linux_kernel) # Add rootfs images into file server AddToFileServer("rootfs.cpio" ${rootfs_file}) # Initialise CAmkES Root Server with addition CPP includes DeclareCAmkESVMRootServer(minimal.camkes) --------------------------------------------------------------------------------------------------------------------------------- I can successfully build the system and 2 vm images are being created namely: vm0_group.bin, vm1_group.bin On running the system using: sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=true --mem-size 2G --extra-cpu-opts "+vmx" --extra-qemu-args="-enable-kvm -net nic,model=e1000 -net tap,script=no,ifname=tap0" I get the following error: --------------------------------------------------------------------------------------------------------------------------------- <<seL4(CPU 0) [decodeUntypedInvocation/209 T0xffbfec00 "rootserver" @804853d]: Untyped Retype: Insufficient memory (1 * 4194304 bytes needed, 2048 bytes available).>> <<seL4(CPU 0) [decodeInvocation/542 T0xffbfec00 "rootserver" @804853d]: Attempted to invoke a null cap #0.>> create_objects@main.c:767 [Err seL4_InvalidCapability]: Untyped retype failed with unexpected error seL4 root server abort()ed Debug halt syscall from user thread 0xffbfec00 "rootserver" halting... Kernel entry via Unknown syscall, word: 523QEMU: Terminated --------------------------------------------------------------------------------------------------------------------------------- I have 2 doubts: a) Can someone suggest a possible way to get this running. b) Is it possible to see the 2 VMs running on separate terminals at the same time. -- Thanks and Regards, Amit Goyal

2 2

An RFC process for seL4
by Curtis.Millar＠data61.csiro.au 02 Jan '19

02 Jan '19

Hi Everyone, We are currently in the process of setting up and moving to a public Jira instance to manage many of our development issues. The first part of this move involves setting up a request for comments (RFC) process which will be implemented using a Jira project. You can find out more about the RFC process in the first RFC: https://sel4kernel.atlassian.net/browse/RFC-1 You are encouraged to leave feedback on the issue, but doing so requires that you are logged in with an Atlassian Cloud account. The introduction of a public issue tracker will allow us to better engage with our community, accept more contribution from outside the seL4 development team, and better communicate the ways in which we are changing and improving the seL4 ecosystem. In the long term, we hope to use this to track all of the major issues currently under development across the ecosystem, accept issues submitted by the public, and open issues up for members of the greater community to work on. The issue tracker will initially be used as the basis of the RFC process, which will allow for the community to get involved with larger changes to the ecosystem. Many of the details of the process can only be clearly resolved as it becomes used more regularly as part of ongoing development, so much of how it works is still to be determined. We are hoping to finalise this process at the beginning of the new year before we use it to present a number of other changes we have been planning so we can get your feedback before their design and implementation is finalised. This new issue tracker and RFC process are just part of greater ongoing changes on which we are working to grow the community and to increase its involvement. We wish you all a happy holiday season and look forward to the start of a new year with seL4. Cheers, Curtis

2 2

seL4 at 35C3 in Leipzig (Chaos Communication Congress)
by Daniel Schäfer 27 Dec '18

27 Dec '18

Hey there, are some of you going to the 35C3 congress in Leipzig, Germany? I'm trying to understand seL4 and get into developing for it. I'd love to talk to someone if anyone's around. Best regards and merry Christmas, Daniel P.S. My "home" is the Selfnet assembly

1 0

Fwd: CAmkES tutorial build system
by Wei Xiang Leow 19 Dec '18

19 Dec '18

Hello Kent, Thanks for the reply :) The moving/copying was to demonstrate the differences between the tutorial and the solution. Creating and completing a new copy of the tutorial doesn't give the expected results either. My understanding is, when we run "./init --tut hello-camkes-1", the build directory is immediately built off the incomplete tutorial, hence it's missing client.instance.bin.dir etc. This isn't fixed when we complete the tutorial and ninja. Hence when someone goes through the tutorial, it doesn't give the expected "Starting the client". If this is the case, could you point me to where I can rectify this? On an separate note, I'm experiencing the same issues as https://sel4.systems/pipermail/devel/2018-October/002221.html. The simulate script exists, but qemu (at least 2.5.0+) seems to only allow "kernel-irqchip=on|off", not split. May I know which version of qemu we should be using? Regards, Leow Wei Xiang On Tue, Dec 18, 2018 at 2:10 PM <Kent.Mcleod(a)data61.csiro.au> wrote: > Hi, > > > Renaming the source directory and the build directories aren't supported > as CMake and Ninja rely on the absolute and relative paths remaining > consistent. You are still able to copy the contents of the source > directory from the solution into the source directory of the non solution > and use the same build directory. The reason why you only see ...Booting all > finished is because when the tutorial starts, there are no components > defined in the camkes assembly, so no components will be loaded by the > initial task. This is why you don't see any output. > > > I don't believe there is an issue, but let me know if I have misunderstood > what you meant. > > > Kind regards, > > Kent. > > > > ------------------------------ > *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Wei Xiang Leow < > leowweixiang1991(a)gmail.com> > *Sent:* Tuesday, December 18, 2018 4:42 PM > *To:* devel(a)sel4.systems > *Subject:* [seL4] CAmkES tutorial build system > > Hello, there seem to be issues with the tutorial build system, at least > for CAmkES tutorial 1. After adding the necessary details and running, I > get "...Booting all finished", no further messages. The solution runs fine, > I get "Starting the client" etc. > > Made fresh copies of the tutorial and solution, and overwrote the > tutorial's files with the solution's. Diff shows that only .tute_config > (--solution) and the .md files differ. Diff on the "_build" folders shows > multiple differences. I assume there is an issue there? > > mkdir tutorial; mkdir solution > ./init --tut hello-camkes-1 > mv hello-camkes-1 tutorial > mv hello-camkes-1_build tutorial > ./init --tut hello-camkes-1 --solution > mv hello-camkes-1 solution > mv hello-camkes-1_build solution > cp solution/hello-camkes-1/hello-1.camkes > tutorial/hello-camkes-1/hello-1.camkes > diff -rq tutorial/hello-camkes-1 solution/hello-camkes-1 > ############################ > Files tutorial/hello-camkes-1/hello-camkes-1.md and > solution/hello-camkes-1/hello-camkes-1.md differ > Files tutorial/hello-camkes-1/.tute_config and > solution/hello-camkes-1/.tute_config differ > ############################ > > diff -rq tutorial/hello-camkes-1_build solution/hello-camkes-1_build > ############################ > Files tutorial/hello-camkes-1_build/build.ninja and > solution/hello-camkes-1_build/build.ninja differ > Files tutorial/hello-camkes-1_build/CMakeFiles/CMakeOutput.log and > solution/hello-camkes-1_build/CMakeFiles/CMakeOutput.log differ > Files tutorial/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt and > solution/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt differ > Files tutorial/hello-camkes-1_build/hello-camkes-1/ast.pickle and > solution/hello-camkes-1_build/hello-camkes-1/ast.pickle differ > Files tutorial/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake and > solution/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake differ > Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: > client.instance.bin.dir > Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: > echo.instance.bin.dir > Files > tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes > and > solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes > differ > Files > tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md > and > solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md > differ > Files tutorial/hello-camkes-1_build/rules.ninja and > solution/hello-camkes-1_build/rules.ninja differ > ############################ > > cp -r tutorial/hello-camkes-1 hello-camkes-1 > cp -r tutorial/hello-camkes-1_build hello-camkes-1_build > cd hello-camkes-1_build > ninja > ./simulate > ############################ > ... > Booting all finished, dropped to user space > ############################ > > <another terminal> > rm -r hello-camkes-1 > rm -r hello-camkes-1_build > cp -r solution/hello-camkes-1 hello-camkes-1 > cp -r solution/hello-camkes-1_build hello-camkes-1_build > cd hello-camkes-1_build > ninja > ./simulate > ############################ > ... > Booting all finished, dropped to user space > Starting the client > ------------------- > Component echo saying: hello world > After the client > ############################ > > Regards, > Leow Wei Xiang >

1 0

CAmkES tutorial build system
by Wei Xiang Leow 18 Dec '18

18 Dec '18

Hello, there seem to be issues with the tutorial build system, at least for CAmkES tutorial 1. After adding the necessary details and running, I get "...Booting all finished", no further messages. The solution runs fine, I get "Starting the client" etc. Made fresh copies of the tutorial and solution, and overwrote the tutorial's files with the solution's. Diff shows that only .tute_config (--solution) and the .md files differ. Diff on the "_build" folders shows multiple differences. I assume there is an issue there? mkdir tutorial; mkdir solution ./init --tut hello-camkes-1 mv hello-camkes-1 tutorial mv hello-camkes-1_build tutorial ./init --tut hello-camkes-1 --solution mv hello-camkes-1 solution mv hello-camkes-1_build solution cp solution/hello-camkes-1/hello-1.camkes tutorial/hello-camkes-1/hello-1.camkes diff -rq tutorial/hello-camkes-1 solution/hello-camkes-1 ############################ Files tutorial/hello-camkes-1/hello-camkes-1.md and solution/hello-camkes-1/hello-camkes-1.md differ Files tutorial/hello-camkes-1/.tute_config and solution/hello-camkes-1/.tute_config differ ############################ diff -rq tutorial/hello-camkes-1_build solution/hello-camkes-1_build ############################ Files tutorial/hello-camkes-1_build/build.ninja and solution/hello-camkes-1_build/build.ninja differ Files tutorial/hello-camkes-1_build/CMakeFiles/CMakeOutput.log and solution/hello-camkes-1_build/CMakeFiles/CMakeOutput.log differ Files tutorial/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt and solution/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt differ Files tutorial/hello-camkes-1_build/hello-camkes-1/ast.pickle and solution/hello-camkes-1_build/hello-camkes-1/ast.pickle differ Files tutorial/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake and solution/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake differ Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: client.instance.bin.dir Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: echo.instance.bin.dir Files tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes and solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes differ Files tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md and solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md differ Files tutorial/hello-camkes-1_build/rules.ninja and solution/hello-camkes-1_build/rules.ninja differ ############################ cp -r tutorial/hello-camkes-1 hello-camkes-1 cp -r tutorial/hello-camkes-1_build hello-camkes-1_build cd hello-camkes-1_build ninja ./simulate ############################ ... Booting all finished, dropped to user space ############################ <another terminal> rm -r hello-camkes-1 rm -r hello-camkes-1_build cp -r solution/hello-camkes-1 hello-camkes-1 cp -r solution/hello-camkes-1_build hello-camkes-1_build cd hello-camkes-1_build ninja ./simulate ############################ ... Booting all finished, dropped to user space Starting the client ------------------- Component echo saying: hello world After the client ############################ Regards, Leow Wei Xiang

2 1

Multiboot and extra modules
by Dave Richards 18 Dec '18

18 Dec '18

Is it (or would it be) possible to specify more than the single root server module and have seL4 create virtual addresses, cap. Spaces, threads (leaving them suspended) and pass the information about these modules to the root server? In this way it would be possible to have GRUB load a multi-server seL4 environment. Thanks, Dave

6 11

(no subject)
by Виктор Фадеев 14 Dec '18

14 Dec '18

Good day everyone! I want to try to port sel4 to mips. I will be grateful if you give me the literature that will help me understand the structure of sel4 and its logical interaction with arm/riscv.

1 0

Camkes Cross-VM Communication
by Amit Goyal 14 Dec '18

14 Dec '18

Hi All, I am using Ubuntu 16.04 on 64 Bit, i7 machine and running Camkes Cross-VM communication tutorial available at: https://docs.sel4.systems/Tutorials/camkes-vm-crossvm.html I am able to build the system properly but when I run the system, I get the following error: --------------------------------------------------------------------------------------------------------------------------------- Creating dataport node /dev/camkes_reverse_src Creating dataport node /dev/camkes_reverse_dest Allocating 8192 bytes for /dev/camkes_reverse_src dataport_map_guest@cross_vm_dataport.c:25 Dataport guest size and host size are different (8192 and 4096) dataport_vmcall_handler@cross_vm_dataport.c:75 Failed to map dataport into guest VM_FATAL_ERROR ::: vmexit handler return error vmm_print_guest_context:27 | ================== GUEST OS CONTEXT ================= vmm_print_guest_context:30 | exit info : reason 0x12 qualification 0x0 instruction len 0x3 interrupt info 0x0 interrupt error 0x0 vmm_print_guest_context:32 | guest physical 0x0 rflags 0x286 vmm_print_guest_context:34 | guest interruptibility 0x0 control entry 0x34 vmm_print_guest_context:37 | eip 0xd881714a vmm_print_guest_context:39 | eax 0x 1 ebx 0x 1 ecx 0x 1 vmm_print_guest_context:41 | edx 0x16a42000 esi 0x 2000 edi 0x 10 vmm_print_guest_context:43 | ebp 0xd6b17f0c vmm_print_guest_context:45 | cr0 0x80050033 cr3 0x16b1e000 cr4 0x2680 --------------------------------------------------------------------------------------------------------------------------------- I tried troubleshooting it a bit and changed the file: ~/camkes_vm_com/projects/vm-linux/camkes-linux-artifacts/camkes-linux-init-scripts/buildroot_init/camkes_init as follows: Earlier: dataport_init /dev/camkes_reverse_src 8192 /dev/camkes_reverse_dest 8192 Changed: dataport_init /dev/camkes_reverse_src 4096 /dev/camkes_reverse_dest 4096 But this also does not work. Please suggest. -- Thanks and Regards, Amit Goyal

2 2

Patent on formal verification
by Tom Mitchell 11 Dec '18

11 Dec '18

Patents possibly gone wrong. https://www.eff.org/deeplinks/2018/11/stupid-patent-month-patent-using-math… Claim 1 of the patent describes creating mathematical “axioms”—formal mathematical statements—that describe a computerized trading forum. The patented method then describes analyzing, with a “computer assessment system … the mathematical axioms that describe the operation of the trading forum.” In other words, the patent describes using formal proofs to check for bugs in a “computerized trading forum.” It’s formal verification—just applied to the financial services industry. -- T o m M i t c h e l l

1 0

Network lwip for imx6
by wong xuguo 11 Dec '18

11 Dec '18

Hi, I am a student fron Nanjing university, a fresh man of microkernel, specially, know very little about the seL4. Recently I accept a chellange about porting the lwip to sel4, on arch of imx6, does any one could give me a clue? I found the source of camkes does have this code, could I do something to port, to make the lwip work? What my aim is make a tcp echo server. Thank you for all of you help. Best regards from Xuguo Wang

4 4

sel4 on Raspberry Pi 3b Not Working
by Amit Goyal 06 Dec '18

06 Dec '18

Hi All, I tried running seL4 on Raspberry Pi 3b using the following links: https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ https://docs.sel4.systems/Hardware/Rpi3.html https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html#fnref1 I get the following: CACHE: Misaligned operation at range [20000000, 20000014] CACHE: Misaligned operation at range [20008c80, 200092ef] CACHE: Misaligned operation at range [200192f0, 203bb4f0] CACHE: Misaligned operation at range [203bc000, 203c6030] CACHE: Misaligned operation at range [203c6030, 203c8000] ## Starting application at 0x20000000 … and then nothing works and the processor halts. I have tried the pre-built uboot binary, complied uboot versions v2017.1 and v2016.11 as suggested by steve sloloski (on the blog) and uboot version v2016.05 (out of curiosity) but nothing works. Can someone please suggest a possible way out. -- Thanks and Regards, Amit Goyal

2 4

[sel4] Building seL4test for x86_64 on Debian
by Dave Richards 06 Dec '18

06 Dec '18

I thought I got all of the host dependencies installed, but evidently I am doing something wrong. I am building on a Debian 9 (x86_64) system. I ran the init script from the build directory with the -DPLATFORM=x86_64 and -DSIMULATION=0 options. I then ran ninja with no options. Please find attached the output of running these 2 steps. I'd appreciate a gentle nudge in the right direction. Thanks! Dave

1 0

Building seL4x86_64 on Debian
by Dave Richards 05 Dec '18

05 Dec '18

I thought I got all of the host dependencies installed, but evidently I am doing something wrong. I am building on Debian 9 (x86_64) system. I ran the init script from the build directory with the -DPLATFORM=x86_64 and -DSIMULATION=0 options. I then ran ninja with no options. Please find attached the output of running these 2 steps. I'd appreciate a gentle nudge in the right direction. Thanks! Dave

3 2

seL4 cache pinning
by 송대영 02 Dec '18

02 Dec '18

Hi, I read "Improving Interrupt Response Time in a Verifiable Protected Microkernel" paper. This paper improved IPC performance by using cache pinning and I want to know how to implement cache pinnng. But this paper doesn't refer how to manipulate cache lines. Would you give me some methods how to read cache lines and write cache lines?

3 2

Is the ASID used in seL4 by default?
by Dd Nirvana 02 Dec '18

02 Dec '18

Hi guys, I found that seL4's ARM version still need "isb" and "dsb" around updating TTBR0_EL1. This fence will flush the TLB and will affect IPC performance. However, it seems that enabling ASID can avoid this costs. I am not sure, is there any concern that makes seL4 to avoid using ASID? BTW, I have seen ASID management in seL4 (ASID control and ASID pool), so maybe I misunderstood something? Dong Du, Shanghai Jiao Tong University

2 1

sel4bench config problem
by 송대영 24 Nov '18

24 Nov '18

Hi, I have a sel4bench config problem. I use 'ccmake ..' command to configure sel4 configuration but system prints error with this message. Build files have been written to: /home/scribnote5/sel4bench_thesis/build CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:18 (include) CMakeLists.txt:21 (include) Please help me!

2 1

seL4 stack overflow
by Anna.Lyons＠data61.csiro.au 22 Nov '18

22 Nov '18

Hi everyone, I've created a proposal for an seL4 stack overflow, which will complement the mailing list. Please support it! https://area51.stackexchange.com/proposals/120611/sel4?referrer=oNjnX5y9POx… Cheers, Anna.

2 1

seL4 on Raspberry 3
by talos 20 Nov '18

20 Nov '18

Hi Did anyone try seL3 on raspberry pi 3? I tried following these links:https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ https://docs.sel4.systems/Hardware/Rpi3.html https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html#fnref1 I set the serial port 115200, 8N1, but I only got some messy codes, I did not get the booting information! Did anyone find this cases? Thanks Sincerely

2 1

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

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

06 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 31 Oct '18

31 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

Camkes x86 VM Build Error
by Amit Goyal 30 Oct '18

30 Oct '18

Hi, I am using Ubuntu 16.04 on 64 Bit, i7 machine and running the CAmkES x86 VM instructions available at: https://docs.sel4.systems/CAmkESVM After running: ../init-build.sh -DCAMKES_VM_APP=minimal I am getting the following error: -------------------------------------------------------------------------------------------------------------------------------- camkes-gen.cmake is out of date. Regenerating... CMake Error at tools/camkes/camkes.cmake:593 (message): Failed to generate camkes-gen.cmake: Traceback (most recent call last): File "/usr/lib/python2.7/runpy.py", line 174, in _run_module_as_main "__main__", fname, loader, pkg_name) File "/usr/lib/python2.7/runpy.py", line 72, in _run_code exec code in run_globals File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py", line 678, in <module> sys.exit(main(sys.argv, sys.stdout, sys.stderr)) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py", line 515, in main instantiate_misc_templates(renderoptions) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py", line 509, in instantiate_misc_templates outfile_name=outfile.name, imported=read, options=renderoptions) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/Renderer.py", line 109, in render self.templates, **kwargs) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/Context.py", line 261, in new_context }.items()) + list(kwargs.items())) AttributeError: type object 'ObjectType' has no attribute '__members__' Call Stack (most recent call first): CMakeLists.txt:35 (GenerateCAmkESRootserver) -- Configuring incomplete, errors occurred! See also "/home/goyal/sel4/camkes_vm/build_vm/CMakeFiles/CMakeOutput.log". ------------------------------------------------------------------------------------------------------------------------------- I also tried to run the same instructions on a different machine (Ubuntu 16.04, 64 Bit, i5 machine) on which ../init-build.sh -DCAMKES_VM_APP=minimal is run successfully. It gets stuck on running ninja. I am getting the following error: -------------------------------------------------------------------------------------------------------------------------------- ghc-8.0.2: 106.97 MiB / 107.55 MiB ( 99.47%) downloaded... ghc-8.0.2: 107.24 MiB / 107.55 MiB ( 99.71%) downloaded... ghc-8.0.2: 107.50 MiB / 107.55 MiB ( 99.96%) downloaded... ghc-8.0.2: 107.55 MiB / 107.55 MiB (100.00%) downloaded... /home/akshat/.stack/programs/x86_64-linux/ghc-8.0.2.tar.xz.tmp: renameFile:renamePath:rename: does not exist (No such file or directory) Makefile:45: recipe for target 'parse-capDL' failed make: *** [parse-capDL] Error 1 ninja: build stopped: subcommand failed. -------------------------------------------------------------------------------------------------------------------------------- Can someone suggest a way out for both the problems. -- Thanks and Regards, Amit Goyal

2 3

can not build tutorials anymore
by Thad Seeberger 30 Oct '18

30 Oct '18

good day. I can no longer build tutorials. These used to build a month ago. My system hasn't changed and I can still build the older ones with no issues. I get lost trying to debug this cmake/python stuff. ./init --verbose --plat pc99 --tut hello-camkes-1 INFO:sh.command:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>: starting process DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: started process INFO:sh.command:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..', pid 17525>: process started DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: acquiring wait lock to wait for completion DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: got wait lock DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: exit code not set, waiting on pid -- The C compiler identification is GNU 7.3.1 -- The CXX compiler identification is GNU 7.3.1 -- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/gcc -- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /opt/rh/devtoolset-7/root/usr/bin/g++ -- Check for working CXX compiler: /opt/rh/devtoolset-7/root/usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /opt/rh/devtoolset-7/root/usr/bin/gcc CMake Error at projects/sel4-tutorials/cmake/helpers.cmake:141 (message): Failed to render: PYTHONPATH=/home/john/sel4/projects/camkes/capdl/python-capdl-tool;python;/home/john/sel4/projects/sel4-tutorials/template.py;--tut-file;/home/john/sel4/projects/sel4-tutorials/tutorials/hello-camkes-1/hello-camkes-1;--out-dir;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/gen;--input-files;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/input_files;--output-files;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/output_files;--arch;x86_64;;;, Traceback (most recent call last): File "/home/john/sel4/projects/sel4-tutorials/template.py", line 154, in <module> sys.exit(main()) File "/home/john/sel4/projects/sel4-tutorials/template.py", line 142, in main render_file(args, env, state, file) File "/home/john/sel4/projects/sel4-tutorials/template.py", line 90, in render_file out_stream.write(template.render(context.get_context(args, state))) File "/home/john/sel4/projects/sel4-tutorials/tools/context.py", line 435, in get_context context.update(ObjectType.__members__.items()) AttributeError: type object 'ObjectType' has no attribute '__members__' Call Stack (most recent call first): projects/sel4-tutorials/cmake/helpers.cmake:164 (ExecuteGenerationProcess) projects/sel4-tutorials/CMakeLists.txt:29 (GenerateTutorial) -- Configuring incomplete, errors occurred! See also "/home/john/sel4/hello-camkes-1_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 91, in <module> File "./init", line 81, in main File "/home/john/sel4/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/john/sel4/projects/sel4-tutorials/common.py", line 69, in _init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output, _err=output) File "/sandbox/lib/python2.7/site-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/sandbox/lib/python2.7/site-packages/sh.py", line 774, in __init__ self.wait() File "/sandbox/lib/python2.7/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/sandbox/lib/python2.7/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 .. STDOUT: STDERR:

2 2

camkes-arm-vmm run multiple VMs at once
by Daniel Wang 26 Oct '18

26 Oct '18

Hi all, I’m wondering can the camkes-arm-vmm run multiple VMs at once? I know it is possible for X86 but I’m not sure about the ARM version. Thanks Best Regards -Daniel Wang

3 2

Kernel Exception in seL4 Tutorial
by Jeremiah Peschka 25 Oct '18

25 Oct '18

I’m attempting to build the seL4 tutorials on a local VM (Ubuntu 18.04 "Linux ubuntu 4.15.0-36-generic #39-Ubuntu SMP Mon Sep 24 16:19:09 UTC 2018 x86_64 x86_64 x86_64 GNU/Linux”). I have confirmed that the VM has the pre-reqs present and the repository was synced using repo this afternoon. The builds succeed, but running the VM produces a kernel exception. Here is sample output from attempting to build the dynamic-1 tutorial: https://pastebin.com/NnShcREU A similar error occurs when I build the completed solution, as well. Using GDB, it appears that main is never reached. Thanks for any assistance, Jeremiah Peschka

2 6

seL4 IPC SMP
by 송대영 24 Oct '18

24 Oct '18

HI, I have question about IPC on SMP. I ran sel4bench on sabre lite(i.mx6, arm v7) which SMP is on. Sabre lite has 4 cores. I supposed that SMP improved IPC performances. But results were not. seL4_CALL SMP on 504 SMP off 336 Would you give me reason why these results are happened?

2 2

Camkes VM Linux tutorial
by hedi delpazir 23 Oct '18

23 Oct '18

Hi, After running ./init --plat pc99 --tut camkes-vm-linux(following https://docs.sel4.systems/Tutorials/camkes-vm-linux.html) following error will occurred: -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc CMake Error at projects/camkes/vm/camkes_vm_helpers.cmake:21 (ApplyCommonReleaseVerificationSettings): ApplyCommonReleaseVerificationSettings Function invoked with incorrect arguments for function named: ApplyCommonReleaseVerificationSettings Call Stack (most recent call first): camkes-vm-linux/CMakeLists.txt:10 (include) -- camkes-gen.cmake is out of date. Regenerating... -- Configuring incomplete, errors occurred! See also "/home/hedi/sel4-tutorials-manifest/camkes-vm-linux_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 91, in File "./init", line 81, in main File "/home/hedi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/hedi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 69, in _init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output, _err=output) File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 1427, in *call* return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 774, in *init* self.wait() File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DFORCE_IOMMU=ON -DTUTORIAL_DIR=camkes-vm-linux .. STDOUT: STDERR: Any Idea?

2 1

CAmkES-VM Stalling
by Chris Guikema 23 Oct '18

23 Oct '18

Hello, I am seeing a weird issue with the CAmkES-VM. Just last week, I was able to run the VM successfully using the "minimal" version. I followed these steps: $ repo init -u https://github.com/seL4/camkes-vm-examples-manifest.git $ repo sync $ mkdir test && cd test $ ../init-build.sh -DCAMKES_VM_APP=minimal $ ninja Everything compiles correctly. I then had to use ccmake .. to switch the FPU save method to FXSAVE before recompiling. My QEMU command is: $ qemu-system-x86_64 -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 --enable-kvm -smp 1 -cpu Nehalem,+vmx -nographic My QEMU version is: $ qemu-system-x86_64 --version QEMU emulator version 2.5.0 (Debian 1:2.5+dfsg-5ubuntu10.32), Copyright (c) 2003-2008 Fabrice Bellard And I'm running on Ubuntu 16.04. I get as far as: [ 1.930000] clocksource: Switched to clocksource pit [ 2.274669] VFS: Disk quotas dquot_6.6.0 [ 2.324891] VFS: Dquot-cache hash table entries: 1024 (order 0, 4096 bytes) [ 2.463451] hugetlbfs: disabling because there are no supported hugepage sizes [ 2.562973] random: fast init done After that, everything just runs extraordinarily slowly, or ends up stalling out completely. This is a change from a couple weeks previously, were I could get to the login prompt within ~10s using the minimal VM configuration. Has anything changed in the past few weeks that would have caused this? Thanks, Chris

2 1

MCS tutorial
by hedi delpazir 23 Oct '18

23 Oct '18

Hi, After running ninja in build directory(following https://docs.sel4.systems/Tutorials/mcs.html) following error will occurred: [15 of 16] Compiling CapDL.Parser ( CapDL/Parser.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Parser.o ) [16 of 16] Compiling Main ( Main.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/Main.o ) Linking .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL ... capDL-tool-1.0.0.1: copy/register Installing executable(s) in /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin stack install Copying from /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin/parse-capDL to /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build/parse-capDL Copied executables to /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build: - parse-capDL Warning: Installation path /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build not found on the PATH environment variable. ninja: build stopped: subcommand failed. Any idea?

2 1

FOSDEM 2019 - Microkernels developer room - CfP
by Alexander Boettcher 12 Oct '18

12 Oct '18

FYI -------- Forwarded Message -------- Subject: FOSDEM 2019 - Microkernels developer room - CfP Date: Thu, 11 Oct 2018 11:48:24 +0200 From: Sebastian Sumpf <Sebastian.Sumpf(a)genode-labs.com> Reply-To: Genode users mailing list <users(a)lists.genode.org> To: users(a)lists.genode.org FOSDEM 2019 - Microkernels and Component-based OSes devroom CALL FOR PARTICIPATION The developers of several free and open-source microkernel-based operating systems will meet at FOSDEM 2019 [1] in Brussels, Belgium and will share a developer room on Sunday February 03, 2019 [2]. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-, unikernel-, and componenent-based operating systems. Possible topics include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * enabling support for hardware (architectures, device drivers) * used languages and tools * maintenance and testing * security and robustness * trends and challenges * use cases, experiences, lessons learned and demos Please use the Pentabarf [3] system to submit your proposals. You do not need to create a new account if you already have one. When in doubt, please use the devroom mailing list [4]. If you do not want to give a talk yourself, you may still send suggestions for what else you would like to see, or do in the devroom. Please send your suggestions to the mailing list. The deadline for your proposal is on December the 1st 2018. Make sure to include the following in your proposal: * title of your talk (will be printed in the FOSDEM booklet) * your full name (will be printed in the FOSDEM booklet) * a short abstract (one or two paragraphs) * duration of your talk (please, at least 25 and no longer than 55 min) The official devroom schedule (along with the accepted talks) will be announced on December the 15th on the devroom's mailing list and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM website. About FOSDEM FOSDEM is a two-day event organised by volunteers to promote the widespread use of free and open source software. Taking place in the beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the best such conference in Europe. FOSDEM covers a wide spectrum of free and open source software projects, and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) with network/internet connectivity and projectors where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and discussions. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. Every year, FOSDEM hosts more than 5000 developers at the ULB Solbosch campus. Participation and attendance is totally free, though the organisers gratefully accept donations and sponsorship. No registration necessary. About the devroom Since the first Microkernel devroom in 2012 this devroom has been part of each following FOSDEM. By now it has become a somewhat institutionalized tradition for the micro kernel community to meet there; to this date over a dozen projects have participated in one way or another. Each of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the Microkernel devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Social events It also has become a habit that the microkernel projects dine together somewhere in Brussels. The year 2019 will not be any different, so there is going to be a microkernel family dinner on Saturday night. We try place a reservation, so we will inform you about the exact location and time later. Consult the FOSDEM web and other projects for additional social events such as the famous FOSDEM-organized Friday Beer Event and the FOSDEM-arranged free sightseeing tours for spouses. Important dates recap * 01.12.2018: Deadline for submissions * 15.12.2018: Schedule published and speakers notified of acceptance * 03.02.2019: The devroom takes places Links [1] http://fosdem.org [2] https://fosdem.org/2019/practical/transportation [3] https://penta.fosdem.org/submission/FOSDEM19 [4] https://lists.fosdem.org/listinfo/microkernel-devroom See you all at FOSDEM! _______________________________________________ Genode users mailing list users(a)lists.genode.org https://lists.genode.org/listinfo/users

1 0

Reverse back to Original TK1-SOM U-boot
by Daniel Wang 12 Oct '18

12 Oct '18

Hi all, I’m using a TK1-SOM board. Following the document (https://docs.sel4.systems/Hardware/CEI_TK1_SOM/#u-boot <https://docs.sel4.systems/Hardware/CEI_TK1_SOM/#u-boot>) I flashed the U-boot to enable booting HYP mode. How do I reverse back to the original U-boot so that I can boot the original on board Linux? Thank you! Best Regards -Daniel Wang

2 5

US Army SBIR calls for open HW/SW stack
by Gernot.Heiser＠data61.csiro.au 09 Oct '18

09 Oct '18

… and mentions seL4 prominently: https://www.sbir.gov/sbirsearch/detail/1508741

1 0

seL4 IPC fastpath question
by 송대영 08 Oct '18

08 Oct '18

Hello, I have question about seL4 IPC fastpath. I ran sel4bench on sabre lite(arm v7). 1. IPC fastpath can apply in seL4_Call and seL4_Reply_Recv, is it right? seL4_Send, seL4_Recv can't apply IPC fastpath. 2. IPC_fastpath can only send message that message's length is 0, is it right? I found these comments. /* Call slowpath, long IPC (10), same prio client to server, different address space */ /* ReplyRecv slowpath, long IPC (10), same prio server to client, on the slowpath, different address space */ 3. In seL4 IPC mechanism, IPC only use registers not memory?

3 2

Questions on CAMKES-ARM-VM Build and Components
by Daniel Wang 05 Oct '18

05 Oct '18

Hi all, It seems CAmkES-arm-vmm has been immigrated to cmake, How can I build it? I tried to build it by invoking: # ../init-build.sh -DCAMKES_VM_APP=tk1_vm -DPLATFORM=tk1 # ninja But it does not work. Also, thank for the detailed CAmkES X86 documents. I’m wondering does the VM Connector and kernel modules work for ARM architecture, TK1 or TK1-SOM specifically? Best Regards -Daniel Wang

3 6

Does seL4 provide an initrd with a shell?
by Baptiste Lepers 03 Oct '18

03 Oct '18

I have been following the instructions "Fetching, Configuring and Building seL4test" on this page https://docs.sel4.systems/GettingStarted.html. Everything seems to work, but the initrd provided only runs a bunch of tests and then exits. Is there another project that provides a shell or a way for me to launch my own programs? I have tried to follow the instructions on these pages https://docs.sel4.systems/Hardware/Qemu/ and https://docs.sel4.systems/CAmkESVM but the repo init command fails (404). Thanks, Baptiste.

3 4

Problem in Installing Genode OS
by Amit Goyal 03 Oct '18

03 Oct '18

Hi All, I tried to run Genode OS (on x86-64, i5, ubuntu 16.04) via 3 means but could not succeed. Can someone please suggest a possible way out. a) Running iso on virtual box [1] The system complete freezes and the corresponding error is: emR3Debug: rc=VERR_PGM_HANDLER_VIRTUAL_CONFLICT b) Running iso on Qemu [1] The interface appears with following options: Introduction, Web Browser, Seamless Linux, OpenGL, Qt4. but none of the options work on clicking. c) Building the kernel [2] After following all the instructions in [2] and creating the build directory, the last command <<make KERNEL=linux demo>> fails: Error: target 'demo' does not exist Makefile:211: recipe for target 'error_missing_targets' failed make: *** [error_missing_targets] Error 1 [1] https://genode.org/download/live-cds [2] https://genode.org/documentation/developer-resources/getting_started Also, can you please direct us towards any other operating system which is built using the seL4 microkernel. -- Thanks and Regards, Amit Goyal

2 1

Alignment fault without U-Boot Cache Enabled
by Nicholas Pahl 29 Sep '18

29 Sep '18

Hi All, I have noticed an alignment fault in the seL4 elfloader when running seL4 on an AArch64 platform with dcache disabled in U-Boot. The alignment fault is caused by reading the elf files header in the elfloader. The fault can be fixed (hacked) by modifying the length of the elf file name, located before the elf file header, to force a proper alignment. Is the seL4 elfloader intended to be dependent on u-boot enabling the cache?

2 1

How is undefined behavior in x86 ISA handled?
by Wean Irdeh 27 Sep '18

27 Sep '18

Hi all. I was having discussion about how secure handwritten asm code compared to C code in https://board.flatassembler.net/topic.php?p=206126#206117 and someone mentioned that there are undefined behavior in x86 instruction set How is these x86 undefined behavior handled in sel4?

2 1

x86 seL4 kernel bug - kernel page faults on seL4_VMEnter
by Alexander Boettcher 26 Sep '18

26 Sep '18

Hello, during some experimental work on Genode/seL4 and VM extensions, I encountered the issue to trigger a kernel fault. The symptom seems, that if a thread invokes seL4_VMEnter, but the actual thread is not meant/supposed to run a VM, the kernel will (ever?/may?) page fault with a nullpointer access - which effectively renders the whole Genode system unusable. A partial log is attached based on Genode on x86_64 with seL4 kernel version 9.0.1. The fault address points to [0], where the variable _expected_vmcs_ is null and the kernel de-references it. I put a message before this line and print the value of the variable (as visible in the log below). The seL4 10.0.0 code looks similar, so I presume the same issue there . (if the code is not verified - which according to the roadmap is not the case [1] ?) Cheers, Alex B. [0] https://github.com/seL4/seL4/blob/0dd40b6c43a290173ea7782b97afbbbddfa23b36/… [1] https://sel4.systems/Info/Roadmap/home.pml -- 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 diff --git a/src/arch/x86/object/vcpu.c b/src/arch/x86/object/vcpu.c index cf74fa4..68a1dca 100644 --- a/src/arch/x86/object/vcpu.c +++ b/src/arch/x86/object/vcpu.c @@ -1540,6 +1540,7 @@ restoreVMCS(void) } #ifndef CONFIG_KERNEL_SKIM_WINDOW + userError("opps expected_vmcs=%p", expected_vmcs); if (getCurrentCR3().words[0] != expected_vmcs->last_host_cr3) { expected_vmcs->last_host_cr3 = getCurrentCR3().words[0]; vmwrite(VMX_HOST_CR3, getCurrentCR3().words[0]); Boot config: parsing cmdline '/boot/sel4 disable_iommu' Boot config: console_port = 0x1808 Boot config: debug_port = 0x1808 Boot config: disable_iommu = true Detected 1 boot module(s): module #0: start=0xfd58000 end=0xffff330 size=0x2a7330 name='/boot/image.elf' Parsing GRUB physical memory map Physical Memory Region from 0 size 89400 type 1 Physical Memory Region from 89400 size 16c00 type 2 Physical Memory Region from d2000 size 2000 type 2 Physical Memory Region from dc000 size 24000 type 2 Physical Memory Region from 100000 size bb17c000 type 1 Adding physical memory region 0x100000-0xbb27c000 Physical Memory Region from bb27c000 size 6000 type 2 Physical Memory Region from bb282000 size dd000 type 1 Adding physical memory region 0xbb282000-0xbb35f000 Physical Memory Region from bb35f000 size 12000 type 2 Physical Memory Region from bb371000 size 81000 type 4 Physical Memory Region from bb3f2000 size 1d000 type 2 Physical Memory Region from bb40f000 size 60000 type 1 Adding physical memory region 0xbb40f000-0xbb46f000 Physical Memory Region from bb46f000 size 1f9000 type 2 Physical Memory Region from bb668000 size 80000 type 4 Physical Memory Region from bb6e8000 size 27000 type 2 Physical Memory Region from bb70f000 size 8000 type 1 Adding physical memory region 0xbb70f000-0xbb717000 Physical Memory Region from bb717000 size 8000 type 2 Physical Memory Region from bb71f000 size 4c000 type 1 Adding physical memory region 0xbb71f000-0xbb76b000 Physical Memory Region from bb76b000 size c000 type 4 Physical Memory Region from bb777000 size 3000 type 3 Physical Memory Region from bb77a000 size 7000 type 4 Physical Memory Region from bb781000 size 1000 type 3 Physical Memory Region from bb782000 size 9000 type 4 Physical Memory Region from bb78b000 size 1000 type 3 Physical Memory Region from bb78c000 size 13000 type 4 Physical Memory Region from bb79f000 size 60000 type 3 Physical Memory Region from bb7ff000 size 1000 type 1 Adding physical memory region 0xbb7ff000-0xbb800000 Physical Memory Region from bb800000 size 800000 type 2 Physical Memory Region from bc000000 size 4000000 type 2 Physical Memory Region from e0000000 size 10000000 type 2 Physical Memory Region from feaff000 size 1000 type 2 Physical Memory Region from fec00000 size 10000 type 2 Physical Memory Region from fed00000 size 400 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from fed20000 size 70000 type 2 Physical Memory Region from fee00000 size 1000 type 2 Physical Memory Region from ff000000 size 1000000 type 2 Physical Memory Region from 100000000 size 38000000 type 1 Adding physical memory region 0x100000000-0x138000000 Multiboot gave us no video information ACPI: RSDP paddr=0xf68e0 ACPI: RSDP vaddr=0xf68e0 ACPI: RSDT paddr=0xbb7f07a2 ACPI: RSDT vaddr=0xbb7f07a2 ***WARNING*** SKIM window not enabled, this machine is probably vulernable to Meltdown (https://www.meltdownattack.com) consider enabling Kernel loaded to: start=0x200000 end=0xaa5000 size=0x8a5000 entry=0x201209 ACPI: RSDT paddr=0xbb7f07a2 ACPI: RSDT vaddr=0xbb7f07a2 ACPI: FADT paddr=0xbb7f0a00 ACPI: FADT vaddr=0xbb7f0a00 ACPI: FADT flags=0xc2ad ACPI: MADT paddr=0xbb7feb45 ACPI: MADT vaddr=0xbb7feb45 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x1 ACPI: MADT_APIC apic_id=0x4 ACPI: MADT_APIC apic_id=0x5 ACPI: MADT_IOAPIC ioapic_id=1 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: 4 CPU(s) detected ELF-loading userland images from boot modules: size=0x110f000 v_entry=0x2000018 v_start=0x2000000 v_end=0x310f000 p_start=0x10000000 p_end=0x1110f000 Moving loaded userland images to final location: from=0x10000000 to=0xaa5000 size=0x110f000 Starting node #0 with APIC ID 0 Mapping kernel window is done Starting node #1 with APIC ID 1 Starting node #2 with APIC ID 4 Starting node #3 with APIC ID 5 Booting all finished, dropped to user space virtual address layout of core: overall [0000000000002000,00000000c0000000) core image [0000000002000000,000000000310f000) ipc buffer [000000000310f000,0000000003110000) boot_info [0000000003110000,0000000003112000) stack area [0000000040000000,0000000050000000) boot module 'timer' (113344 bytes) boot module 'test-vmm_sel4' (9912 bytes) boot module 'config' (609 bytes) boot module 'ld.lib.so' (937616 bytes) boot module 'init' (352672 bytes) Genode sculpt_vc-2-ge2fd5e5 2909 MiB RAM and 261141 caps assigned to init ... <<seL4(CPU 0) [restoreVMCS/1543 T0xffffff80ba295400 "child of: 'child of: 'rootserver''" @10000c9]: opps _expected_vmcs_=(nil)>> ========== KERNEL EXCEPTION ========== Vector: 0xe ErrCode: 0x0 IP: 0xffffffff80835236 SP: 0xffffffff8087ef18 FLAGS: 0x10086 CR0: 0x8001003b CR2: 0x3298 (page-fault address) CR3: 0xba043000 (page-directory physical address) CR4: 0x6620 Stack Dump: *0xffffffff8087ef18 == 0x10000c9 *0xffffffff8087ef20 == 0xffffffff80a93000 *0xffffffff8087ef28 == 0xffffffff80890040 *0xffffffff8087ef30 == 0x40 *0xffffffff8087ef38 == 0xffffff80ba295400 *0xffffffff8087ef40 == 0xffffffff8087efb8 *0xffffffff8087ef48 == 0xffffffffffffffe7 *0xffffffff8087ef50 == 0xffffffff80a93000 *0xffffffff8087ef58 == 0xffffffff80a93000 *0xffffffff8087ef60 == 0x0 *0xffffffff8087ef68 == 0x0 *0xffffffff8087ef70 == 0xffffffff80890040 *0xffffffff8087ef78 == 0xffffffffffffffff *0xffffffff8087ef80 == 0xffffffff808357fe *0xffffffff8087ef88 == 0xffffffff80a93000 *0xffffffff8087ef90 == 0xffffffff80838c93 *0xffffffff8087ef98 == 0x1001d4 *0xffffffff8087efa0 == 0x0 *0xffffffff8087efa8 == 0xffffffffffffffe7 *0xffffffff8087efb0 == 0xffffffff80839982 Halting... halting... Kernel entry via Interrupt, irq 157

2 2

create a new thread in sel4
by Dongxu Ji 25 Sep '18

25 Sep '18

Hello, My platform is imx6q sabrelite and I have run sel4-test successfully. Now I'm trying to create a new thread in the initial thread according to sel4 tutorial2. But it didn't run. The code is shown below: struct driver_env env; allocman_t *allocman; /* function to run in the new thread */ void thread_2(void) { printf("thread_2: hallo wereld\n"); while (1); } int main(void) { int error; reservation_t virtual_reservation; seL4_BootInfo *info = platsupport_get_bootinfo(); seL4_DebugNameThread(seL4_CapInitThreadTCB, "sel4test-driver"); /* initialise libsel4simple */ simple_default_init_bootinfo(&env.simple, info); /* create an allocator */ allocman = bootstrap_use_current_simple(&env.simple, ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool); /* create a vka */ allocman_make_vka(&env.vka, allocman); /* create a vspace */ error = sel4utils_bootstrap_vspace_with_bootinfo_leaky(&env.vspace, &data, simple_get_pd(&env.simple), &env.vka, platsupport_get_bootinfo()); /* fill the allocator with virtual memory */ void *vaddr; virtual_reservation = vspace_reserve_range(&env.vspace, ALLOCATOR_VIRTUAL_POOL_SIZE, seL4_AllRights, 1, &vaddr); if (virtual_reservation.res == 0) { ZF_LOGF("Failed to provide virtual memory for allocator"); } bootstrap_configure_virtual_pool(allocman, vaddr, ALLOCATOR_VIRTUAL_POOL_SIZE, simple_get_pd(&env.simple)); /* Allocate slots for, and obtain the caps for, the hardware we will be * using, in the same function. */ sel4platsupport_init_default_serial_caps(&env.vka, &env.vspace, &env.simple, &env.serial_objects); vka_t serial_vka = env.vka; serial_vka.utspace_alloc_at = arch_get_serial_utspace_alloc_at(&env); /* Construct a simple wrapper for returning the I/O ports. */ simple_t serial_simple = env.simple; /* enable serial driver */ platsupport_serial_setup_simple(&env.vspace, &serial_simple, &serial_vka); simple_print(&env.simple); /* get our cspace root cnode */ seL4_CPtr cspace_cap; cspace_cap = simple_get_cnode(&env.simple); /* get our vspace root page diretory */ seL4_CPtr pd_cap; pd_cap = simple_get_pd(&env.simple); /* create a new TCB */ vka_object_t tcb_object = {0}; error = vka_alloc_tcb(&env.vka, &tcb_object); /* initialise the new TCB */ error = seL4_TCB_Configure(tcb_object.cptr, seL4_CapNull, cspace_cap, seL4_NilData, pd_cap, seL4_NilData, 0, 0); /* give the new thread a name */ name_thread(tcb_object.cptr, "hello-2: thread_2"); UNUSED seL4_UserContext regs = {0}; /* set instruction pointer where the thread shoud start running */ sel4utils_set_instruction_pointer(&regs, (seL4_Word)thread_2); error=sel4utils_get_instruction_pointer(regs); /* check that stack is aligned correctly */ const int stack_alignment_requirement = sizeof(seL4_Word) * 2; uintptr_t thread_2_stack_top = (uintptr_t)thread_2_stack + sizeof(thread_2_stack); /* set stack pointer for the new thread */ sel4utils_set_stack_pointer(&regs, thread_2_stack_top); error=sel4utils_get_sp(regs); /* actually write the TCB registers. */ error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, &regs); /* start the new thread running */ error = seL4_TCB_Resume(tcb_object.cptr); /* we are done, say hello */ printf("main: hello world \n"); return 0; } And I can get some output: cspace_cap is 2 pd_cap is 3 tcb_object.cptr is 5f7 tcb_object.ut is 10000208 tcb_object.type is 1 tcb_object.size_bits is a regs.pc is 9640 regs.sp is 3f24f0 Any advice about the issue? Thank you, Dongxu Ji

2 2

seL4 and rump kernel synchronization primitives limitations
by Jason Wenger 20 Sep '18

20 Sep '18

I think I've uncovered an interesting problem involving IPC between rump kernels and seL4, and I'm curious if anyone has any thoughts on mitigating it. My use case is that I want a CAmkES component to be able to notify the rump component to send a network packet. However, as far as I can see: CAmkES connector, mutex, and semaphore threads that run in a rump component • can wait on their seL4 synchronization primitives • ... but they can't call rump function calls because they're not rump threads. You can try to call, becuase you're running in the same address space as the rump kernel, but if you call a rumpkernel function, the CAmkES thread crashes when it reaches curlwp() becuase the calling thread is unknown to the NetBSD kernel. Therefore you can't call sendto() inside, for example, a notification callback or an seL4RPCCall handler, unless you can work out a way to signal to the NetBSD kernel that you're calling into the kernel from a foreign thread. Is this somehow possible through use of rump_schedule() and rump_unschedule()? ... and the other possible path I can see also has problems: rumpkernel created userspace threads (pthreads) • can wait on seL4 synchronization primitives • ... but if they do wait, they also unschedule the* entire rest of the rump kernel and userspace* because every single rump thread (both kernel and user) all run in one seL4 thread. Therefore you can't do while(true) { semaphore_wait(); sendto(...); } without unscheduling the entire rump component when you hit the wait(). For this to work, there would need to be a way to have multiple seL4 threads for rump kernel execution so that one could block while the others continue. That *is* done for interrupt and timer handling, but there's no way I can see to set it up from a rump userspace program. The only other possible path appears to be busy-wait polling which is obviously very inefficient. Any thoughts? --Jason C. Wenger

2 1

genode-sel4-arm -- Genode OS with seL4 on ARM hardware
by Adam Wiethuechter 19 Sep '18

19 Sep '18

Webite -- http://genodl4arm.critical.com/ Github -- https://github.com/CriticalTechnologiesInc/genode-sel4-arm Hello everyone, I have something rather exciting to share with you all today that we here at Critical Technologies Inc (CTI) have been working on for sometime now - the marriage of Genode OS and seL4 on native ARM hardware. We currently are supporting the Wandboard Quad (from Wandboard) and the SabreLite (from Boundary Devices). We are hoping to continue development targeting ARMv8a boards of interest; mainly the Raspberry Pi 3B and/or the Xilinx Zynq UltraScale+ ZCU102. This is obviously a work in progress with only the first step but we wished to share our documentation to the community for others to contribute and see what we are doing. I am happy to answer any questions you may have. -- 73's, Adam Wiethuechter, Jr Software Engineer Critical Technologies Inc. <adam.wiethuechter(a)critical.com>

2 1

Building/Running https://github.com/SEL4PROJ/docs with docker
by Axel Heider 18 Sep '18

18 Sep '18

Hi, I'm trying to build and run https://github.com/SEL4PROJ/docs with docker. Following the instrucitons: git clone https://github.com/SEL4PROJ/docs cd docs git submodule init git submodule update docker run --network=host -v $PWD:/host -w /host -it ruby bash -c 'bundle install && bundle exec jekyll serve' things fails with: ... Bundle complete! 8 Gemfile dependencies, 29 gems now installed. Bundled gems are installed into `/usr/local/bundle` Configuration file: /host/_config.yml Source: /host Destination: /host/_site Incremental build: disabled. Enable with --incremental Generating... Liquid Exception: No such file or directory @ rb_sysopen - /host/_repos/sel4/manual/generated_markdown/GeneralSystemCalls.md in ApiDoc.md jekyll 3.6.2 | Error: No such file or directory @ rb_sysopen - /host/_repos/sel4/manual/generated_markdown/GeneralSystemCalls.md Any hint what's failing here? I don't even see a folder "_repo", but I assume the build should create one? Thanks, Axel

2 1

Getting Started
by Dave Richards 14 Sep '18

14 Sep '18

I am in the process of reading the Getting Started documentation and building a development environment on Debian Linux. I thought RefOS would be the best example project to start with. When I execute the command: repo init -u ssh://git@github.com/seL4/refos-manifest -b master I get the response: Please make sure you have the correct access rights and the repository exists. Permission denied (publickey). fatal: Could not read from remote repository. Please make sure you have the correct access rights and the repository exists. fatal: cannot obtain manifest ssh://git@github.com/seL4/refos-manifest Apparently something has changed since the instructions were written. Dave

2 1

Notion of a User in seL4
by Amit Goyal 11 Sep '18

11 Sep '18

Hi All, As far as I understand, in seL4, the notion of a subject is similar to a thread (process). Each process has a different cspace and thus has different capabilities. Correct me, if I am wrong. Currently, we can make different components say server and client which run on the same seL4 kernel. They can interact with each other by creating endpoint and adding capability for that endpoint, in others cspace. Now, I want to extend it and run client and server on different host machines which run seL4. The threads (client and server) thus generated will be different users as per the standard linux convention. a) How does the communication happen in such a scenario in seL4? The problem which I see is how the capabilities for endpoint on one machine will be minted into other machine's process cspace. b) I also want to understand the notion of a user in seL4. -- Thanks and Regards, Amit Goyal

2 1

seL4 - getting the execution time of different threads
by Mr. Peace 11 Sep '18

11 Sep '18

Hello together, I was wondering how you do get the execution time in seL4 if you are using multiple threads. In the initial thread I can use the timer as it is shown in the tutorial about timers since I do have the bootinfo, vka, allocman and so on. But how do I use the timer to measure the execution time of the other threads without stopping their execution to "pull" the time from the initial thread? Is it possible to share the timer or create new ones in the other threads? Or is there another way to measure the execution time? Some background information: The threads have different VSpace's and CSpace's. Used tutorials: seL4-tutorial 4, seL4-tutorial timer. The other threads do not have a bootinfo in their environment. Kind regards, Chris

4 5

Strange behavior when writing to memory mapped to a custom device in the VMM.
by Dan DaCosta 09 Sep '18

09 Sep '18

To Whom It May Concern: I am observing seL4+VM+ARM behavior on the TK1-SOM that I find very puzzling. Consider the following code: #define idx(i) (i%16) for(i = 0; i < buf->capacity() && buf->capacity() > 16; i++, pArray++){ mem[idx(i)] = *pArray; } where 'pArray' is the array representation of 'buf' and 'mem' is a memory mapped page set that corresponds to a page set of memory that is managed by a fault handler in the VMM (something I have installed myself using a 'DEV_CUSTOM' device). This code runs as I would expect. However, the follow code results in an assertion failure in the VMM: #define idx(i) (i%16) for(i = 0; i < 16; i++, pArray++){ mem[idx(i)] = *pArray; } The error report follows: 32 bit ARM insts not decoded -------- Pagefault from [Linux]: write fault @ PC: 0xbd7499a8 IPA: 0xe0001000, FSR: 0x2000046 Context: r0: 0xb6d2a050 r1: 0x0 r2: 0xb6ac76b8 r3: 0x4c r4: 0xb6d2a050 r5: 0xb6d2a8ec r6: 0x1 r7: 0xb6d2a050 r8: 0x7fb73000 r9: 0xad13cfff r10: 0xabe31310 r11: 0x19 r12: 0xb6d285d8 pc: 0x7f68f9a8 r14: 0x7f68f99c sp: 0xaf1c3c20 cpsr: 0x80000010 -------- Assertion failed: rt >= 0 (../projects/seL4_projects_libs/libsel4arm-vmm/src/fault.c: get_rt: 357) Some added information that may be helpful; if the strange modulo operation I am performing on the index is removed I receive a similar crash for both code snippets. Any thoughts on where I might look to get to the bottom of this problem would be helpful. Thanks! Dan DaCosta

2 1

CAmkES VMM platform support
by Grant Jurgensen 07 Sep '18

07 Sep '18

Hi all, I was hoping someone could clarify for me a couple of points regarding the CAmkES VMMs. First off, I have a program I want to run under a linux VM within CAmkES. However, it is written in a language which can be compiled to x86-64 but not IA-32. The impression I have gotten from the documentation and the examples is that the x86 CAmkES VMM only supports the 32-bit variant. Is that correct? My attempt to build the project targeting x86_64 has been met with errors (qemu complains "Huge page not supported by the processor"). Alternatively, said program can be compiled to ARMv6. In fact, the ultimate goal is for this project to run on an Odroid XU4, but as that platform is not currently supported by the CAmkES ARM VMM, I was hoping to build up the infrastructure as much as possible by testing it on any platform I could. The two platforms that are supported for the ARM VMM do not seem to have support on the qemu end though, so unfortunately I have no way of testing there either. Is it fair to assume that porting the Odroid implementation to the Odroid XU4 would be a non-trivial undertaking, or are they perhaps more similar than I am imagining? Thanks, Grant Jurgensen

2 4

issues in running sel4test on RISC-V rocket-chip FPGA
by Tuo Li 06 Sep '18

06 Sep '18

Hi guys, I have ported rocket chip (github.com/ucb-bar/fpga-zynq) on a ZCU102 FPGA board and it successfully runs riscv-linux. It's RV64G RISC-V. I am trying to run sel4test on the same hardware system. So far, the system gives no output after "Jumping to kernel-image entry point..." and seems to be stuck there. The same code has been tested on qemu simulator targeting spike 1.10 with the same device tree, following the online guide ( https://docs.sel4.systems/Hardware/RISCV.html) No problem. I have seen this thread ( http://sel4.systems/pipermail/devel/2018-August/002069.html) and used the solution provided for modifying the paddr range. I tried to add a few printf statements and even a fail statement in the boot.c file in kernel/src/arch/riscv/kernel/, which I guess is the first function executed after head.S. Same problem happens. Any suggestions? Thanks. Best regards, Tuo

2 2

Camkes Build Error
by Amit Goyal 05 Sep '18

05 Sep '18

Hi All, My Camkes has been working fine since now. Suddenly, it stopped working and produce the attached error log on running ninja. I am running it on x86 system (i5 processor), ubuntu 16.04 on qemu: I am running the following commands: mkdir build cd build ../init --plat pc99 --tut hello-camkes-2 --solution ninja Can you please suggest a possible way out? -- Thanks and Regards, Amit Goyal

2 1

Does seL4 support raspberry pi 3B+
by talos 04 Sep '18

04 Sep '18

Hi I saw that seL4 supported raspberry pi 3B, did it support 3B+ now? If it did not, how can I modify it for 3B+? Thanks! Sincerely

2 1

SMC in seL4
by 冀东旭 31 Aug '18

31 Aug '18

Hello, I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone. I initialize the monitor mode directly using the functions "install_monitor_hook()" and “switch_to_mon_mode()”. Is the sp in monitor mode appropriate? After calling smc in SVC mode, it hangs(do nothing in smc_handle()). What's wrong with it? Do you have any ideas? Thank you! Dongxu Ji

2 1

seL4 benchmark configure
by 송대영 31 Aug '18

31 Aug '18

Hi, I want to change seL4 benchmark configuration in ninja build tool. First, I want to change seL4's cache use. Sencond, I want to change CPU core number. How can I change these configuration?

2 1

32 bit vs 64 bit
by Chris Rothrock 31 Aug '18

31 Aug '18

When building the x86 demo for both 32 and 64 bit builds, it looks like the kernel is still a 32 bit elf file regardless of the build and only the sel4test-driver file is what is either 32 bit or 64 bit depending on which is selected. Is this normal or should the kernel also be 64 bit on the 64 bit build? -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637

2 1

Fwd: SMC in seL4
by Dongxu Ji 29 Aug '18

29 Aug '18

Hi Yanyan, 1. It doesn't set the NS bit to 1 in SCR(I just want it to return without do anything). The arm_monitor_vector and the smc_handler(): arm_monitor_vector: ldr pc, [pc, #28] ldr pc, [pc, #24] ldr pc, =smc_handler ldr pc, [pc, #16] ldr pc, [pc, #12] ldr pc, [pc, #8] ldr pc, [pc, #4] ldr pc, [pc, #0] smc_handler: movs pc, lr 2. I didn't do any extra work other than the boot log: .......... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[20000000..203fbfff] ELF-loading image 'kernel' paddr=[10000000..10026fff] vaddr=[e0000000..e0026fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[10027000..10500fff] vaddr=[8000..4e1fff] virt_entry=25a6c Enabling MMU and paging Jumping to kernel-image entry point... 3. The initialization operations in platform_init.c: set sp: #define MONITOR_MODE (0x16) #define MON_VECTOR_START (0x11000000) #define VECTOR_BASE 0x11000000 #define STACK_TOP (VECTOR_BASE + (1 << 12) - 0x10) asm volatile ( "mrs r1, cpsr\n\t" "cps %0\n\t" "isb\n" "mov sp, %1\n\t" "msr cpsr, r1\n\t" ::"I"(MONITOR_MODE),"r"(STACK_TOP)); copy monitor mode vector to MON_VECTOR_START and write into MVBAR: uint32_t size = arm_monitor_vector_end - arm_monitor_vector; printf("Copy monitor mode vector from %x to %x size %x\n", (arm_monitor_vector), MON_VECTOR_START, size); memcpy((void *)MON_VECTOR_START, (void *)(arm_monitor_vector), size); asm volatile ("dmb\n isb\n"); asm volatile ("mcr p15, 0, %0, c12, c0, 1"::"r"(MON_VECTOR_START)); I enter into SVC mode by software interrupt and call the function smc(): asm (".arch_extension sec\n"); asm volatile ("stmfd sp!, {r3-r11, lr}\n\t" "dsb\n" "smc #0\n" "ldmfd sp!, {r3-r11, pc}"); and then the problem arises. Thank you, Dongxu Ji <Yanyan.Shen(a)data61.csiro.au> 于2018年8月28日周二下午8:30写道： > Hi, > > The smc_handle() in monitor.S, it does nothing but "movs pc, lr". > > Does it set the NS bit to 1 in SCR? > > Also, what did you do to ensure that 0x11000000 is not used by the kernel? > > Could you share the code (if possible) so that I could better understand > the problem. > > Regards, > Yanyan > > > ------------------------------ > *From:* Devel <devel-bounces(a)sel4.systems> on behalf of 冀东旭 < > jidongxu1993(a)gmail.com> > *Sent:* Tuesday, August 28, 2018 1:02 PM > *To:* devel(a)sel4.systems > *Subject:* [seL4] SMC in seL4 > > Hello, > > I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone. I initialize the monitor mode by setting the sp to STACK_TOP and copying arm_monitor_vector to MON_VECTOR_START according to the functions "install_monitor_hook()" and "switch_to_mon_mode()" in "platform_init.c". > > #define VECTOR_BASE 0x11000000(addr is not used by the seL4 kernel) > > #define STACK_TOP (VECTOR_BASE + (1 << 12) - 0x10) > > #define MON_VECTOR_START 0x11000000(The VECTOR_BASE is the same as MON_VECTOR_START) > > The smc_handle() in monitor.S, it does nothing but "movs pc, lr". After calling smc in SVC mode, it hangs without any log. If I comment the "smc #0", it can return the caller successfully in usr mode. > > stmfd sp!, {r3-r11, lr} > dsb > smc #0 > ldmfd sp!, {r3-r11, pc} > > Is the sp in monitor mode appropriate? Or I need to do something else in initialization operations? What's wrong with it? Do you have any ideas? > > Thank you! > > Dongxu Ji > >

2 2

SMC in seL4
by 冀东旭 28 Aug '18

28 Aug '18

Hello, I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone. I initialize the monitor mode by setting the sp to STACK_TOP and copying arm_monitor_vector to MON_VECTOR_START according to the functions "install_monitor_hook()" and "switch_to_mon_mode()" in "platform_init.c". #define VECTOR_BASE 0x11000000(addr is not used by the seL4 kernel) #define STACK_TOP (VECTOR_BASE + (1 << 12) - 0x10) #define MON_VECTOR_START 0x11000000(The VECTOR_BASE is the same as MON_VECTOR_START) The smc_handle() in monitor.S, it does nothing but "movs pc, lr". After calling smc in SVC mode, it hangs without any log. If I comment the "smc #0", it can return the caller successfully in usr mode. stmfd sp!, {r3-r11, lr} dsb smc #0 ldmfd sp!, {r3-r11, pc} Is the sp in monitor mode appropriate? Or I need to do something else in initialization operations? What's wrong with it? Do you have any ideas? Thank you! Dongxu Ji

2 1

building sel4test for zynqmp platform
by Leonid Meyerovich 27 Aug '18

27 Aug '18

Hello, I have tried to build sel4test following 'running SEL4' instruction. It was successful for x86 platform, but when I try to build it for 'zyncmp' I've got an error: gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'? gcc: error: unrecognized command line option '-mfloat-abi=soft' Thank you, Leonid -- Build files have been written to: /home/lm/sel4test/build-zynqmp lm@u-18:~/sel4test/build-zynqmp$ ninja [2/235] Generating linker.lds_pp FAILED: elfloader-tool/linker.lds_pp cd /home/lm/sel4test/build-zynqmp/elfloader-tool && /usr/bin/gcc -march=armv8-a -marm -D__KERNEL_32__ -I/home/lm/sel4test/build-zynqmp/autoconf -I/home/lm/sel4test/build-zynqmp/kernel/gen_config -I/home/lm/sel4test/build-zynqmp/elfloader-tool/gen_config -I/home/lm/sel4test/build-zynqmp/libsel4/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4vka/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4utils/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4platsupport/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4serialserver/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4debug/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4test/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4muslcsys/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4vmm/gen_config -I/home/lm/sel4test/build-zynqmp/projects/sel4test/apps/sel4test-driver/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libutils/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libplatsupport/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libethdrivers/gen_config -P -E -o linker.lds_pp -x c /home/lm/sel4test/tools/seL4/elfloader-tool/src/arch-arm/linker.lds gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'? [3/235] Building C object kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj FAILED: kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj ccache /usr/bin/gcc --sysroot=/home/lm/sel4test/build-zynqmp -I../kernel/include -I../kernel/include/32 -I../kernel/include/arch/arm -I../kernel/include/arch/arm/arch/32 -I../kernel/include/plat/zynqmp -I../kernel/include/plat/zynqmp/plat/32 -I../kernel/include/arch/arm/armv/armv8-a -I../kernel/include/arch/arm/armv/armv8-a/32 -Ikernel/gen_config -Ikernel/autoconf -Ikernel/gen_headers -march=armv8-a -marm -D__KERNEL_32__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mfloat-abi=soft -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -E -P -MD -MT kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -MF kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj.d -o kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -c kernel/kernel_bf_gen_target_1_pbf_temp.c gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'? gcc: error: unrecognized command line option '-mfloat-abi=soft' [4/235] Creating C input file for preprocessor ninja: build stopped: subcommand failed. ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

interesting i.MX8 hardware
by Corey Richardson 24 Aug '18

24 Aug '18

https://puri.sm/shop/librem-5/ A seL4 port for that platform might be nice... -- cmr http://octayn.net/ +16038524272

2 2

Re: [seL4] Demo build
by Kent.Mcleod＠data61.csiro.au 23 Aug '18

23 Aug '18

Hi Chris, For your ia32 issue, it appears that you are missing the package libx32gcc-5-dev which provides 32-bit versions of libgcc and libgcc_eh. It is normally installed automatically by gcc-5-multilib. With regards to cpio --reproducible, what version of cpio are you using? The release notes indicate that it was added in version 2.12 (https://www.gnu.org/software/cpio/) but I had it in my Debian package from version 2.11 so I assumed that it was more universally available now. Kent From: Mcleod, Kent (Data61, Kensington NSW) Sent: Thursday, August 23, 2018 11:28 AM To: Chris Rothrock; Lyons, Anna (Data61, Kensington NSW) Cc: devel(a)sel4.systems Subject: Re: [seL4] Demo build Hi Chris, For your ia32 issue, it appears that you are missing the package libx32gcc-5-dev which provides 32-bit versions of libgcc and libgcc_eh. It is normally installed automatically by gcc-5-multilib. With regards to cpio --reproducible, what version of cpio are you using? The release notes indicate that it was added in version 2.12 (https://www.gnu.org/software/cpio/) but I had it in my Debian package from version 2.11 so I assumed that it was more universally available now. Kent From: Devel <devel-bounces(a)sel4.systems> on behalf of Chris Rothrock <cgrothrock(a)gmail.com> Sent: Thursday, August 23, 2018 10:22 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel(a)sel4.systems Subject: Re: [seL4] Demo build I am using a newly initialized build directory for ia32. I can get a good, successful build for v 9.0.0 but not 10.0.0. As for x86_64, I was able to get a good build of x86_64 on 10.0.0 before but now I can't. It seems that there is a switch for cpio that is being set in the build that is invalid for that command. Possibly the latest version of cpio no longer support --reproducable switch since this is where it errors. On Wed, Aug 22, 2018 at 7:33 PM <Anna.Lyons(a)data61.csiro.au> wrote: Hi Chris, For the first issue - just making sure you initialised a new build directory for building ia32? The second issue - our HPET driver is very bare and doesn't support the full gamut of features. If you want to continue with this platform you'll need to improve the driver. Thanks, Anna. From: Chris Rothrock <cgrothrock(a)gmail.com> Sent: Thursday, 23 August 2018 3:56 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel(a)sel4.systems Subject: Re: [seL4] Demo build So my initial problem is actually resolved - it turns out I had the package 'ninja' installed, not 'ninja-build' which threw everything into a fit when I tried to actually use ninja. That being resolved, I was able to get a clean build of the 64 bit kernel (for x86) and made a simulated run. All looked well during the simulation. I do have 2 problems following up from this, however. When trying to use this build for a hardware boot (not simulated boot) I get an error (listed below). Also, for lengthy reasons, I also need to build a 32 bit version but when I do, this build fails. This is the build output from the ia32 build: Desktop:~/sel4test/build-ia32$ ninja [5/32] Linking CXX executable projects/sel4test/apps/sel4test-tests/sel4test-tests FAILED: : && ccache /usr/bin/g++ --sysroot=/home/jennifer/sel4test/build-ia32 -m32 -march=nehalem -D__KERNEL_32__ -nostdinc++ -g -march=nehalem -D__KERNEL_32__ -Wl,-m -Wl,elf_i386 -static -nostdlib -z max-page-size=0x1000 -u __vsyscall_ptr /home/jennifer/sel4test/build-ia32/lib/crt1.o /home/jennifer/sel4test/build-ia32/lib/crti.o /usr/lib/gcc/x86_64-linux-gnu/5/crtbegin.o projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/arch.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/alignment.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/alignment_asm.S.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/breakpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/helpers.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/main.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/benchmark_api.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/binding.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/breakpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cache.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cnodeops.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cspace.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/domains.cxx.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/endpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ept.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/faults.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/fpu.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/frames.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/inc_untyped.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/interrupt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ioports.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/iopt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ipc.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/multicore.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/nbwait.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/pagetables.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/preempt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/regressions.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/schedcontext.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/scheduler.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/serial_server.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/sync.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/threads.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/trivial.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/vspace.c.obj -lgcc -lgcc_eh libsel4/libsel4.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/sel4test/libsel4testsupport/libsel4testsupport.a projects/seL4_libs/libsel4serialserver/libsel4serialserver.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a -lgcc -lgcc_eh libsel4/libsel4.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/sel4test/libsel4testsupport/libsel4testsupport.a projects/seL4_libs/libsel4serialserver/libsel4serialserver.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a /usr/lib/gcc/x86_64-linux-gnu/5/crtend.o /home/jennifer/sel4test/build-ia32/lib/crtn.o -o projects/sel4test/apps/sel4test-tests/sel4test-tests && : /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc.a when searching for -lgcc /usr/bin/ld: cannot find -lgcc /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc_eh.a when searching for -lgcc_eh /usr/bin/ld: cannot find -lgcc_eh /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc.a when searching for -lgcc /usr/bin/ld: cannot find -lgcc /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc_eh.a when searching for -lgcc_eh /usr/bin/ld: cannot find -lgcc_eh collect2: error: ld returned 1 exit status [5/32] Generating from generated/plat_mode/machine/hardware.bf.pbf ninja: build stopped: subcommand failed. Here is the serial output of the x86_64 build boot: Boot config: parsing cmdline '' Boot config: console_port = 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xa11000 end=0xd054f0 size=0x2f44f0 name='' Parsing GRUB physical memory map Physical Memory Region from 0 size 9e800 type 1 Physical Memory Region from 9e800 size 1800 type 2 Physical Memory Region from e0000 size 20000 type 2 Physical Memory Region from 100000 size ac722000 type 1 Adding physical memory region 0x100000-0xac822000 Physical Memory Region from ac822000 size a23000 type 2 Physical Memory Region from ad245000 size 69000 type 3 Physical Memory Region from ad2ae000 size 4b5000 type 4 Physical Memory Region from ad763000 size 430000 type 2 Physical Memory Region from adb93000 size 1000 type 1 Adding physical memory region 0xadb93000-0xadb94000 Physical Memory Region from adb94000 size 206000 type 4 Physical Memory Region from add9a000 size 156000 type 1 Adding physical memory region 0xadd9a000-0xadef0000 Physical Memory Region from adef0000 size 935000 type 2 Physical Memory Region from ae825000 size 4b000 type 1 Adding physical memory region 0xae825000-0xae870000 Physical Memory Region from ae870000 size 781000 type 2 Physical Memory Region from aeff1000 size f000 type 1 Adding physical memory region 0xaeff1000-0xaf000000 Physical Memory Region from e0000000 size 10000000 type 2 Physical Memory Region from feb80000 size 82000 type 2 Physical Memory Region from fec10000 size 1000 type 2 Physical Memory Region from fed00000 size 1000 type 2 Physical Memory Region from fed40000 size 5000 type 2 Physical Memory Region from fed80000 size 10000 type 2 Physical Memory Region from ff000000 size 1000000 type 2 Physical Memory Region from 100000000 size 40000000 type 1 Adding physical memory region 0x100000000-0x140000000 Got VBE info in multiboot. Current video mode is 3 ACPI: RSDP paddr=0xf0490 ACPI: RSDP vaddr=0xf0490 ACPI: RSDT paddr=0xad269028 ACPI: RSDT vaddr=0xad269028 Warning: Your kernel was not compiled for the current microarchitecture. SKIM window for mitigating Meltdown (https://www.meltdownattack.com) not necessary for AMD and performance is being needlessly affected, consider disabling Kernel loaded to: start=0x100000 end=0xa11000 size=0x911000 entry=0x10123e ACPI: RSDT paddr=0xad269028 ACPI: RSDT vaddr=0xad269028 ACPI: FADT paddr=0xad269148 ACPI: FADT vaddr=0xad269148 ACPI: FADT flags=0x385a5 ACPI: MADT paddr=0xad2764a8 ACPI: MADT vaddr=0xad2764a8 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x10 ACPI: MADT_APIC apic_id=0x11 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x12 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x13 ACPI: Not recording this APIC, only support 1 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec01000 gsib=24 ACPI: Not recording this IOAPIC, only support 1 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xf ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: size=0x35b000 v_entry=0x436000 v_start=0x400000 v_end=0x75b000 p_start=0xd06000 p_end=0x1061000 Moving loaded userland images to final location: from=0xd06000 to=0xa11000 size=0x35b000 Starting node #0 with APIC ID 16 Mapping kernel window is done Booting all finished, dropped to user space Received reserved IRQ: 7Skipping table FPDTD, unknown Skipping table FIDT▒, unknown Skipping table TCPA2, unknown Skipping table MSDMU, unknown Skipping table UEFIB, unknown Skipping table IVRSx, unknown Skipping table BGRT8, unknown Skipping table CRAT(, unknown Skipping table LUFT▒), unknown Warning: skipping table ACPI XSDT hpet_init@hpet.c:223 This driver expects hpet timer0 to be 64bit init_timer@main.c:192 [Cond failed: error] Failed to initialise default timer seL4 root server abort()ed Debug halt syscall from user thread 0xffffff80aeff5400 "sel4test-driver" halting... Kernel entry via Unknown syscall, word: 52 On Wed, Aug 15, 2018 at 8:30 PM <Anna.Lyons(a)data61.csiro.au> wrote: Hi Chris, That's strange, the build system definitely should not hang. However I need more information to help at all. Which OS version are you using (host and seL4)? Which gcc version and cmake version? Is there any output from the init-build script at all? Also, have you used a clean build directory after the initial failure? Cheers, Anna. From: Devel <devel-bounces(a)sel4.systems> on behalf of Chris Rothrock <cgrothrock(a)gmail.com> Sent: Thursday, 16 August 2018 3:16 AM To: devel(a)sel4.systems Subject: [seL4] Demo build Most of my experience with the seL5 microkernel has been through the Genode framework, but now I am attempting to build the demo test of seL4 without Genode using the instructions on the "Getting Started" page of seL4.systems but this seems to not be working for me. I have the latest version of repo, ninja and CMake (originally, I was given an error that I needed 3.9.x so I upgraded CMake manually). When I get to the instruction of "../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE" demo build, the script only hangs. Nothing gets built and no demo is run. Is there something missing that I should be doing? Thanks, Chris -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637 -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637 -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637

2 2

Demo build
by Chris Rothrock 23 Aug '18

23 Aug '18

Most of my experience with the seL5 microkernel has been through the Genode framework, but now I am attempting to build the demo test of seL4 without Genode using the instructions on the "Getting Started" page of seL4.systems but this seems to not be working for me. I have the latest version of repo, ninja and CMake (originally, I was given an error that I needed 3.9.x so I upgraded CMake manually). When I get to the instruction of "../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE" demo build, the script only hangs. Nothing gets built and no demo is run. Is there something missing that I should be doing? Thanks, Chris -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637

2 4

formal guarantee about preserving user behaviour
by Abhishek Anand 18 Aug '18

18 Aug '18

I have been reading the following paper for some time: Klein, Gerwin, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. “Comprehensive Formal Verification of an OS Microkernel.” *Trustworthy Sytems*, 2014. https://ts.data61.csiro.au/publications/nictaabstracts/Klein_AEMSKH_14.abst… This is fantastic work and provides powerful guarantees about kernel behavior. However, I am confused about the guarantees about the behavior of user programs. The paper seems to suggest that in the abstract model of sel4, the user transitions are nondeterministic. page 21 bottom: "User transitions are specified as nondeterministically changing arbitrary user-accessible parts of the state space" Does this mean that the refinement theorem of sel4 (Theorem 3 in the above paper: the C implementation refines the abstract model) provides no guarantee about what the user program does, except that the user program does not mess up with the kernel state? Is it fair to say that the refinement theorem does not preclude the sel4 implementation from incorrectly changing the behavior of the user programs, e.g. by messing up the user state? I was expecting the abstract model in Isabelle to concretely specify how the user programs behave, perhaps according to x86/arm/riscv semantics extended with syscalls. Sorry if I misunderstood the paper. Thanks in advance for any clarification, Abhishek -- -- Abhishek http://www.cs.cornell.edu/~aa755/

3 5

Cap fault in send phase while spawning processes
by Noah Kennedy 17 Aug '18

17 Aug '18

Hi folks, I'm currently porting over a project from the Kbuild/Kconfig build system to the new CMake based build system and am having some issues. I'm trying trying to spawn additional processes (2+) and I am encountering an error when I attempt to call 'process_config_default_simple'. The message reads: Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x0 with status 0x4 in thread 0xffffff801ffb5400 "PRIMARY" at address 0x4252ba I loaded the executables which I am trying to spawn into the new processes into the cpio using a variation of the call MakeCPIO(archive.o $<TARGET_FILE:SECONDARY>;$<TARGET_FILE:TERTIARY>;...) where SECONDARY and TERTIARY are the executables which I am using later to spawn the new processes. The source code in question worked previously when using Kbuild, so I'm wondering if I'm doing something wrong with the CMake. Does anyone have any ideas? I've gone through the tutorials, but I'm still fairly new to seL4, so any help would be very much appreciated.

2 2

sel4test driver can not load big elf file
by Dd Nirvana 17 Aug '18

17 Aug '18

Hi guys, When I try to run some application tests(written by myself) on sel4test (x86-qemu environment), I found the following errors. *Starting test suite sel4test* *Starting test 0: Test that there are tests* *Starting test 1: APPTEST1* *vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1* *new_pages_at_vaddr@vspace.c:330 Failed to allocate page number: 0 out of 1* *load_segment@elf.c:103 ERROR: failed to allocate frame by loadee vka: 10* *sel4utils_elf_load_record_regions@elf.c:519 Failed to load segments* *sel4utils_configure_process_custom@process.c:596 Failed to load elf file* It seems seL4test's driver can not load tests with very large size? I also tried to change the "DRIVER_UNTYPED_MEMORY" size from "(1 << 25)" to "(1 << 27)", but it also failed. Any advices about the issue? Dong

2 1

create process in seL4
by Leonid Meyerovich 16 Aug '18

16 Aug '18

Hello, Is there any way to define untyped size while creating process using library functions? process_config_default_simple(simple_t *simple, const char *image_name, uint8_t prio) sel4utils_configure_process_custom(sel4utils_process_t *process, vka_t *vka, vspace_t *spawner_vspace, sel4utils_process_config_t config) The second question is how to initialize allocator (probably I should use bootstrap_use_current_1level, but how where should I get parameters?) in created process to support memory allocation operations? Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 2

Interrupts in SEL4
by Sathya Narayanan N 16 Aug '18

16 Aug '18

Hi Experts, We are trying to port sel4 to Shakti FPGA. It is similar to Rocket FPGA. The memory footprint is 256 mb [0x80000000 - 0x8fffffff]. Shakti support -march=imafd. A single core 64 bit design. The run in FPGA stops at *"memcpy((char *)dest_vaddr + phys_virt_offset, (char *)elf + data_offset, data_size);*" called in the function " *unpack_elf_to_paddr()".* Earlier it stopped just at the memset (one line above). I manually commented out memset part and made it to run till memcpy. So I doubt it has something to do with wrong memory access. can someone please explain me the above said function (blue color) ? what could be reasons for memcpy to hung ? Can someone please guide me to the area in code where memory related interrupts are coded ? We have the latest upstream of SEL4 (Aug 10). It has the dornerworks upstream changes. We are trying to load at 0x88000000. The image works well in spike simulation. *Commands to build:* ../init-build.sh -DPLATFORM=spike -DKernelPlatformSpikeRocketChip=ON -DSIMULATION=FALSE -DRISCV64=TRUE ninja *Snapshot of the run in FPGA:* DTB { #address-cells = <0x00000002>; #size-cells = <0x00000002>; compatible = "shakti,spike-bare-dev"; model = "shakti,spike-bare"; cpus { #address-cells = <0x00000001>; #size-cells = <0x00000000>; timebase-frequency = <0x00989680>; cpu@0 { device_type = "cpu"; reg = <0x00000000>; status = "okay"; compatible = "riscv"; riscv,isa = "rv64imafd"; mmu-type = "riscv,sv39"; clock-frequency = <0x3b9aca00>; interrupt-controller { #interrupt-cells = <0x00000001>; interrupt-controller; compatible = "riscv,cpu-intc"; linux,phandle = <0x00000001>; phandle = <0x00000001>; } } } memory@80000000 { device_type = "memory"; reg = <0x00000000 0x80000000 0x00000000 0x10000000>; } soc { #address-cells = <0x00000002>; #size-cells = <0x00000002>; compatible = "shakti,spike-bare-soc", "simple-bus"; ranges; } uart { compatible = "shakti,uart0"; reg = <0x00000000 0x00011200 0x00000000 0x00001000>; } htif { compatible = "ucb,htif0"; } } ELF-loader started on paddr=[80200000..8060e7d7] elf check file returned 1 elf check file returned 1 ELF-loading image 'kernel' paddr=[88000000..8802bfff] vaddr=[ffffffff80000000..ffffffff8002bfff] virt_entry=ffffffff80000000 configured page table levels = 3...... elf check file returned 1 image size 2b350 *(char *)dest_vaddr + phys_virt_offset = ffffffff88000000 * *phys_virt_offset = 8000000 * *(char *)elf + data_offset, = ffffffff8020f854* *started memcpy* ------------------------------------------------------------> *Hangs* -- regards, Sathya

2 2

seL4 benchmark cache unable.
by 송대영 15 Aug '18

15 Aug '18

Hi, I have question about sel4 benchmark cache unable. I want to benchmark sel4 without cache but I don't know where is the location that configures cache. Would you give advice?

2 1

Questions about sel4bench IPC statistic in the website
by Zihan Yang 14 Aug '18

14 Aug '18

Hi, Your website(https://sel4.systems/About/Performance/home.pml) lists the IPC benchmark result, and I wonder is the x64 result for both fastpath, or both slowpath, or one fastpath and the other slowpath? According to the evaluation of my own on x64 kabylake, the fastpath client->server takes about 600 cycles, and slow path client->serve takes over 1100 cycles. But the website data is 1465 and 780, but it does not show whether it is fastpath or slow path. It looks like that the website data has client->server goes into slowpath(maybe because of lower priority), and the server->client goes into fastpath. Is it so? Thanks, Zihan

2 3

Re: [seL4] Porting SEL4 on RISCV FPGA
by Sathya Narayanan N 13 Aug '18

13 Aug '18

Hi, I am porting SEL4 on RISCV FPGA. I am stuck midway in the kernel elf loader. The function stuck is memcpy. I have added prints and I am not progressing after the last memcpy call in unpack_elf_to_paddr(). All kinds of input appreciated. Function under review: *static void unpack_elf_to_paddr(void *elf, paddr_t dest_paddr)* /* Parse size/length headers. */ dest_vaddr = elf_getProgramHeaderVaddr(elf, i); data_size = elf_getProgramHeaderFileSize(elf, i); data_offset = elf_getProgramHeaderOffset(elf, i); /* Load data into memory. */ * memcpy((char *)dest_vaddr + phys_virt_offset,* * (char *)elf + data_offset, data_size);* * printf("loaded data into memory \n"); -----> Stuck Here !* } } *Can anyone give me a clue on whatsoever to check here ? **It worked perfectly in spike simulation.* *RISCV FPGA configuration* - It supports IMAFD. It has already booted linux. Kernel is loaded at physical address 80 million. *Snap shot* ELF-loader started on paddr=[80200000..8060dc17] elfFile->e_phnum = 1 elfFile->e_phnum = 1 elfFile->e_phnum = 1 elfFile->e_phnum = 1 ELF-loading image 'kernel' paddr=[c0000000..c002dfff] vaddr=[ffffffff80000000..ffffffff8002dfff] virt_entry=ffffffff80000000 elf file is valid image is aligned phy range valiidngetting size of image elfFile->e_phnum = 1 elfFile->e_phnum = 1 memset each segment in the elf file loading each segment in the elf file 2d018 elfFile->e_phnum = 1 loading data into memory char *)dest_vaddr + phys_virt_offset = ffffffffc0000000 (char *)elf + data_offset, = ffffffff8020a694 ----- ? -- regards, Sathya

2 2

Porting SEL4 on RISCV FPGA
by Sathya Narayanan N 13 Aug '18

13 Aug '18

Hi, I am porting SEL4 on RISCV FPGA. I am stuck midway in the kernel elf loader. The function stuck is memcpy. I have added prints and I am not progressing after the last memcpy call in unpack_elf_to_paddr(). All kinds of input appreciated. Function under review: *static void unpack_elf_to_paddr(void *elf, paddr_t dest_paddr)* /* Parse size/length headers. */ dest_vaddr = elf_getProgramHeaderVaddr(elf, i); data_size = elf_getProgramHeaderFileSize(elf, i); data_offset = elf_getProgramHeaderOffset(elf, i); /* Load data into memory. */ * memcpy((char *)dest_vaddr + phys_virt_offset,* * (char *)elf + data_offset, data_size);* * printf("loaded data into memory \n"); -----> Stuck Here !* } } *Can anyone give me a clue on whatsoever to check here ? **It worked perfectly in spike simulation.* *RISCV FPGA configuration* - It supports IMAFD. It has already booted linux. Kernel is loaded at physical address 80 million. -- regards, Sathya

2 1

Paging in SEL4
by Sathya Narayanan N 10 Aug '18

10 Aug '18

Hi Experts, Could some one help me in understanding the paging in SEL4 ? the MMU architecture ? Is there any material to understand ? -- regards, Sathya

4 4

compile error aarch64 platform hikey
by Thad Seeberger 10 Aug '18

10 Aug '18

I really want to target zcu102 but i../init-build.sh -DPLATFORM=zynqmp unsupported platform so I decided to target another A53 target I dont know if this is the proper way to get started on this. ../init-build.sh -DPLATFORM=hikey -DAARCH64=1 ninja [maddthad@localhost build-zcu102]$ ccache /usr/lib64/ccache/aarch64-linux-gnu-gcc --sysroot=/home/maddthad/sel4/sel4test/build-zcu102 -DHAVE_AUTOCONF -I../tools/seL4/elfloader-tool/include -I../tools/seL4/elfloader-tool/include/plat/hikey -I../tools/seL4/elfloader-tool/include/arch-arm -I../tools/seL4/elfloader-tool/include/arch-arm/64 -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv8-a -I../tools/seL4/elfloader-tool/include/arch-arm/armv/armv8-a/64 -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/sel4test/apps/sel4test-driver/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -I../projects/util_libs/libcpio/include -march=armv8-a+crc -D__KERNEL_64__ -D_XOPEN_SOURCE=700 -ffreestanding -Wall -Werror -W -Wextra -mgeneral-regs-only -fpic -fno-pie -MD -MT elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -MF elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj.d -o elfloader-tool/CMakeFiles/elfloader.dir/src/string.c.obj -c ../tools/seL4/elfloader-tool/src/string.c ../tools/seL4/elfloader-tool/src/string.c:97:29: error: expected ‘;’, ‘,’ or ‘)’ before ‘dest’ void *memcpy(void *restrict dest, const void *restrict src, size_t n) gcc ver: COLLECT_GCC=/usr/bin/aarch64-linux-gnu-gcc COLLECT_LTO_WRAPPER=/usr/libexec/gcc/aarch64-linux-gnu/4.8.5/lto-wrapper Target: aarch64-linux-gnu gcc version 4.8.5 20150623 (Red Hat 4.8.5-16) (GCC) thx Thad

3 3

Re: [seL4] Porting SEL4 on RISCV FPGA
by Sathya Narayanan N 09 Aug '18

09 Aug '18

> > Hi, > > I am porting SEL4 on RISCV FPGA. I am stuck midway in the kernel elf > loader. > > The function stuck is memcpy. I have added prints and I am not progressing > after the last memcpy call in unpack_elf_to_paddr(). All kinds of input > appreciated. > > > Function under review: > *static void unpack_elf_to_paddr(void *elf, paddr_t dest_paddr)* > > /* Parse size/length headers. */ > dest_vaddr = elf_getProgramHeaderVaddr(elf, i); > data_size = elf_getProgramHeaderFileSize(elf, i); > data_offset = elf_getProgramHeaderOffset(elf, i); > > /* Load data into memory. */ > > * memcpy((char *)dest_vaddr + phys_virt_offset,* > * (char *)elf + data_offset, data_size);* > * printf("loaded data into memory \n"); -----> Stuck Here > !* > } > > } > > *Can anyone give me a clue on whatsoever to check here ? **It worked > perfectly in spike simulation.* > > *RISCV FPGA configuration* - It supports IMAFD. It has already booted > linux. Kernel is loaded at physical address 80 million. > -- regards, Sathya

1 0

sel4 thread creation problem
by Leonid Meyerovich 08 Aug '18

08 Aug '18

Hello, My platform is ARM (zynqmp), seL4 v8. I have created a timer in simple initial thread: int err; seL4_timer_t timer; vka_object_t ntfn_object; ntfn_object.cptr = 0; err = vka_alloc_notification(&_env.vka, &ntfn_object); assert(err == 0); err = sel4platsupport_init_default_timer(&_env.vka, &_env.vspace, &_env.simple, ntfn_object.cptr, &timer); err = ltimer_set_timeout(&timer.ltimer, NS_IN_MS * 20, TIMEOUT_PERIODIC); assert(err == 0); int count = 0; int count_s = 0; while (1) { /* Handle the timer interrupt */ seL4_Word badge; seL4_Wait(ntfn_object.cptr, &badge); printf("time_thread: badge=%lx\n", badge); sel4platsupport_handle_timer_irq(&timer, badge); count++; if ((count / 50) * 50 == count) { count_s++; printf("-----------------timer=%d %d\n", count, count_s); } } It works fine (I am not sure why TIMESTAMP timer interrupt coming every ~40 sec, but it's not an issue right now) Now I am trying to move all this timer code into a new thread, which I have created in the same vspace // create thread void initSleep(env_t penv) //seL4_BootInfo *info) { _penv = penv; vka_object_t tcb_object = {0}; int error = vka_alloc_tcb(&penv->vka, &tcb_object); seL4_CPtr cspace_cap; cspace_cap = simple_get_cnode(&penv->simple); seL4_CPtr pd_cap; pd_cap = simple_get_pd(&penv->simple); seL4_CPtr ipc_page; seL4_Word ipc_buffer = (seL4_Word)vspace_new_ipc_buffer(&penv->vspace, &ipc_page); error = seL4_TCB_Configure(tcb_object.cptr, , seL4_NilData, cspace_cap, seL4_NilData, pd_cap, seL4_NilData, ipc_buffer, ipc_page); error = seL4_TCB_SetPriority(tcb_object.cptr, simple_get_tcb(&penv->simple), seL4_MaxPrio); seL4_UserContext regs = { .pc = (seL4_Word)time_thread, .sp = (seL4_Word)thread_time_stack }; error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, &regs); error = seL4_TCB_Resume(tcb_object.cptr); } And this is thread function static void time_thread(void) { _tick_number = 0; int count_s = 0; init_timer(); while (1) { /* Handle the timer interrupt */ seL4_Word badge; seL4_Wait(timer_ntfn_object.cptr, &badge); printf("time_thread: badge=%lx\n", badge); sel4platsupport_handle_timer_irq(&timer, badge); _tick_number++; if ((_tick_number / 50) * 50 == _tick_number) { count_s++; printf("-----------------timer=%lu %d\n", _tick_number, count_s); } } The system crashed: setup_irq@timer.c:81 Setting up IRQ 8000000000000000 <<seL4(CPU 0) [handleInvocation/281 T0xff8000001200 "child of: 'rootserver'" @42195c]: Invocation of invalid cap #48762580.>> Here is dump: /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/functions.h:23 421938: d53bd066 mrs x6, tpidrro_el0 setup_irq(): /home/lm/sel4vm/libs/libsel4platsupport/src/timer.c:85 error = seL4_IRQHandler_SetNotification(irq->handler_path.capPtr, irq->badged_ntfn_path.capPtr); 42193c: f85c8340 ldur x0, [x26,#-56] arm_sys_send_recv(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:165 register seL4_Word msg1 asm("x3") = *in_out_mr1; 421940: d2800003 mov x3, #0x0 // #0 seL4_SetCap(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/arch/functions.h:59 421944: f901e8c1 str x1, [x6,#976] arm_sys_send_recv(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:166 register seL4_Word msg2 asm("x4") = *in_out_mr2; 421948: d2800004 mov x4, #0x0 // #0 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:167 register seL4_Word msg3 asm("x5") = *in_out_mr3; 42194c: d2800005 mov x5, #0x0 // #0 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:170 register seL4_Word scno asm("x7") = sys; 421950: 92800007 mov x7, #0xffffffffffffffff // #-1 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:161 register seL4_Word info asm("x1") = info_arg; 421954: d2941001 mov x1, #0xa080 // #41088 421958: f2a00021 movk x1, #0x1, lsl #16 /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:171 asm volatile ( 42195c: d4000002 hvc #0x0 seL4_MessageInfo_get_label(): /home/lm/sel4vm/stage/arm/zynqmp/include/sel4/shared_types_gen.h:49 I suspect that my thread initialization is not right, can somebody see any problem? Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 3

Re: [seL4] camkes-project error
by talos 08 Aug '18

08 Aug '18

Hi I changed it to: ../init-build.sh -DPLATFORM=sabre -DCROSS_COMPILER_PREFIX=arm-none-eabi- -DCAMKES_APP=adder -DSIMULATE=1 -Dc_std=gnu99 and it worked for ninja build. But when started simulation by ./simulate the error is: qemu-system-arm: -kernel images/capdl-loader-image-arm-imx6: unsupported machine type Use -machine help to list supported machines How could I choose the machine type? Thanks! Sincerely

3 2