Proof-oriented domain-specific language design for high-assurance software
Design de langage dédié orienté vers la preuve pour le logiciel critique
Résumé
Program verification consists in analyzing a computer program as a formal artifact in order to prove the absence of certain categories of bugs before execution. But to use a program verification framework, one has to first translate the original source code of the program to verify in the formal language of the framework. Moreover, one might use different verification frameworks to prove increasingly specialized properties about the program. To answer the need for multiple translations of the source program to various program verification frameworks with different proof paradigms, we advocate for the use of proof-oriented domain-specific languages. These domain-specific languages should act as a frontend to proof backends, with a language design that incorporates and distributes the proof obligations between provers. Moreover, the original program has often already been translated from informal domain-specific requirements that act as its specification. To close the top layer of the chain of trust, we claim that proof-oriented domain-specific language can help domain experts review the program specification at the base of formally verified implementation developments. This dissertation discusses the design and usefulness of proof-oriented domain-specific languages in five case studies. These case studies range from the domain of cryptographic implementations to legal expert systems, and often target real-world high-assurance software. Each of the case study gives its name to a chapter of this dissertation. LibSignal* is a verified implementation of the Signal cryptographic protocol for the Web. Hacspec is a domain-specific language for cryptographic specifications in Rust. Steel is a separation-logic-powered program verification framework for the F* proof assistant. Mlang is a compiler for a tax computation domain-specific language used by the French tax authority. Finally, Catala is a novel language for encoding legislative specifications into executable and analyzable artifacts.
La vérification de programme consiste en l'analyse d'un programme informatique vu comme un artefact formel, afin de prouver l'absence de certaines catégories de bogues avant l’exécution. Mais pour utiliser un cadriciel de vérification de programmes, il faut auparavant traduire le code source originel du programme dans le langage formel du cadriciel. De plus, il est possible d'utiliser plusieurs cadriciels de vérification pour prouver des propriétés de plus en plus spécialisées à propos du programme. Pour répondre au besoin de traductions multiples du programme source vers différents cadriciels de vérification de programmes ayant chacun leur paradigme de preuve, nous défendons l'utilisation de langages dédiés orientés vers la preuve. Ces langages dédiés devraient être pensés comme une sur-couche au-dessus des cadriciels de preuves, avec un design qui incorpore et distribue les obligations de preuves entre les prouveurs. De plus, le programme originel est souvent déjà traduit depuis des spécifications d'exigences informelles liées au domaine d'activité afférent. Afin de raffermir le maillon le plus haut de la chaîne de confiance, nous soutenons que les langages dédiés orientés vers la preuve peuvent aider les experts du domaine à relire la spécification du programme, spécification à la base d'ultérieurs développements d'implantations vérifiées. Cette dissertation traite du design et de l'utilité des langages dédiés orientés vers la preuve au travers de cinq études de cas. Ces études de cas portent sur des domaines allant des implantations cryptographiques aux systèmes experts légaux, et sur des logiciels à haut niveau d'assurance actuellement utilisés en production. Chaque étude de cas donne son nom à l'un des chapitres de cette dissertation. LibSignal* est une implémentation vérifiée du protocole cryptographique Signal à destination du Web. Hacspec est un langage dédié pour les spécifications cryptographiques en Rust. Steel est un cadriciel de vérification de programmes utilisant la logique de séparation à l'intérieur de l'assistant de preuve F*. Mlang est un compilateur pour un langage dédié aux calculs fiscaux utilisé par la DGFiP. Enfin, Catala est un nouveau langage qui permet l'encodage de spécifications législatives dans un code source exécutable et analysable.
Origine : Version validée par le jury (STAR)