(***************************************************************************** * * Secure-OCaml - Checking safety and security properties of OCaml programs * ******************************************************************************) (**************************************************************************** * English (Voir plus bas pour une version française.) ****************************************************************************) Offer: postdoc Publication date: June 23 2015 Workplace: ENSTA-paris, Palaiseau (see http://www.ensta-paris.fr/en/getting-ensta-paris) Duration: from 12 to 24 months Starting: ASAP Salary: from 2200 € to 2400 € net per month (incl. social security) Mission: design and implement libraries for verifying safety and security properties of dynamically loaded OCaml code and data. Description: The Secure-OCaml project aims at adapting the OCaml language to the development of applications involving security issues. The project gathers the following industrial and academic partners: OCamlPro, SafeRiver, LexiFi, TrustInSoft, INRIA, ENSTA-paris, CEA, and Trusted Labs. Among the objectives of the Secure-OCaml project, the safety of dynamically loaded code and data is a particularly important issue. In the same way as static typing ensures safety properties about statically linked code, applications shoould be able to have similar ensurance about dynamically loaded code and data. The postdoc's mission will be to study these problems and bring effective solutions that shall be made freely available to the OCaml community. This work will be realized in cooperation with INRIA-Paris and OCamlpro SAS. Profile sought: - skills in typing and compilation - strong capabilities and taste in functional programming in general and OCaml in particular - a knowledge of the OCaml compiler is an additional advantage Context of the job: ENSTA-paris is a french (top ten) engineering schools, located at Palaiseau, on a campus shared with INRIA and Ecole Polytechnique. The research group "Software Safety and Reliability of Software" is part of ENSTA's Computer Science and System Engineering Department, and aims at improving techniques of development, analysis and verification of software. For more information, contact: - michel.mauny ensta-paris fr - +33 1 8187 2032 To apply, send the following documents to michel.mauny ensta-paris fr: - your resume, with a list of publications - a motivation letter - the name and address (e-mail) of two persons who could write a recommendation Applications will be received as long as the position remains available. Please check at: http://u2is.ensta-paris.fr/members/mauny/ that the position is still available. (**************************************************************************** * Français (See above for an english version.) ****************************************************************************) Type d'offre : post-doctorant Date de publication : 23 juin 2015 Lieu de travail : ENSTA-paris, Palaiseau Durée : de 12 à 24 mois Date de début : dès que possible Salaire : entre 2200 € et 2400 € nets par mois (sécurité sociale incluse) Thèmes : Langages de programmation, compilation, typage, OCaml Mission : concevoir et réaliser des bibliothèques permettant de vérifier des propriétés de sûreté et de sécurité de codes et données chargées dynamiquement par des applications OCaml. Descriptif du poste : Le projet Secure-OCaml (FUI18) a pour objectif d'adapter le langage OCaml au développement d'applications présentant des enjeux de sécurité. Le projet réunit les partenaires industriels et académiques suivants : OCamlPro, SafeRiver, LexiFi, TrustInSoft, INRIA, ENSTA-paris, CEA, et Trusted Labs. Parmi les objectifs du projets Secure-OCaml, la fiabilité du traitement des données et codes chargés dynamiquement est un enjeu particulièrement important : en effet, le typage statique effectué par le compilateur OCaml fournit des garanties fortes aux applications. En revanche, lors du chargement dynamique d'un code ou d'une donnée, une application n'a aucune l'assurance que ce code ou cette donnée est conforme aux hypothèses qu'elle fait. La mission du post-doctorant sera d'étudier ces problèmes et d'y apporter des solutions qui seront rendues librement disponibles sous forme de bibliothèques. Ce travail sera réalisé en étroite coopération avec INRIA-Paris et OCamlpro SAS. Profil recherché : - compétences fortes en typage et compilation - goût affirmé pour le développement OCaml - la connaissance de la chaîne de compilation d'OCaml est un atout supplémentaire Contexte de travail : l'ENSTA-paris est une Grande École d’ingénieurs généraliste, localisée à Palaiseau, sur un campus qu'elle partage avec l'Ëcole Polytechnique. L'équipe « Sûreté et Fiabilité des Logiciels » (http://u2is.ensta-paris.fr/groups/SURF/) de l'Unité d'Informatique et d'Ingénierie des Systèmes » vise à contribuer à l'amélioration des techniques de développement, d'analyse et de vérification des logiciels. Informations complémentaires : - michel.mauny ensta-paris fr - +33 1 8187 2032 Pour candidater, envoyer à michel.mauny ensta-paris fr les documents suivants : - CV avec liste de publications - lettre de motivation - coordonnées de deux personnes en mesure de recommander le candidat Les candidatures seront examinées jusqu'à ce qu'un candidat soit accepté. Merci de vérifier sur http://u2is.ensta-paris.fr/members/mauny/ que l'offre est encore disponible avant de candidater.