Présentation
du projet
Le thème de recherche central du projet Lande
est la conception d'outils d'aide au développement et à
la validation de logiciels. Notre approche est fondée sur une
collection de méthodes formelles permettant de spécifier
ou d'extraire une vue partielle de l'architecture et du comportement
d'un logiciel. Cette approche nous a amenés à
étudier deux types de problèmes. D'une part, la
spécification d'un logiciel en vues partielles nécessite
une vérification de la cohérence entre plusieurs vues
afin que celles-ci puissent être synthétisées.
D'autre part, l'extraction d'une vue demande des techniques d'analyse
statique et dynamique précises. Nous insistons sur la
nécessité que les réponses apportées
à ces problèmes reposent sur des bases formelles
(sémantique du langage étudié, définitions
de propriétés à vérifier dans des logiques
formelles) afin d'obtenir une garantie sur les résultats
produits. De plus, il est important que les outils construits soient le
plus automatiques possible car les utilisateurs visés ne sont
pas nécessairement des experts en méthodes formelles.
Lande est un projet commun avec le CNRS,
l'Université de Rennes 1 et l'Insa de Rennes.
Axes de
recherche
La description multi-vues de l'architecture de gros
logiciels a comme objectif de spécifier l'organisation globale
de systèmes afin d'améliorer la maîtrise de leur
développement (spécification, analyse, programmation,
test, maintenance, etc.).
Une ambition majeure dans ce domaine est le passage à
l'échelle de techniques comme l'analyse, le raffinement ou la
vérification de programmes. Nos travaux visent à assurer
une forme de cohérence de ces descriptions
hétérogènes. Le défi principal est de
trouver comment mettre en relation des vues qui mettent en jeu des
propriétés de nature très différentes ou
qui se situent à des niveaux d'abstraction différents.
Une fois les vues mises en relation, il devient possible d'utiliser des
techniques standards d'analyse statique ou de vérification afin
d'assurer des propriétés de cohérence.
La nouvelle technique de programmation appelée
" programmation par aspects " consiste à décrire un
logiciel comme un ensemble formé d'un composant principal et
d'une collection de vues ou d'aspects décrivant des tâches
comme la gestion mémoire, la synchronisation, les optimisations,
etc. Un outil, appelé tisseur, est chargé de produire
automatiquement un programme intégrant les différents
aspects au composant principal. L'intérêt de cette
approche est de localiser (dans les aspects) des choix de mise en
oeuvre qui seraient sinon dispersés dans le code source.
Après avoir proposé un aspect dédié
à la sécurisation de code mobile, nous avons
étudié les problèmes d'interactions qui se posent
lorsque l'on doit tisser plusieurs aspects. En effet, comme pour les
vues, les aspects ne sont pas obligatoirement orthogonaux et des
conflits ou ambiguïtés peuvent apparaître lors du
tissage. Nous travaillons également sur un langage d'aspect
dédié à la composition de composants.
Pour faciliter la navigation et l'organisation de
logiciels de taille importante nous cherchons à définir
un cadre logique pour les systèmes d'information qui
décrit uniformément la navigation, l'interrogation et
l'analyse des données. Ce cadre est générique par
rapport à la logique utilisée pour naviguer et interroger
; en particulier il peut être appliqué à plusieurs
types de logiques de programme,
comme les types ou des propriétés statiques. Ces travaux
se basent sur une extension de la théorie de l'analyse de
comcepts.
La validation d'un logiciel utilisent des
méthodes d'analyses et de test de programmes. Nous nous
intéressons à différents aspects de l'analyse
statique de programmes, aussi bien sur le plan des fondements
(spécification d'analyses à partir de règles
d'inférence) que des applications (détection des
pointeurs pendants pour l'aide à la mise au point de programmes
C, analyse de flot de
données et de contrôle dans des programmes Java et Java
Card, analyse de protocoles cryptographiques) et à la mise en
oeuvre d'analyses statiques par des techniques de résolution
itérative de systèmes d'équations et de
réécriture d'automates d'arbres.
Pour faciliter l'analyse dynamique de programmes,
nous développons un outil d'analyse de traces d'exécution
permettant à l'utilisateur d'exprimer des requêtes dans un
langage de programmation logique. Ces requêtes peuvent être
traitées à la volée, ce qui permet d'analyser des
traces de grande taille. L'outil peut être utilisé pour le
débogage de programmes séquentiels et nous
étudions maintenant son application au problème de la
détection d'intrusion.
En collaboration avec la société AQL
nous poursuivons le développement de l'outil Casting dont le
noyau utilise une méthode de génération de suites
de tests. L'outil peut prendre des entrées dans des formats
variés et produit des suites de tests selon des
stratégies spécifiées par l'utilisateur. Nous
adaptons actuellement Casting pour la génération de
suites de test à partir de spécifications
UML.
La sécurité logicielle constitue un
domaine d'application privilégié pour le projet. Nous
élaborons un cadre pour la définition de
propriétés de sécurité et une technique
pour leur vérification automatique. Cette technique
intègre des techniques d'analyses statiques et de
vérification de modèle ("model checking"). Ce cadre a
été appliqué à la formalisation et la
vérification de politiques de sécurité
d'applications programmées avec la nouvelle architecutre de
sécurité de Java 2 et à la vérification de
propriétés de sécurité des cartes à
puce multi-applicatives programmées avec le langage Java Card.
