le 21 avril 2016 à 13:00
L’analyse statique du code C est difficile. Cet exposé explore l’utilisation d’un vérificateur C comme interprète, sacrifiant la solidité mais éliminant l’imprécision due à la sur-approximation. Ce mode d’analyse fonctionne mieux pour les systèmes qui ont des suites de tests très complètes, qu’elles soient construites manuellement ou générées par un outil tel que afl-fuzz. En utilisant Frama-C comme interprète, nous avons analysé des bibliothèques largement utilisées et critiques en termes de sécurité, telles que SQLite, lipng et libwebp, trouvant un certain nombre de problèmes dans chacune d’entre elles et ouvrant la voie à de futurs efforts de vérification solides.
CV : Le professeur Regehr a obtenu son son doctorat en 2001 à l ‘université de Virginie. Il est actuellement professeur d’informatique à l’université de l’Utah, où il enseigne depuis 2003. Ses recherches portent sur les compilateurs, les tests de logiciels et la vérification des logiciels.
Amphithéâtre IRCICA
français
English