SPARK (langage de programmation) - SPARK (programming language)
Paradigme | Multi-paradigme |
---|---|
Développeur | Altran et AdaCore |
Version stable | Communauté 2021 / 1er juin 2021
|
Discipline de frappe | statique , fort , sûr , nominatif |
Système d'exploitation | Multiplateforme : Linux , Microsoft Windows , Mac OS X |
Licence | GPLv3 |
Site Internet | À propos de SPARK |
Les principales mises en œuvre | |
SPARK Pro, SPARK Édition GPL, Communauté SPARK | |
Influencé par | |
Ada , Eiffel |
SPARK est un langage de programmation informatique formellement défini basé sur le langage de programmation Ada , destiné au développement de logiciels à haute intégrité utilisés dans des systèmes où un fonctionnement prévisible et hautement fiable est essentiel. Il facilite le développement d'applications qui exigent la sûreté, la sécurité ou l'intégrité de l'entreprise.
À l'origine, il existait trois versions du langage SPARK (SPARK83, SPARK95, SPARK2005) basées respectivement sur Ada 83, Ada 95 et Ada 2005.
Une quatrième version du langage SPARK, SPARK 2014, basée sur Ada 2012, a été publiée le 30 avril 2014. SPARK 2014 est une refonte complète du langage et des outils de vérification associés.
Le langage SPARK consiste en un sous-ensemble bien défini du langage Ada qui utilise des contrats pour décrire la spécification des composants sous une forme adaptée à la fois à la vérification statique et dynamique.
Dans SPARK83/95/2005, les contrats sont encodés dans des commentaires Ada et sont donc ignorés par tout compilateur Ada standard, mais sont traités par le "Examiner" SPARK et ses outils associés.
SPARK 2014, en revanche, utilise la syntaxe "aspect" intégrée d'Ada 2012 pour exprimer les contrats, les amenant au cœur du langage. L'outil principal de SPARK 2014 (GNATprove) est basé sur l' infrastructure GNAT/GCC et réutilise la quasi-totalité du front-end GNAT Ada 2012.
Aperçu technique
SPARK utilise les forces d'Ada tout en essayant d'éliminer toutes ses ambiguïtés potentielles et ses constructions non sécurisées. Les programmes SPARK sont conçus pour être sans ambiguïté et leur comportement ne doit pas être affecté par le choix du compilateur Ada . Ces objectifs sont atteints en partie en omettant certaines des fonctionnalités les plus problématiques d'Ada (telles que les tâches parallèles illimitées ) et en partie en introduisant des contrats qui codent les intentions et les exigences du concepteur de l'application pour certains composants d'un programme.
La combinaison de ces approches permet à SPARK d'atteindre ses objectifs de conception, qui sont :
- solidité logique
- définition formelle rigoureuse
- sémantique simple
- Sécurité
- pouvoir expressif
- vérifiabilité
- besoins limités en ressources (espace et temps).
- exigences minimales du système d'exécution
Exemples de contrats
Considérez la spécification du sous-programme Ada ci-dessous :
procedure Increment (X : in out Counter_Type);
En Ada pur, cela peut incrémenter la variable X
de un ou de mille ; ou il peut définir un compteur global X
et renvoyer la valeur d'origine du compteur dans X
; ou il pourrait ne rien faire X
du tout.
Avec SPARK 2014, des contrats sont ajoutés au code pour fournir des informations supplémentaires sur ce que fait réellement un sous-programme. Par exemple, nous pouvons modifier la spécification ci-dessus pour dire :
procedure Increment (X : in out Counter_Type) with Global => null, Depends => (X => X);
Ceci précise que la Increment
procédure n'utilise (ni ne met à jour ni ne lit) aucune variable globale et que la seule donnée utilisée dans le calcul de la nouvelle valeur de X
est X
elle - même.
Alternativement, le concepteur peut spécifier :
procedure Increment (X : in out Counter_Type) with Global => (In_Out => Count), Depends => (Count => (Count, X), X => null);
Cela spécifie qui Increment
utilisera la variable globale Count
dans le même package que Increment
, que la valeur exportée de Count
dépend des valeurs importées de Count
et X
, et que la valeur exportée de X
ne dépend d'aucune variable et qu'elle sera dérivée de données constantes uniquement .
Si GNATprove est ensuite exécuté sur la spécification et le corps correspondant d'un sous-programme, il analysera le corps du sous-programme pour construire un modèle du flux d'informations. Ce modèle est ensuite comparé à celui qui a été spécifié par les annotations et les écarts éventuels signalés à l'utilisateur.
Ces spécifications peuvent être encore étendues en affirmant diverses propriétés qui doivent soit être conservées lorsqu'un sous-programme est appelé ( préconditions ) soit être conservées une fois l'exécution du sous-programme terminée ( postconditions ). Par exemple, nous pourrions dire ce qui suit :
procedure Increment (X : in out Counter_Type) with Global => null, Depends => (X => X), Pre => X < Counter_Type'Last, Post => X = X'Old + 1;
Ceci, maintenant, spécifie non seulement qui X
est dérivé de lui seul, mais aussi que before Increment
est appelé X
doit être strictement inférieur à la dernière valeur possible de son type et qu'après X
sera égal à la valeur initiale de X
plus un.
Conditions de vérification
GNATprove peut également générer un ensemble de conditions de vérification ou de VC. Ces conditions sont utilisées pour établir si certaines propriétés sont valables pour un sous-programme donné. Au minimum, le GNATprove générera des VC pour établir que toutes les erreurs d'exécution ne peuvent pas se produire dans un sous-programme, telles que :
- index de tableau hors limites
- violation de plage de type
- division par zéro
- débordement numérique.
Si une postcondition ou toute autre assertion est ajoutée à un sous-programme, GNATprove générera également des VC qui exigent que l'utilisateur montre que ces propriétés sont valables pour tous les chemins possibles à travers le sous-programme.
Sous le capot, GNATprove utilise le langage intermédiaire Why3 et le générateur de VC, ainsi que les prouveurs de théorème CVC4, Z3 et Alt-Ergo pour décharger les VC. L'utilisation d'autres prouveurs (y compris des vérificateurs de preuves interactifs) est également possible via d'autres composants de l'ensemble d'outils Why3.
Histoire
La première version de SPARK (basée sur Ada 83) a été produite à l' Université de Southampton (avec le parrainage du ministère britannique de la Défense ) par Bernard Carré et Trevor Jennings. Le nom SPARK est dérivé de SPADE Ada Kernel , en référence au sous-ensemble SPADE du langage de programmation Pascal .
Par la suite, le langage a été progressivement étendu et affiné, d'abord par Program Validation Limited, puis par Praxis Critical Systems Limited. En 2004, Praxis Critical Systems Limited a changé son nom pour Praxis High Integrity Systems Limited. En janvier 2010, la société devient Altran Praxis .
Au début de 2009, Praxis a formé un partenariat avec AdaCore et a publié "SPARK Pro" sous les termes de la GPL. Cela a été suivi en juin 2009 par la SPARK GPL Edition 2009, destinée aux FOSS et aux communautés académiques.
En juin 2010, Altran-Praxis a annoncé que le langage de programmation SPARK serait utilisé dans le logiciel du projet américain lunaire CubeSat , qui devrait être achevé en 2015.
En janvier 2013, Altran-Praxis change de nom pour devenir Altran.
La première version Pro de SPARK 2014 a été annoncée le 30 avril 2014, et a été rapidement suivie par l'édition SPARK 2014 GPL, destinée aux communautés FLOSS et académiques.
Applications industrielles
SPARK a été utilisé dans plusieurs systèmes critiques de haut niveau, couvrant l'aviation commerciale ( moteurs à réaction Rolls-Royce Trent , le système ARINC ACAMS, le Lockheed Martin C130J), l'aviation militaire ( EuroFighter Typhoon , Harrier GR9, AerMacchi M346), l'aviation -gestion du trafic (système UK NATS iFACTS), ferroviaire (nombreuses applications de signalisation), médicales (le dispositif d'assistance ventriculaire LifeFlow ) et spatiales (le projet CubeSat du Vermont Technical College ).
SPARK a également été utilisé dans le développement de systèmes sécurisés. Les utilisateurs incluent Rockwell Collins (solutions inter-domaines Turnstile et SecureOne), le développement du MULTOS CA original, le démonstrateur NSA Tokeneer, le poste de travail multi-niveau secunet, le noyau de séparation Muen et le crypteur bloc-dispositif Genode.
En août 2010, Rod Chapman, ingénieur principal d'Altran Praxis, a implémenté Skein , l'un des candidats pour SHA-3 , dans SPARK. En comparant les performances des implémentations SPARK et C et après une optimisation minutieuse, il a réussi à faire tourner la version SPARK seulement environ 5 à 10 % plus lentement que C. Amélioration ultérieure du middle-end Ada dans GCC (implémenté par Eric Botcazou d'AdaCore ) a comblé l'écart, le code SPARK correspondant exactement au C en termes de performances.
NVIDIA a également adopté SPARK pour la mise en œuvre de micrologiciels critiques pour la sécurité.
En 2020, Rod Chapman a réimplémenté la bibliothèque cryptographique TweetNaCl dans SPARK 2014. La version SPARK de la bibliothèque dispose d'une preuve auto-active complète de sécurité de type, de sécurité de la mémoire et de certaines propriétés d'exactitude, et conserve des algorithmes à temps constant tout au long. Le code SPARK est également nettement plus rapide que TweetNaCl.
Voir également
Les références
Lectures complémentaires
- John Barnes (2012). SPARK : L'approche éprouvée des logiciels à haute intégrité . Altran Praxis. ISBN 978-0-9572905-1-8.
- John W. McCormick et Peter C. Chapin (2015). Création d'applications à haute intégrité avec SPARK 2014 . La presse de l'Universite de Cambridge. ISBN 978-1-107-65684-0.
- Philip E. Ross (septembre 2005). "Les Exterminateurs" . Spectre IEEE . 42 (9) : 36-41. doi : 10.1109/MSPEC.2005.1502527 . ISSN 0018-9235 .
Liens externes
- Site communautaire SPARK 2014
- Site Internet SPARK Pro
- Site Web édition SPARK Libre (GPL)
- Altran
- L'exactitude par construction : un manifeste pour un logiciel à haute intégrité
- Club des systèmes critiques pour la sécurité du Royaume-Uni
- Comparaison avec un langage de spécification C (Frama C)
- Page du projet de jeton
- Sortie publique de Muen Kernel
- Projet LifeFlow LVAD
- Projet VTU CubeSat