Projets financés

Le projet TACOS propose une approche par composants pour la sp´ecification de syst`emes sˆurs, depuis l'expression des besoins jusqu'`a une sp´ecification formelle, en utilisant ou adaptant des langages et des outils existants. Le domaine d'application choisi est celui du transport ; ce choix r´ep

De nouvelles applications, comme le d´eveloppement de serveurs web, les jeux impliquant un grand nombre de joueurs ou les applications de stockage de donn´ees `a l'´echelle d'Internet sont, de fa¸con inh´erente, massivement parall`eles, et ouvertes `a des acteurs ´eventuellement peu fiables. Ces a

Le tatouage num´erique est l'art de cacher des informations dans des contenus num´eriques d'une mani`ere robuste. Le mot 'cacher' a plusieurs significations. Certains le traduisent par l'imperceptibilit´e de la marque ins´er´ee. D'autres y voient un crit`ere de s´ecurit´e. Cette tendance est appar

Ce projet se situe dans le domaine de la protection de l'information ; les deux themes de recherche concernes sont la cryptographie et calcul symbolique. Nous nous interessons ici essentiellement - mais pas exclusivement - a la cryptographie a clef publique. La cryptographie a clef publique est ba

Le domaine de la s´ecurit´e des syst`emes d'information a connu de profondes mutations r´ecemment, avec d'une part l'apparition d'attaques ayant des cons´equences financi`eres (phishing par exemple) ou techniques (d´eni de service) importantes, et d'autre part l'apparition de nouveaux ´equipements

Dans le domaine de la s´ecurit´e informatique, les m´ethodes de v´erification formelles connaissent un succ`es grandissant et commencent `a infiltrer le monde industriel. De ces nouveaux utilisateurs ´emanent de nouvelles demandes quant aux m´ethodologies de sp´ecification et de v´erification : pl

Le d´eveloppement des r´eseaux informatiques coupl´e `a la convergence rapide des divers types de donn´ees sous la forme num´erique n'est pas sans soulever de nombreuses questions quand `a la s´ecurit´e que l'on peut assurer `a l'information dans ce contexte. Celle-ci repose `a sa base sur l'exist

L'objectif de la d´etection d'intrusions est d'analyser l'activit´e d'un syst`eme d'information afin de d´etecter des actions malveillantes, susceptibles de violer les propri´et´es de confidentialit´e, d'int´egrit´e et de disponibilit ´e des service et des donn´ees. Afin de garantir la compl´etude

Dans le contexte de projets en cours ou pass´es incluant des partenaires industriels de domaines d'application vari´es, les partenaires de FoToVP ont observ´e plusieurs approches pour le d´eveloppement maˆitris´e des syst`emes embarqu´es, bas´ees sur la notion de prototype virtuel. Cela nous a per

Dans les syst`emes informatiques, la confiance est un concept-cl´e garantissant, au-del`a de la fiabilit´e du syst`eme, son utilisation (par des agents humains, mais aussi de plus en plus par des agents artificiels). Ceci est le cas non seulement en ce qui concerne les aspects de s´ecurit´e, mais

La possibilit´e de pannes partielles est une caract´eristique fondamentale des applications informatiques r´eparties. La communaut´e de recherche en tol´erance aux fautes a d´evelopp´e des solutions (algorithmes et architectures), notamment bas´ees sur l'id´ee de r´eplication, appliqu´ees par exem

Les succ`es r´ecents de recherche de collisions dans les fonctions de hachage cryptographiques, ont suscit´e l'´emoi dans la communaut´e des chercheurs en cryptologie. En particulier, aujourd'hui des collisions pour les fonctions MD5 et SHA-0 ont ´et´e obtenues, et des attaques, coˆuteuses mais ac

Le projet DOTS porte sur la sp´ecification formelle et la v´erification automatique des syst`emes informatiques. Plus particuli`erement il s'int´eresse aux syst`emes complexes, comme les fameux syst`emes embarqu ´es, qui int`egrent des aspects temporis´es (des contraintes temps-r´eel), des aspects

L'utilisation généralisée des syst`emes automatis´es dans tous les aspects de nos vies donne une importance incontestable `a la sˆuret´e de leur fonctionnement. La pr´esence de tels syst`emes dans des applications critiques, coupl´ee `a leur complexit´e croissante, rend indispensable leur v´erific

La vérification de programmes est une tˆache difficile qui repr´esente un th`eme de recherche important. L'objectif de ce projet est de fournir des techniques avanc´ees pour la v´erification automatique du logiciel, en prenant compte des aspects complexes de tels syst`emes ´ecrits dans des langage

Le projet RIMEL (Raffinement Incr´emental de Mod`eles ´ev´enementiELs) concerne principalement le raffinement de mod`eles ´ev´enementiels et la syst´ematisation de cette technique dans le cadre d'applications cibl´ees notamment la conception d'algorithmes ou syst`emes r´epartis. La syst´ematisatio

Le projet a pour but de construire une plateforme exp´erimentale pour la validation de circuits `a signaux analogiques et mixtes ; un composent d'importance croissante pour le fonctionnement des syst`emes embarqu ´es modernes. La plateforme combinera deux technologies en cours de d´eveloppement pa

Le projet propos´e consiste : - `a ´etudier et caract´eriser les fonctionnalit´es qu'un environnement integr´e de d´eveloppement (IDE) doit offrir non seulement pour produire des logiciels en conformit´e avec les exigences requises pour atteindre de hauts niveaux de confiance (EAL 5 6 7), mais au