Les analyses de sécurité au niveau binaire (par exemple, l’analyse des vulnérabilités, rétro-ingénierie des logiciels malveillants, etc.) sont des tâches importantes mais complexes. D’où le besoin de techniques et d’outils capables d’en automatiser une partie. Par ailleurs, comme l’analyse de programmes au niveau du code source et les méthodes formelles pour les applications critiques ont fait d’énormes progrès au cours des dernières décennies, il est extrêmement tentant de les adapter pour passer d’analyses de sûreté niveau source à des analyses de sécurité niveau binaire.
Dans cet exposé, nous présenterons d’abord les avantages et les défis des méthodes formelles et de l’analyse de programme pour les scénarios de sécurité au niveau du code binaire, puis nous esquisserons un panorama des résultats et des réalisations obtenus jusqu’à présent dans ces directions par le groupe BINSEC du CEA LIST. En particulier, nous montrerons comment des techniques telles que l’exécution symbolique et la résolution de contraintes peuvent être adaptées à un certain nombre de scénarios pratiques de sécurité au niveau binaire (tels que la recherche de vulnérabilités, la vérification formelle au niveau binaire de primitives cryptographiques, la rétro-ingénierie et la désobfuscation), et nous discuterons des dernières avancées de l’outil BINSEC.
Cette session sera animée par le Dr. Sébastien Bardin, Fellow du CEA, Responsable de l’équipe LSL/SABR
