Automated verification of systems code using type-based memory abstractions

Vérification automatisée de code système à l'aide d'abstractions mémoire basées sur le typage Les logiciels étant des composants essentiels de nombreux systèmes embarqués et de nombreux systèmes d'information, un dysfonctionnement logiciel peut entraîner d'importants dommages ou des failles de sécurité. De nouveaux bugs et de nouvelles vulnérabilités sont trouvés régulièrement dans les programmes existants; une grande partie d'entre eux est causeé par des violations de la sûreté mémoire. En particulier, le code bas niveau, écrit dans des langages de programmation qui offrent peu de garanties de sûreté, est le plus susceptible de contenir ce type de bug. Malgré cela, écrire dans un langage bas niveau reste parfois nécessaire pour des raisons de performance, ou pour accéder directement aux fonctionnalités du matériel. Les méthodes formelles peuvent permettre de vérifier la sûreté des programmes bas niveau, mais les techniques automatisées de vérification de propriétés mémoire, telles que les analyses de forme, nécessitent encore un effort manuel important, ce qui est un obstacle à une adoption large. Dans cette thèse, nous proposons une analyse automatisée facilement applicable, basée sur un système de types exprimant des invariants structurels sur la mémoire, précis jusqu'au niveau de l'octet. Cette analyse, que nous formalisons dans le cadre de l'interprétation abstraite, offre un compromis entre les analyses de forme, précises et sensibles au flot de contrôle, et les analyses de pointeurs, qui sont insensibles au flot de contrôle, mais passent très bien à l'échelle. Elle peut être appliquée à du code bas niveau avec peu d'annotations manuelles. Nous montrons comment cette analyse basée sur les types peut être complémentée par des prédicats de pointeurs conservés et reportés, afin de supporter précisément des motifs fréquents en code bas niveau tels que l'initialisation de structures de données. Nous démontrons l'efficacité et l'applicabilité de l'analyse en vérifiant la conservation d'invariants structurels (qui impliquent la sûreté mémoire spatiale) sur des programmes C et du code machine, montrant qu'elle peut être utile pour éliminer toute une classe de failles de sécurité. Nous appliquons ensuite notre analyse à des exécutables de noyaux embarqués, et nous montrons que nos invariants à base de types permettent de vérifier l'absence d'erreurs à l'exécution et l'absence d'escalade de privilèges. Pour cela, nous introduisons le concept de propriété implicite, c'est-à-dire de propriété qui peut être définie sans référence à un programme en particulier, qui se prêtent bien à la vérification automatique ; et nous montrons que l'absence d'escalade de privilèges est une propriété implicite. La vérification paramétrée, c'est-à-dire la vérification de noyaux indépendamment du code et des données des applications, comporte plusieurs défis, comme le besoin de résumer la mémoire ou bien la dépendance à une précondition complexe sur l'état initial. Nous proposons une méthodologie pour les résoudre à l'aide de notre technique d'analyse. À l'aide de cette méthodologie, nous vérifions l'absence d'erreurs à l'exécution et l'absence d'escalade de privilèges sur un noyau entier sans modification, avec un haut niveau d'automatisation.