En finir avec les faux positifs grâce à l’exécution symbolique robuste

Benjamin Farinier (1) , Sébastien Bardin (1) , Richard Bonichon (1) , Marie-Laure Potet (2)

1 DILS (CEA, LIST) - Département Ingénierie Logiciels et Systèmes
2 VERIMAG - IMAG - VERIMAG

L’exécution symbolique est une technique de vérification formelle par sous-approximation ayant fait ses preuves en recherche de bogues, notamment grâce à son absence de faux positifs : un bogue trouvé est un bogue réel. Cependant, si cette propriété est vraie dans le cas où l’utilisateur contrôle toutes les entrées du programme, les choses se compliquent quand certaines entrées sont hors de son contrôle, typiquement l’environnement. L’exécution symbolique devient alors fragile dans le sens où elle peut produire des faux positifs. Ce cas se rencontre particulièrement en recherche de vulnérabilités, où les failles cherchées doivent être reproductibles. Dans cet article nous montrons comment l’utilisation de quantificateurs permet de passer du problème de l’accessibilité à celui de l’accessibilité robuste et proposons une modélisation cohérente en tant que sous-approximation. Ces quantificateurs sont ensuite éliminés et les formules obtenues simplifiées afin de limiter au maximum l’impact sur le temps de résolution. Il en résulte ainsi une analyse par exécution symbolique efficace et robuste vis-à-vis de son environnement, réellement exempte de faux positifs

Domaines: Informatique; Cryptographie et sécurité [cs.CR]; Langage de programmation [cs.PL]

Benjamin Farinier, Sébastien Bardin, Richard Bonichon, Marie-Laure Potet. En finir avec les faux positifs grâce à l’exécution symbolique robuste. JFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France. pp.245-252. ⟨cea-04484565⟩