From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id 77F0D2DF6 for ; Mon, 11 Mar 2019 20:24:58 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.58,468,1544482800"; d="scan'208";a="372906455" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 11 Mar 2019 21:24:57 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 313CE8264A; Mon, 11 Mar 2019 21:24:57 +0100 (CET) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id BB1F082581; Mon, 11 Mar 2019 21:24:45 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=david.nowak@univ-lille.fr; spf=Pass smtp.mailfrom=david.nowak@univ-lille.fr; spf=None smtp.helo=postmaster@mx1.univ-lille.fr IronPort-PHdr: =?us-ascii?q?9a23=3A4SknyRT2OohmAKr6VpuwRfn3GNpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa67ZhSBt8tkgFKBZ4jH8fUM07OQ7/m4HzRZqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRo?= =?us-ascii?q?LerpBIHSk9631+ev8JHPfglEnjWwba5uIBmssQndq9QdjJd/JKo21hbHuGZDdf?= =?us-ascii?q?5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXM?= =?us-ascii?q?TRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmij?= =?us-ascii?q?oINyQh/W/XlsN+g61Urg+vqRxx3YDbYoKbOv1lc6PBZNMaQHZNXsZNWyFDBI63?= =?us-ascii?q?cosBD/AGPeZdt4TzqUEBrQW/BQaxGejh0jhIh3Hs0q05zu8sFhzJ0xY+H9IPrX?= =?us-ascii?q?vYttP1NKAcUO+vz6nF1ijDb/VX2Tfj8YTIdhEhofWIXb1ua8bRx1MvGhrDg16N?= =?us-ascii?q?p4LlODaV2f4Ms2id9+dvS/igi3Unqg5tojig3MYsipPTioIS0FDE+j11wJszJd?= =?us-ascii?q?25Vk53eNqkEJpUtyGeKYR6WM0iQ3twtCYh1rIGuIC0fC4Wx5s53B7Qd/uHc46G?= =?us-ascii?q?4h75U+aROzh4iXR4c7y8nxa/6VWsx+nzW8WuzlpHriVInsPRunwT0xHf8MaKR/?= =?us-ascii?q?Vl8ku8xTqC0xrf5vxALEwoj6bXNZEszqIqmpccvknOGDL9ll/sg6+MbEok//Cl?= =?us-ascii?q?6+T5bbXioZ+RL4p0iw7jPqg0h8y/B+U4MhYXU2if+OS80Lnj8lPjTLVElP06iq?= =?us-ascii?q?jZsJbEKsQHvqO1HgtY34k55xqhDzqr384UkWQZIF9BYh6KgYbkN0nLIP/iDPe/?= =?us-ascii?q?h1qskC1sx/DDJrDuH4/CLmbCkLj8Z7p97UlcyQQpwtBc/J9UF7cBIPPtWkPosN?= =?us-ascii?q?zYDxs5MwiqzOr9BtV9zJsSWXiTDa+BLKPSrViI6/ozLOaWYY8VvC/xK/wk5/71?= =?us-ascii?q?kX80gkQdfKms3ZsPcn+0BPVmI0ODYXrtmNgNC2kKvhAmRuzwlFKCSSJTZ2q1X6?= =?us-ascii?q?8k+j47D5umAZ7fSYCpnbyOxzy2HoZWZ2BDElCDC23kd4SCW/cWaSKdONVtkjIe?= =?us-ascii?q?Vevpd4h0zRC28QT+1rBPM+zV5GgctJbn2Z57/ambnB4+/BRwDt+ByCeGT2hwm2?= =?us-ascii?q?4SXHkt0eQ3qEd5kH+ezax5mOBDU8FP6uNASUE3OYOYh+dzDtS3XgPaYv+ITkyn?= =?us-ascii?q?S5OoG3V5Usg4xcQAZFx4M9GjlQzOxGyrDaQJi7WRQpIuturY2HfwLIN4z17I07?= =?us-ascii?q?JnjEQnWY1MJGq6getisQHYQYzR1w2bjL2xaeEExCrl+mCYi2mTvVoeUx93TaKA?= =?us-ascii?q?QDYWbQ3UtZCxrF/TV7K1TL0hNAxcz8WPAq9LccHyy05LTeylJczTZWT3lmutT1?= =?us-ascii?q?7c2qKUYZGvcmMb2zjbA0UstyEowU3ADiUXPWGcm0/4KnpDOW+5Jwvn9vA7o3em?= =?us-ascii?q?RGc1yRuLZgtvzf799RIPwOeRQO4J364J/ikmsShxNFen3snfTdSa9CR7e6AJTd?= =?us-ascii?q?oj4VsP82XGvg81apCpMaFuwFgZbA10l17o1gsyDoRElcVsoml8n1k6Er6RzF4U?= =?us-ascii?q?L2DQ5pv3ILCCcjCjriDqULbf3xTl6PjT/64O7PoirFC64VO0EEs8tnFm191YlX?= =?us-ascii?q?WGtMyTUFgiFKnpW0NyzCBU4qnAa3BgtZ7S1GMpNaiwtjKE1ch7XLJ4mCblRM9W?= =?us-ascii?q?Nea/LCG3E8AeAJH/euk6wh60aBMaeeRT8Ko5ec28JaOL?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0D4BAC0w4ZchyGB/sJkDggGAQEBBAEBB?= =?us-ascii?q?wQBAYFlgngDgQAnhAqTToMJmSUNI4FUgnUChDoaBwEENBIBAQMBAQcBAwEBARM?= =?us-ascii?q?BAQEKCwkIKSMMgjoigm8DAx0GHQEBJgoCBg8dCAImAgJJDgYBEoMiAYF5C694c?= =?us-ascii?q?YEvgngBAQWBBAGGMAiBCySLLYFXP4ERJx+CFweBb4FdBBiBIIMxMYImiiMmmVs?= =?us-ascii?q?HAoEfgSMEhQuLVIsCiDiDPIc8hWWJdIMWgV6BdzMaJ3YBgkEJNYFMGAKFEoNWh?= =?us-ascii?q?QQEOD4BMgGNcgIkB4IgAQE?= X-IPAS-Result: =?us-ascii?q?A0D4BAC0w4ZchyGB/sJkDggGAQEBBAEBBwQBAYFlgngDgQA?= =?us-ascii?q?nhAqTToMJmSUNI4FUgnUChDoaBwEENBIBAQMBAQcBAwEBARMBAQEKCwkIKSMMg?= =?us-ascii?q?joigm8DAx0GHQEBJgoCBg8dCAImAgJJDgYBEoMiAYF5C694cYEvgngBAQWBBAG?= =?us-ascii?q?GMAiBCySLLYFXP4ERJx+CFweBb4FdBBiBIIMxMYImiiMmmVsHAoEfgSMEhQuLV?= =?us-ascii?q?IsCiDiDPIc8hWWJdIMWgV6BdzMaJ3YBgkEJNYFMGAKFEoNWhQQEOD4BMgGNcgI?= =?us-ascii?q?kB4IgAQE?= X-IronPort-AV: E=Sophos;i="5.58,468,1544482800"; d="scan'208";a="372906365" X-MGA-submission: =?us-ascii?q?MDG5dOc79Q131a1PdZVdddNYtXZ97WiArH5CV7?= =?us-ascii?q?Ml0BNHNuHWrWMS2fwOqTqzCb9NYE+NId39cWZlowLW5DOIdUr7TSHpXx?= =?us-ascii?q?l+IILf1u8gvgPxG+Af9iyqxPbDU9FqOGZT4YKzGZwlLP7WCDfatAsFTL?= =?us-ascii?q?bLV1/21U4IUjjikuQxtOSHaw=3D=3D?= Received: from mx1.univ-lille.fr ([194.254.129.33]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 11 Mar 2019 21:24:39 +0100 Received: from smtp1.univ-lille.fr (smtp1.univ-lille.fr [10.140.10.72]) by mx1.univ-lille.fr (LA PUISSANCE) with ESMTP id 33C3947858; Mon, 11 Mar 2019 21:24:35 +0100 (CET) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=univ-lille.fr; s=dkim; t=1552335876; bh=YiNI2fMssg5CeKPc++1cycY3zuIiGdvlDgjqykNEJtI=; h=From:Subject:Date:References:To:In-Reply-To:From; b=aSrqKMXTw8OZPkfuROhDRo0egFMKWwf6t6JgphGQ9+cnXOjFf1UmrYWXYtUbNEe74 GT5U0/awIzFQqHr4k9gm4TRhqU06EpoPVbsrvoeUN42Ui6WVh4oPRXtPBnxBGleqxg lvVZ76vOVZkRj9kpOF9+RcdGE2SwxDYm4ymXYF24= Received: from [192.168.1.80] (44-240-190-109.dsl.ovh.fr [109.190.240.44]) (Authenticated sender: david.nowak@univ-lille.fr) by smtp1.univ-lille.fr (Postfix) with ESMTPSA id 525FF2014B; Mon, 11 Mar 2019 21:24:35 +0100 (CET) From: David Nowak Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 12.2 \(3445.102.3\)) Date: Mon, 11 Mar 2019 21:24:34 +0100 References: <2364ECC8-852C-4A07-AA9C-ED08CB1B17E7@univ-lille.fr> To: pip-club@univ-lille.fr, agda@lists.chalmers.se, acl2@utlists.utexas.edu, caml-list@inria.fr, transform@listes.ifsttar.fr, logic-ml@fos.kuis.kyoto-u.ac.jp, jssst-ppl@fos.kuis.kyoto-u.ac.jp, "types-announce@lists.seas.upenn.edu" , coq-club@inria.fr, gdr-securite.forum@irisa.fr In-Reply-To: <2364ECC8-852C-4A07-AA9C-ED08CB1B17E7@univ-lille.fr> Message-Id: X-Mailer: Apple Mail (2.3445.102.3) X-UDL-MailScanner-Information: Please contact the ISP for more information X-UDL-MailScanner-ID: 33C3947858.A9C76 X-UDL-MailScanner: Found to be clean X-UDL-MailScanner-SpamCheck: n'est pas un polluriel, SpamAssassin (not cached, score=-2.999, requis 6, autolearn=not spam, ALL_TRUSTED -1.00, BAYES_00 -1.90, DKIM_SIGNED 0.10, DKIM_VALID -0.10, DKIM_VALID_AU -0.10, URIBL_BLOCKED 0.00) X-UDL-MailScanner-From: david.nowak@univ-lille.fr Subject: [Caml-list] ENTROPY 2019: Deadline Extension -- Final Call for Papers Reply-To: David Nowak X-Loop: caml-list@inria.fr X-Sequence: 17402 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: The deadline for ENTROPY 2019 is extended to March 15, 2019. You can submit via our Easychair website: https://easychair.org/conferences/?conf=3Dentropy2019 Questions can be directed to: entropy2019@sciencesconf.org = **************************************************************************= Final Call for papers =E2=80=94 ENTROPY 2019 ENabling TRust through Os Proofs =E2=80=A6 and beYond Second International workshop on the use of theorem provers for = modelling=20 and verification at the hardware-software interface=20 https://entropy2019.sciencesconf.org 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 15, 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=20= this software runs on, is critical for application security. In contrast=20= with user applications, OS kernel software runs in privileged CPU mode=20= and is thus highly critical. Large projects such as seL4, VeriSoft,=20 CertiKoS and Prosper have invested considerable resources in developing=20= formally verified systems such as hypervisors and microkernels, = supplying=20 proofs that they satisfy critical properties. Such proofs are delicate = in=20 terms of the scale and complexity of real systems, the models used in=20 performing the proof search, and the relations between the two, which=20 recent vulnerabilities such as Spectre and Meltdown have shown to be a=20= highly non-trivial issue. The purpose of this workshop is to share, compare and disseminate best=20= practices, tools and methodologies to verify OS kernels, also setting = the=20 stage for future steps in the direction of fully verified systems,=20 dealing with issues related to modelling, model validation, and large=20 proof maintenance through system evolution. On one hand, we need to make=20= low-level proofs more scalable, modular and cost-effective. On the other=20= hand, once certified systems are available, preservation and maintenance=20= of their proofs of validity become key questions. The goal of the ENTROPY workshop is to provide a forum for researchers=20= and practitioners in this space, linking operating systems, formal=20 methods, and hardware architecture, interested in system design as well=20= as machine verified mathematical proofs using proof assistants such as=20= Coq, Isabelle and HOL4. This will be the second edition of the ENTROPY workshop series. The=20 first workshop was organised by the Pip Development Team at University=20= 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=20= of ideas, so position papers, work-in-progress and industrial=20 experience submissions are welcome. SUBMISSION AND PUBLICATION There are two categories of submissions: 1. Regular papers describing fully developed work and complete results=20= (10 pages, references included, IEEE format) 2. Short papers, position papers, industry experience reports, work-in-progress submissions (4 pages, references included, IEEE=20 format) All papers should be in English and describe original work that has not=20= been published or submitted elsewhere. The submission category should=20 be clearly indicated. All submissions will be fully reviewed by members=20= of the Programme Committee. Papers will appear in IEEE Xplore in a=20 companion volume to the regular EuroS&P proceedings. For formatting and=20= 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=C3=BAblica, 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 --=20 David Nowak http://www.cristal.univ-lille.fr/~nowakd/