- 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