ANALYSE STATIQUE PAR INTERPRÉTATION ABSTRAITE
par Charles  HYMANS (EADS France), Xavier  ALLAMIGEON (EADS)
Résumé
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.
Biographie
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.
Biographie
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.

Icon  Name                                                                 Size  
[PARENTDIR] Parent Directory - [   ] SSTIC07-article-Allamigeon_Hymans-Heap_Overflow_Analyse_Statique.pdf 359K [   ] SSTIC07-Allamigeon_Hymans-Heap_Overflow_Analyse_Statique.pdf 588K