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 sympa.inria.fr (Postfix) with ESMTPS id E09377F6CB for ; Tue, 27 Jan 2015 21:34:01 +0100 (CET) X-IronPort-AV: E=Sophos;i="5.09,476,1418079600"; d="scan'208";a="118916589" Received: from pat35-4-88-164-243-190.fbx.proxad.net (HELO [192.168.0.1]) ([88.164.243.190]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 27 Jan 2015 21:34:01 +0100 From: =?utf-8?Q?Fr=C3=A9d=C3=A9ric_Besson?= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Message-Id: <041A78B3-18D6-4CB1-AE02-AF0063C20471@inria.fr> Date: Tue, 27 Jan 2015 18:59:01 +0100 To: caml-list@inria.fr Mime-Version: 1.0 (Mac OS X Mail 8.1 \(1993\)) X-Mailer: Apple Mail (2.1993) X-Validation-by: frederic.besson@inria.fr Subject: [Caml-list] Post-Doctoral position for the security of binary code The Inria Celtique group in Rennes has open post-doctoral positions. The po= sitions are funded by the national ANR projects Binsec[1] and Anastasec[2]. Both projects share the o= bjective of improving the security of software, especially at the binary level. - The Anastasec project aims at the formal verification of security propert= ies of large-scale software-intensive embedded systems using static analysis techniques. The p= roject is driven by industrial case studies. One of these case study is a hosting platform whi= ch has to ensure security properties (e.g., task isolation) in the presence of arbitrary bin= ary code (vulnerable and/or malicious). The research will consist in designing static analyses t= echniques to ensure at load-time that a binary code complies with the security requirements of the= hosting platform. - The Binsec project aims at providing tools (grounded on formal methods) f= or the security analysis of binary code. The main application domains are vulnerability analysis an= d virus detection.=20 The research will consist in designing novel static analysis techniques to= compensate for the absence of high-level abstractions and tackle specific challenges of binary code s= uch as auto-modifying code. Positions are for one year (with a possible 1 year extension) and the start= ing date is flexible =E2=80=94 to some extent.=20 Applicants must have a PhD in Computer Science with a strong background in= one of the following fields: formal methods, static analysis, compilers. For further information and applications, potential applicant should contac= t Sandrine Blazy sandrine.blazy@irisa.fr and Fr=C3=A9d=C3=A9ric Besson frederic.besson@inria.fr. The application dea= dline is the 28 February 2015. [1] http://binsec.gforge.inria.fr/ [2] http://www.di.ens.fr/~feret/anastasec/=