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
Résumé
As software is an essential component of many embedded systems or online information systems, its malfunction can cause harm or security vulnerabilities. New bugs and vulnerabilities keep being discovered in existing software; many of those bugs and vulnerabilities are caused by violations of memory safety. In particular, low-level code, written in languages that offer few safety guarantees, is the most prone to this kind of bug. However, writing low-level code is sometimes necessary for performance or direct access to hardware features. Formal methods can be used to verify the safety of low-level programs, but automated analysis techniques to verify memory-related properties, such as shape analyses, still require important human effort, preventing wide adoption. In this thesis, we propose a practical automated analysis based on types that express structural invariants on memory down to the byte level. This analysis, which we formalize in the framework of abstract interpretation, offers a trade-off between precise, flow-sensitive shape analyses and scalable, flow-insensitive pointer analyses. It can be applied to low-level code with only a small amount of manual annotations. We show how the type-based abstraction can be complemented with retained and staged points-to predicates to handle precisely common low-level code patterns, such as data structure initialization. We demonstrate the effectiveness and practicality of the analysis by verifying the preservation of structural invariants (implying spatial memory safety) on C and machine code programs, showing that it can be helpful in eliminating an entire class of security vulnerabilities. We then apply our analysis to executables of embedded kernels and show that our typebased invariants allow to verify absence of runtime errors and absence of privilege escalation. To do this, we introduce the concept of implicit properties, i.e. properties which can be defined without reference to a specific program, and therefore lend themselves well to automated verification; and we prove that absence of privilege escalation is an implicit property. Parameterized verification, i.e. verification of the kernel independently from applicative code and data, poses many challenges, such as the need to summarize memory, or the dependence on a complex precondition on the initial state. We propose a methodology to solve them using our analysis technique. We apply this methodology to verify absence of runtime errors and absence of privilege escalation on a full, unmodified embedded kernel with a high level of automation.
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.
Origine : Version validée par le jury (STAR)