SPARK (langage de programmation) - SPARK (programming language)

ÉTINCELLE
Sparkada.jpg
Paradigme Multi-paradigme
Développeur Altran et AdaCore
Version stable
Communauté 2021 / 1er juin 2021 ; Il ya 4 mois ( 2021-06-01 )
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 Xde un ou de mille ; ou il peut définir un compteur global Xet renvoyer la valeur d'origine du compteur dans X; ou il pourrait ne rien faire Xdu 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 Incrementprocé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 Xest Xelle - 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 Incrementutilisera la variable globale Countdans le même package que Increment, que la valeur exportée de Countdépend des valeurs importées de Countet X, et que la valeur exportée de Xne 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 Xest dérivé de lui seul, mais aussi que before Incrementest appelé Xdoit être strictement inférieur à la dernière valeur possible de son type et qu'après Xsera égal à la valeur initiale de Xplus 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

Systèmes liés à la sécurité

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 ).

Systèmes liés à la sécurité

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

Liens externes