De nombreuses failles de sécurité sont rendues possibles par la présence de bogues dans les logiciels. Le buffer overflow est l'exemple typique de bogue qui permet la prise de contrôle d'une machine. Concevoir des logiciels de la taille et complexité actuelles, et exempts d'erreurs, relève de l'utopie. Nous présentons l'analyse statique par interprétation abstraite : sans exécuter le logiciel, par inspection de code uniquement, elle permet d'assurer l'absence de bogues d'une certaine catégorie (tel que les buffer overflows). Nous détaillons la méthodologie de conception de tels analyseurs, les difficultés, et les compromis réalisés. Nous donnons des exemples d'analyseurs conçus sur ce principe et les résultats auxquels ils parviennent.

Charles Hymans, chercheur au centre de recherche d'EADS, travaille sur la vérification automatique de programmes pour l'embarqué. Il a effectué sa thèse sur la vérification formelle de descriptions matérielles.

Xavier Allamigeon réalise une thèse au centre de recherche d'EADS en collaboration avec le CEA sur la vérification de manipulations de mémoire dans les logiciels.

 Name                                                                 Size  
 Parent Directory                                                       -   
 SSTIC07-Allamigeon_Hymans-Heap_Overflow_Analyse_Statique.pdf         588K  
 SSTIC07-article-Allamigeon_Hymans-Heap_Overflow_Analyse_Statique.pdf 359K