Analyse et vérification de programmes
L'analyse et la vérification de programmes emploient des techniques rigoureuses pour raisonner sur le comportement des programmes, détectant les erreurs ou prouvant que les logiciels respectent leurs spécifications.
Definition
L'analyse de programmes est la dérivation automatisée des propriétés du comportement d'un programme sans l'exécuter sur toutes les entrées, et la vérification de programmes est l'établissement, par preuve ou par vérification exhaustive, qu'un programme satisfait une spécification formelle.
Scope
Ce domaine couvre le raisonnement automatisé et semi-automatisé sur les programmes : l'analyse statique et les techniques d'analyse de flux de données, l'interprétation abstraite comme cadre unificateur pour l'approximation sûre (sound approximation), la vérification de modèles (model checking) de systèmes à états finis et concurrents, et la vérification déductive avec des assistants de preuve. Il aborde la sûreté (soundness), le compromis entre précision et décidabilité, et l'utilisation de ces méthodes pour construire des logiciels fiables.
Sub-topics
Core questions
- Comment les propriétés des programmes peuvent-elles être calculées de manière sûre (soundly) malgré l'indécidabilité ?
- Comment les analyses arbitrent-elles entre précision et évolutivité ?
- Quand la correction d'un système peut-elle être vérifiée de manière exhaustive plutôt que testée ?
- Comment les preuves complètes de correction fonctionnelle sont-elles construites et vérifiées par machine ?
Key theories
- Interprétation abstraite
- Cousot et Cousot ont établi un cadre basé sur la théorie des treillis (lattice-theoretic framework) dans lequel les analyses statiques sûres (sound static analyses) sont dérivées comme des approximations de la sémantique d'un programme, unifiant de nombreuses analyses et garantissant leur sûreté (soundness).
- Vérification de modèles par logique temporelle
- Clarke, Emerson et Sistla ont montré comment vérifier automatiquement des systèmes concurrents à états finis par rapport à des spécifications en logique temporelle, en explorant de manière exhaustive l'espace d'états.
- Vérification mécanisée de bout en bout
- Le compilateur vérifié de Leroy démontre que des logiciels réalistes peuvent être prouvés corrects à l'aide d'un assistant de preuve, apportant une garantie vérifiée par machine que la compilation préserve le comportement du programme.
Clinical relevance
L'analyse et la vérification de programmes sont à la base d'outils qui détectent les bogues et les vulnérabilités de sécurité à grande échelle, certifient les logiciels avioniques et automobiles critiques pour la sécurité, et produisent des compilateurs et des noyaux de systèmes d'exploitation vérifiés par machine. Elles transforment la correction, d'une confiance basée sur les tests, en garanties prouvables.
History
L'analyse de flux de données est apparue avec les compilateurs optimisants dans les années 1970, la même décennie où les Cousot ont introduit l'interprétation abstraite. La vérification de modèles (model checking) a émergé au début des années 1980 grâce à Clarke et Emerson, et indépendamment à Queille et Sifakis, leur valant plus tard un prix Turing. Les années 2000 ont été marquées par des succès industriels à grande échelle en analyse statique et en vérification mécanisée, tels que CompCert et seL4.
Debates
- Sûreté (soundness) contre praticité des analyses
- Les développeurs d'outils débattent si les analyses devraient être entièrement sûres (fully sound), signalant toutes les erreurs possibles mais risquant de nombreux faux positifs, ou délibérément non sûres (unsound) pour réduire le bruit et améliorer l'évolutivité, une tension qui façonne les outils industriels de détection de bogues.
Key figures
- Patrick Cousot
- Radhia Cousot
- Edmund Clarke
- E. Allen Emerson
- Xavier Leroy
Related topics
Seminal works
- cousot1977
- clarke1986
- leroy2009
- nielson1999
Frequently asked questions
- Quelle est la différence entre l'analyse statique et la vérification ?
- L'analyse statique infère automatiquement des propriétés approximatives (telles que les déréférencements nuls possibles) sans spécifications complètes, tandis que la vérification prouve qu'un programme satisfait une spécification formelle précise, nécessitant généralement plus d'efforts et offrant des garanties plus solides.
- Si la correction est indécidable, comment l'analyse peut-elle fonctionner ?
- Les analyses contournent l'indécidabilité en calculant des approximations sûres (sound approximations) : elles peuvent signaler certaines possibilités qui ne peuvent pas réellement se produire, mais elles ne manquent jamais une violation réelle de la propriété qu'elles vérifient.