Registration
The primary aim of the session is to give an opportunity to students and academics and non-academic researchers to hear about recent developments of this kind carried out in an industry context. Talks will be in French.
April 28 at Institut Henri Poincaré.
People interested in participating should register here for logistic reasons. Notice that the inscription for this day is separate from other workshops!
Dominique Bolignano ( Prove & Run)
Méthodes formelles et sécurité mobile
Compte tenu du nombre sans cesse croissant de téléphones mobiles et tablettes en circulation et de la multiplication de leurs usages, la sécurité mobile est en train de devenir un enjeu majeur pour la protection des utilisateurs et des fournisseurs de service. De nouvelles architectures ont été identifiées pour y faire face. Mais elles butent toutes sur le problème de réduction du nombre de bogues exploitables par des attaques de sécurité. Ces bogues se trouvent dans l’implémentation, dans la conception ou dans la configuration de la base de confiance qui comprend au minimum le noyau du système mais peut aussi inclure certaines applications.
Les méthodes formelles sont les seules techniques qui pourraient véritablement permettre de répondre à cette problématique. Mais malgré l’énorme effort de recherche et les résultats obtenus ces dernières décennies dans ce domaine, leur utilisation est restée relativement marginale, a fortiori dans le domaine de la sécurité mobile.
Prove & Run développe un outillage et une approche de méthode formelle et se propose de les rendre applicables à des problèmes à fort enjeu comme celui de la sécurité mobile.
Dans cet exposé nous décrirons nos objectifs, en termes d’outils et méthodologies, et la manière dont nous pensons pouvoir les appliquer dans un premier temps au problème de la sécurité mobile.
Philippe Bonnard et Georges Uzbelger ( IBM )
Des règles métier pour la gestion de l'incertain
Les systèmes de gestion de règles métier (Business Rules) ont été largement développés et utilisés depuis 15 ans par le monde de l'industrie (banque, assurance, transport…), dont notamment le système ODM (Operational Decision Manager) développé par IBM. Une règle métier permet de définir une prise de décision ou une stratégie élémentaire de l'entreprise de manière simple et accessible aux non-informaticiens. Cependant, les systèmes actuels gèrent difficilement les informations incomplètes ou incohérentes. Pour répondre à cette problématique, le projet d'étude “Uncertain Reasoning for Business RuleS”, commencé au sein du Lab France d'IBM en collaboration avec le LIP6, proposent d'étendre le système ODM sur des modèles de connaissance probabilistes en utilisant l'inférence bayésienne. Nous développerons tous ces points lors de notre exposé.
Jean-Louis Colaço ( Esterel-Technologies)
SCADE: un langage formel pour l'embarqué critique
L'environnement de développement SCADE permet de construire des spécifications exécutables pour des applications temps réel critique. Il s'appuie pour cela un langage synchrone aussi appelé SCADE, historiquement dérivé de Lustre et intégrant depuis sa version 6 des machines à état hiérarchiques ainsi que des structures de contrôle inspirés des Syncharts (notation graphique pour Esterel).
Son générateur de code certifié autorise la production de code (compilation vers du C) sans vérification que celui-ci est bien conforme à la spécification SCADE dont il est issu.
Nous donnerons dans cet exposé quelques éléments de la formalisation de la sémantique statique de SCADE 6 et des propriétés qui en découlent. Enfin, Nous montrerons comment il est possible de vérifier formellement des propriétés de sûreté sur des logiciels développés en SCADE.
Alain Frish ( LexiFi)
LexiFi: Approche “langage” pour la description de contrats financiers
LexiFi est un éditeur de logiciel spécialisé dans le domaine de la finance et des produits structurés. L'originalité de LexiFi est de combiner des méthodes innovantes issues des mathématiques financières et de la théorie des langages de programmation. En particulier, LexiFi a développé un langage de description des contrats financiers, permettant de traiter de manière générique, via des techniques “langages” (analyse, réécriture, compilation), la grande diversité des produits traités. L'exposé présentera ce domaine et la contribution de LexiFi, ainsi que l'utilisation par LexiFi du langage OCaml pour ses développements applicatifs.
Emmanuel Ledinot ( Dassault Aviation) - Keynote
Analyse de valeur ² : regard sur 25 ans de méthodes formelles dans le secteur aéronautique
En dépit de succès indéniables dans quelques secteurs industriels, de la progression de quelques PME en pointe et d'une recherche de qualité tout particulièrement en France, la diffusion des méthodes formelles dans l'industrie ne semble pas en rapport avec la dynamique de croissance des secteurs d'activité auxquels elles sont destinées, et ce en dépit d'un durcissement des cadres réglementaires. En s'appuyant sur le cas du secteur aéronautique et sur un retour d'expérience de 25 ans de “success” et de “failure” stories dans le transfert de méthodes formelles de la recherche vers des équipes opérationnelles de développement de logiciel embarqué, on tentera de dégager quelques facteurs à l'origine de cet échec relatif, ou de ce succès mitigé.
On considèrera l'utilisation des méthodes formelles sous le double point de vue du développement des logiciels embarqués critiques et de la qualification d'outils d'ingénierie, et on s'efforcera de dégager quelques orientations prospectives sur ce que pourrait être un positionnement des méthodes formelles plus favorable à leur diffusion.
Olivier Levillain ( ANSSI)
Langages de développement et sécurité — Mind your language
Il existe de nombreux langages informatiques, et les débats concernant leurs avantages et inconvénients respectifs sont nombreux, mais peu considèrent la question du développement d'applications sécurisées, c'est-à-dire robustes contre les actions d'agents malveillants. C'est l'optique abordée dans cette présentation, qui rebondit sur quelques illustrations dans différents langages afin de pouvoir cerner ce que seraient les bonnes propriétés d'un langage vis-à-vis de la sécurité, mais aussi des recommandations de codage pertinentes ou encore des outils pertinents pour le développement et l'évaluation d'applications de sécurité.
Benjamin Monate ( TrustInSoft)
TrustInSoft : des méthodes formelles pour donner confiance dans les composants logiciels existants