Réécriture et Approximation pour la Vérification d'Applications Java – RAVAJ

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 : plus d'automatisation
et plus de flexibilit´e. Ces deux besoins s'expliquent par le fait que la s´ecurit´e s'applique maintenant `a une
tr`es grande quantit´e et tr`es grande vari´et´e de syst`emes ou de logiciels grands publics, eux-mˆemes ´evoluant
rapidement. Pour r´epondre `a cette demande, la mod´elisation formelle doit ˆetre simple, rapide `a mettre en
place et facilement transformable. Pour la v´erification, les preuves doivent ˆetre aussi automatiques que
possibles et facilement adaptables aux transformations du mod`ele.
Parmi les m´ethodes formelles appliqu´ees `a la s´ecurit´e, les syst`emes de r´e´ecriture sont un formalisme simple,
flexible et de plus en plus utilis´e pour la sp´ecification de programmes ou de syst`emes. A titre d'exemple,
on peut trouver des s´emantiques de r´e´ecriture pour diff´erentes versions de la machine virtuelle Java ou
encore des mod`eles de r´e´ecriture pour les protocoles cryptographiques. En revanche, pour effectuer des
v´erifications sur ces mod`eles, les outils classiques de la r´e´ecriture ne sont pas pleinement satisfaisants.
Ceci est dˆu au fait que ces mod`eles de r´e´ecriture ont g´en´eralement un comportement infini (ensemble
infini de donn´ees d'entr´ees ou ensemble infini de chemins d'ex´ecution), ce qui est incompatible avec la
majeure partie des outils de preuve automatique de la r´e´ecriture.
D'autre part, dans le domaine de l'analyse statique, la technique g´en´eralement utilis´ee pour la v´erification
de propri´et´es de s´ecurit´e sur des programmes ayant un comportement infini est celle de l'interpr´etation
abstraite. Grˆace `a cette derni`ere, il est possible de repr´esenter de fa¸con finie (abstraite) un ensemble
infini de donn´ees ou de chemins d'ex´ecution. Cependant, la validit´e de ces preuves repose sur la sˆuret´e
des abstractions, une ´etape de preuve suppl´ementaire, g´en´eralement manuelle, qui doit ˆetre renouvel´ee
pour toute nouvelle abstraction utilis´ee ou tout nouveau mod`ele `a v´erifier.
Le premier objectif de ce projet est de concevoir et de d´evelopper une m´ethode automatique d'analyse
statique certifi´ee pour la preuve de propri´et´es de s´ecurit´e sur des mod`eles de r´e´ecriture. L'approche retenue
repose sur les approximations r´eguli`eres de termes atteignables, qui sont des abstractions particuli`eres
et dont la sˆuret´e est garantie par construction. Le deuxi`eme objectif est d'´etudier le passage `a l'´echelle
et la flexibilit´e de cette technique pour la v´erification de propri´et´es de s´ecurit´e sur des applications Java
multi-tˆaches, de taille r´eelle, destin´ee aux t´el´ephones mobiles.