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 084175D5 for ; Tue, 21 May 2019 14:50:05 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.60,495,1549926000"; d="scan'208";a="384118848" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 21 May 2019 16:49:59 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 81755826DB; Tue, 21 May 2019 16:49:59 +0200 (CEST) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 22E798249C; Tue, 21 May 2019 16:49:57 +0200 (CEST) Authentication-Results: mail3-smtp-sop.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=3An7QDwBYKbncnxyB/Kb17PLr/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZps67Zh7h7PlgxGXEQZ/co6odzbaP6ua5ADRLsc/JmUtBWaQEbwUCh8?= =?us-ascii?q?QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6?= =?us-ascii?q?OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MQi6oR/MusULnYduJaU8xgbUqXZUZu?= =?us-ascii?q?pawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnF?= =?us-ascii?q?VguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hC?= =?us-ascii?q?oBKjU09nzchM5tg6JBuB+vpwBwzYHbb4+bKfRwfb3Tc9QBSGpdR8ZRUjBNAoOg?= =?us-ascii?q?Y4YNCecKIOZWr5P6p1sLtRawCxOjBP3uyjBVm3T4xao60uo7HgHFwQctGM8Bv2?= =?us-ascii?q?7KrNX0KageS+a1zK7GzDrZbPNbwir96I7JchA/uP2MWbNwcc7VyUYxDQ/FgE+Q?= =?us-ascii?q?pJXjMjiI2OoNtG2b4PBhVeKpk2MnsB1+ojmxyccqlobGmJkVxUzD9SV/zoY5P9?= =?us-ascii?q?q4SFR0YdOiDZBetDmaOpNrTs4mTGxkojg2x70JtJKhYSQG1pAqywTRZvGJa4SE?= =?us-ascii?q?/xzuWemLLTtmmH5oeaiziwiy/ES61+HxVs+520tQoCVfiNnDrHUN2gTT6seZTv?= =?us-ascii?q?t9+V+s2TOA1gzO8O1EPEY0lavFK5I4xr4wl54TsUDdESPslkX2lreadkQi+ue2?= =?us-ascii?q?9+Tqeqjqq5uTOoNulA3zMqsjltaiDegmNgUCRWaW9Oqk2L3m50L5QbFKjvMskq?= =?us-ascii?q?netZDXPdkUqbSnAw9Uz4kv8RC/DzCo0dsCnnkKN09FeBSGj4j3Il3OJPH4DfO7?= =?us-ascii?q?g1uyijtryerGMqX7AprRNnjDjKvhfbFl5kFA0gUzyNRf64tQCrEAO/LzRlT8tM?= =?us-ascii?q?fYDx88Kwy72fzrCNR71oMEWGKAGLWVMK3IsVWQ/OIgP/GMZJMJuDb6M/Uq+/nu?= =?us-ascii?q?jWYglVABeampwIAYZWujHvVmJkWZeWDjjs0AEWcMpAo+TfblhEeMUT5Jf3yyRb?= =?us-ascii?q?4z5iknCIK6CofOXpqtgKGa3CemBZBXZ2FGClWXHnfybYqIQfYMaCSIIs9giDMI?= =?us-ascii?q?T7ahS5VynS2p4Rf70/9sKvfe0jAetIym0Nlx4+CVmwt2vTV7A82112CWU3oylW?= =?us-ascii?q?MBQzo7xrs5ukE5gl6I1fJQnuBcFMdP/LVUTgoqPIWawuBnT5j5UwfFO9OIU0qO?= =?us-ascii?q?Q9O8ADh3QMh1i8MUakBmFdK4izjH3jG2DqRTlrKQGIA96OTSxTy5I8Fyyn2D0a?= =?us-ascii?q?0JgV49BMhSNHbghb946w+WGsjAmAObj+Lid78HxzKI7H+H5WSJpwdbTQ9rF6bU?= =?us-ascii?q?WmwYI1aQpN+/5FuGB/WyGKwqKU5Iz8iFN61BZ/XtjE5aX7H4Nd3FJX+plmG2Qx?= =?us-ascii?q?uE2/nEOJb7Y2gGmSzbDk8ZlQse1VKnDjQFQByMilmYMQRDM3SpTm/Rp602o3Si?= =?us-ascii?q?C0Qw0guibkt71rPz9ARRzfOQUbYI07kZoiY9pnN6G0yg2vrXEdubrkxvZvZye9?= =?us-ascii?q?Q4tXtOy2PV/yp6IZWjZ/Ruj0Aff0JxuFzn1D1qDIRe1MwrqHcnigRof/HLmGhd?= =?us-ascii?q?fi+ViMijcobcLXP/qUj2Nvzmn2rG2dPTwZ8hrfQ1r1K67VOsBhNk7nNmzZxR0n?= =?us-ascii?q?+Y69PEFlhKCMOjYgMM7xF/4oriTGw47oLQ22drNPDp4CLE2sxsAOohzhvmcc0N?= =?us-ascii?q?afrYRj+3KNUTAo2VEMJvg0KgN09WIeZT6uswPseier2IwvzzMQ=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BuAwAkD+RchyGB/sJlDoUDUjIohBOTC?= =?us-ascii?q?oF7AZphCQEDAQwfDgIBAYFLhR0bBwEENBMBAwEBBAEBAgEBAwETAQEBCgsJCCk?= =?us-ascii?q?jDII6IoMSBh0BATg0AiYCXwGDNAGCCgQLpgFxgS+CeQEBBYEGAYFBgyeBPQMGg?= =?us-ascii?q?Qwoi1GBVz+BOB4Bgh5sgQSGSjKCJqgnBwKBK2RYBIVSjG2WLIN9iFmSTYMjgWa?= =?us-ascii?q?BeDMaJ3YBgkE+gWkChRODVoUEBDk9ATKBCI4pAQE?= X-IPAS-Result: =?us-ascii?q?A0BuAwAkD+RchyGB/sJlDoUDUjIohBOTCoF7AZphCQEDAQw?= =?us-ascii?q?fDgIBAYFLhR0bBwEENBMBAwEBBAEBAgEBAwETAQEBCgsJCCkjDII6IoMSBh0BA?= =?us-ascii?q?Tg0AiYCXwGDNAGCCgQLpgFxgS+CeQEBBYEGAYFBgyeBPQMGgQwoi1GBVz+BOB4?= =?us-ascii?q?Bgh5sgQSGSjKCJqgnBwKBK2RYBIVSjG2WLIN9iFmSTYMjgWaBeDMaJ3YBgkE+g?= =?us-ascii?q?WkChRODVoUEBDk9ATKBCI4pAQE?= X-IronPort-AV: E=Sophos;i="5.60,495,1549926000"; d="scan'208";a="306755569" X-MGA-submission: =?us-ascii?q?MDGmfdP/XiF5hHZpdEalK9Vc2Nlmb8wnXhRIK0?= =?us-ascii?q?aua8WG0GEZZ6xJiGNBxx/cmnylJvhoEpav3CEKbi+fsz3HGaiirZ7BGm?= =?us-ascii?q?P/1ZXTzsEoL5z9chWqrygL3bjFb+0g6J89imV4CcHfaBBQc3P/Rao0Bi?= =?us-ascii?q?wU4z613DfaNXrsAputIitlLA=3D=3D?= Received: from mx1.univ-lille.fr ([194.254.129.33]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 21 May 2019 16:49:56 +0200 Received: from smtp1.univ-lille.fr (smtp1.univ-lille.fr [10.140.10.72]) by mx1.univ-lille.fr (LA PUISSANCE) with ESMTP id 6DB44494C6; Tue, 21 May 2019 16:49:53 +0200 (CEST) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=univ-lille.fr; s=dkim; t=1558450193; bh=jCdAJl1OT6+ngRc3LbhWzaIjx/13c+FK4g2PPaAzMd0=; h=From:Date:Subject:To:From; b=krHCKGTRb6qj0qgZM3A8QSH0kik/YO5lGupfUC0RA6i1nsTYxj01nZK2Um6sTgpl4 g81aUZ73P648wP1IqejeHU/76iEvfAO6QS/P8/+ta2WDHpJ+b+tQY2w46HraOgdhQw 2sTnjM+Tb0j+qvq3Xq/hO3Wm6VqyXQTdR2Plwn0g= Received: from upper.lifl.fr (upper.lifl.fr [134.206.25.15]) (Authenticated sender: david.nowak@univ-lille.fr) by smtp1.univ-lille.fr (Postfix) with ESMTPSA id 08DDE21235; Tue, 21 May 2019 16:49:53 +0200 (CEST) From: David Nowak Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 12.4 \(3445.104.8\)) Date: Tue, 21 May 2019 16:49:52 +0200 Message-Id: <03CCAC24-6CA5-4F67-B580-B15F4CC1C577@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 X-Mailer: Apple Mail (2.3445.104.8) X-UDL-MailScanner-Information: Please contact the ISP for more information X-UDL-MailScanner-ID: 6DB44494C6.A8F86 X-UDL-MailScanner: Found to be clean X-UDL-MailScanner-SpamCheck: n'est pas un polluriel, SpamAssassin (not cached, score=-0.3, requis 7, autolearn=not spam, ALL_TRUSTED -1.00, BAYES_50 0.80, DKIM_SIGNED 0.10, DKIM_VALID -0.10, DKIM_VALID_AU -0.10) X-UDL-MailScanner-From: david.nowak@univ-lille.fr Subject: [Caml-list] ENTROPY 2019: Call for Participation - Co-located with EuroS&P'19 Reply-To: David Nowak X-Loop: caml-list@inria.fr X-Sequence: 17562 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: *************************************************************** Call for participation =E2=80=94 ENTROPY 2019 ENabling TRust through Os Proofs =E2=80=A6 and beYond 16 June 2019 Second International workshop on the use of theorem provers for modelling and verification at the hardware-software interface=20 https://entropy2019.sciencesconf.org Co-located with EuroS&P'19, KTH, Stockholm, June 2019 *************************************************************** PROGRAM HIGHLIGHTS Formal Proof of a Secure OS Full Trusted Computing Base by Dominique Bolignano, Prove & Run Time protection: principled prevention of timing channels by Gernot Heiser, University of New South Wales Proving the security of interrupt handling against interrupt-based = side-channel attacks: a case study by Frank Piessens, KU Leuven Nailing Down the Architectural Abstraction by Peter Sewell, University of Cambridge