Vérification automatique de code bas-niveau : C, assembleur et binaire

Formal methods for software development have made great strides in the last twodecades, to the point that their application in safety-critical embedded software isan undeniable success. Their extension to non-critical software is one of the notableforthcoming challenges. For example, C programmers regularly use GNU style inlineassembly for low-level optimizations and system primitives. This usually results inrendering state-of-the-art formal analyzers developed for C ineffective. This is parti-culary problematic since inline assembly is notoriously hard to write correctly∶ notonly the assembly chunk may contain some errors, but there is a risk of a mismatchat the interface between C and assembly, leading to subtle and hard-to-find bugs.We propose to address the problem of verifying C programs containing inline assem-bly. We thus designed two techniques, named RUSTInA and TInA, based on anoriginal formalization of inline assembly together with novel dedicated algorithms.RUSTInA is the first automated technique for formally checking inline assemblyinteface compliance (i.e. no mismatch between code and interface), with the extraability to propose (proven) patches and code refinements (optimization) in certaincases. TInA is the first automated, generic, verification-friendly and trustworthylifting technique turning inline assembly into semantically equivalent C code ame-nable to verification, in order to take advantage of existing C analyzers. Extensiveexperiments on real-world code (all assembly chunks found on the Debian Jessiepackages) raised 986 significant issues in 54 packages, including 156 issues in 7 pa-ckages that were succesfully repported to and addressed by the developpers thanksto our automatic patch generation method, and show the feasibility of our principledassembly-to-C lifting and its benefits for state-of-the-art C analyzers.Les méthodes formelles pour le développement logiciel ont fait de grands progrès au cours des deux dernières décennies, au point que leur application dans les logiciels embarqués critiques pour la sûreté est un succès indéniable. Leur application aux logiciels non critiques est cependant l’un des défis majeurs à venir. Par exemple, les programmeurs C utilisent régulièrement l’assembleur embarqué (inline assembly)GNU pour réaliser des optimisations de bas niveau ou accéder aux primitives du système. Cela a généralement pour conséquence de rendre inopérants les analyseurs formels de pointe développés pour C. Ceci est doublement problématique puisque l’assembleur embarqué est notoirement difficile à écrire correctement : non seulement le morceau d’assembleur peut contenir des erreurs, mais il y a également un risque d’incompatibilité à l’interface entre C et assembleur, ce qui peut entraîner des bugs subtils et difficiles à trouver. Nous proposons d’attaquer le problème de la vérification de programmes C contenant de l’assembleur embarqué. Nous avons donc conçu deux techniques, nommées RUSTInA et TInA, basées sur une formalisation originale de l’assembleur embarqué, ainsi que de nouveaux algorithmes dédiés. RUSTInA est la première technique automatisée pour la vérification formelle de la conformité de l’interface de l’assembleur embarqué (c’est-à-dire l’absence d’incompatibilité entre le code et l’interface), avec la capacité supplémentaire de proposer des correctifs (prouvés) et des raffinements de code (optimisation). TInA est la première technique de traduction automatique, générique, adaptée aux outils de vérification formelle et digne de confiance qui transforme l’assembleur embarqué en code C sémantiquement équivalent, afin de tirer parti des analyseurs C existants. Des expériences intensives sur du code réel (tous les morceaux d’assembleur embarqué trouvés dans les paquets de Debian Jessie) ont permis de remonter 986 problèmes significatifs dans 54 paquets,dont 156 problèmes de 7 paquets qui ont été signalés avec succès et traités par les développeurs grâce à notre génération automatique de correctifs. Ces expériences montrent également la faisabilité de notre traduction « orientée pour la vérification »et ces avantages pour les analyseurs C de l’état de l’art