Verified Programming at the Intersection of Dependent Types and Static Analysis
Programmation vérifiée à l'intersection des types dépendants et de l'analyse statique
Résumé
Dependently-typed languages allow for a new paradigm: proof-oriented or type-driven programming, consisting in writing a program, its specifications and proofs simultaneously. This yields the greatest quality of software, at the cost of manual proof effort. Conversely, static analysis methods aim at inferring properties by analyzing existing programs –usually written without proofs in mind.This Ph.D. thesis studies how advanced type systems and static analysis methods can work cooperatively. As for the latter, we focus primarily on a theory of sound approximation: abstract interpretation. Our first contribution demonstrates the effectiveness of proof-oriented programming (with the F* language) for writing verified sound abstract interpreters. Such interpreters exist but understanding them requires expertise in both proof-engineering and abstract interpretation. Our approach yields an order of magnitude less explicit proofs, leading to a very concise and accessible implementation. We then study how abstract interpretation andweakest-precondition (WP) monads could be hybridized, aiming at better type inference for F*. Our approach consists in turning abstract interpreters into WP monad transformers.We finally look at the benefits of F* dependent types and effects for Information Control Flow (IFC). We present the design and implementation of a library allowing any combination of static and dynamic IFC verification.
La programmation dirigée par les types ou orientée preuves consiste à écrire et prouver des programmes simultanément. Elle émerge grâce aux langages équipés de types dépendants, et permet une formidable qualité logicielle, au prix de temps passé à écrire des preuves. Inversement, l’analyse statique vise à inférer des propriétés en analysant des programmes existants.Cette thèse étudie la façon dont les systèmes avancés de typage et l’analyse statique peuvent coopérer. Quant à l’analyse statique, nous nous focalisons principalement sur une théorie correcte d’approximation de programmes : l’interprétation abstraite. Notre première contribution démontre l’efficacité de la programmation orientée preuves (avec le langage F*) pour écrire des interpréteurs abstraits formellement vérifiés. De tels interpréteurs existent, mais requièrent une expertise avec les assistants de preuves et en interprétation abstraite, les rendant particulièrement inaccessibles. Notre approche ne nécessite que très peu de preuves manuelles (un ordre de magnitude inférieur en comparaison avec les travaux similaires) : notre implémentation est particulièrement concise et accessible. Nous avons ensuite étudié l’hybridation d’interpréteurs abstraits et de monades de pré-condition la plus faible (WP). Notre approche instrumente des interpréteurs abstraits en des transformeurs de monades de WP. Enfin, nous avons travaillé sur les bénéfices des types dépendants et du système d’effets de F* pour le contrôle de flux d’information (IFC). Nous présentons une librairie permettant de vérifier des politiques d’IFC de manière flexible, entre statique et dynamique.
Origine : Version validée par le jury (STAR)