Suport technique et veille technologique

LinuxFr.org : les journaux  -  Re-implémentation de TweetNaCl en Spark

 -  Janvier 2022 - 

Sommaire

• Mais c'est quoi Spark ?
• Show me the code
  • Les types
  • Les fonctions
  • Le programme principal
• Spark en action
• TweetNaCl

A l'origine, ce n'était qu'un lien mais finalement, cela méritait un journal sur Spark.

Avant de vous filer le lien sur le portage, on va commencer par un petit exemple rapide de ce que peut faire Spark.

Mais c'est quoi Spark ?

Spark est, aujourd'hui, un sous-ensemble d'Ada restreignant les capacités aux fonctions sécurisées et non-abmigües.

Via un ensemble d'aspects, une sorte d'annotations, le compilateur gnatprove génère des conditions de vérification pour chaque sous-programme.
Ces conditions de vérification sont ensuite passées à un ou plusieurs prouveurs afin de vérifier que les conditions sont maintenues tout au long de l'exécution du programme.

Dans la liste des conditions, on trouvera notamment :
- l'absence de dépassement d'index d'un tableau
- l'absence de débordement d'une variable numérique
- le respect des contraintes de type (la plage de valeurs acceptable)
- l'absence de division par zéro

Il existe bien sûr d'autres vérifications plus complexes mais ce n'est pas le but de ce journal.

Show me the code

Commençons par un simple exemple pour montrer la capacité de Spark à prouver un code sans ajouter des tonnes de choses.

Un package de conversion °C vers °K et inversement m'a semblé suffisamment simple pour montrer cela.

Les types

En Ada, on commence généralement par définir les types.

Ici, pour faire simple, on ne traite que des entiers, ce qui nous donne la spécification de package suivante :

package Temperatures with
   SPARK_Mode => On
is

   type Kelvin is range 0 .. Integer'Last;
   type Celsius is range Kelvin'First - 273 .. Integer'Last;

   function convert_to_c (temp_k : Kelvin) return Celsius 
      with 
         Global => null;

   function convert_to_k (temp_c : Celsius) return Kelvin
      with
         Global => null;

end Temperatures;

Le 0°K étant le zéro absolu, il s'agira forcément d'un entier positif.
Nous nous servons aussi de cette propriété pour définir le °C. Ainsi, on sait que l'on ne peut descendre en dessous de -273°C (pour le plaisir, j'ai utilisé Kelvin'First qui représente la première valeur du type).

Les fonctions

A la suite des déclarations de type, on trouve les deux fonctions de conversion précisant via l'annotation With Global => null que ces fonctions ne dépendent d'aucune variable globale.

Le corps du package est trivial

package body Temperatures with
   SPARK_Mode => On
is

   function convert_to_c (temp_k : Kelvin) return Celsius is
   begin
      --  On doit faire un cast bien que les deux types soient des entiers
      --  Ils sont incompatibles entre eux
      return Celsius (temp_k - 273);
   end convert_to_c;

   function convert_to_k (temp_c : Celsius) return Kelvin is
   begin
      --  On doit faire un cast bien que les deux types soient des entiers
      --  Ils sont incompatibles entre eux
      return Kelvin (temp_c + 273);
   end convert_to_k;

end Temperatures;

Le programme principal

Le programme principal ne fait rien d'extraordinaire, juste deux conversions de l'affichage.

with Ada.Text_IO;  use Ada.Text_IO;
with Temperatures; use Temperatures;

procedure Test_Convert with
   SPARK_Mode => On
is

   temp_c : Celsius := -273;
   temp_k : Kelvin  := 0;

begin
   Put_Line
     ("Temp " & Celsius'Image (temp_c) & "°C vaut " &
      Kelvin'Image (convert_to_k (temp_c)) & "°K");

   Put_Line
     ("Temp " & Kelvin'Image (temp_k) & "°K vaut " &
      Celsius'Image (convert_to_c (temp_k)) & "°C");
end Test_Convert;

Spark en action

Le lancement de gnatprove sur le programme précédent renvoie le résultat suivant

Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

temperatures.adb:12:29: medium: overflow check might fail
   12 |      return Kelvin (temp_c + 273);
      |                     ~~~~~~~^~~~~
  reason for check: result of addition must fit in a 32-bits machine integer
  possible fix: subprogram at temperatures.ads:11 should mention temp_c in a precondition
   11 |   function convert_to_k (temp_c : Celsius) return Kelvin with
      |   ^ here

En ne se basant que sur les définitions de type, Spark trouve une erreur. En effet, le résultat de l'addition peut déborder.
Si cela est autorisé en Ada moyennant une exception, c'est interdit en Spark.
La proposition est de placer une précondition sur le paramètre :

   function convert_to_k (temp_c : Celsius) return Kelvin with
     Global => null,
     Pre => Temp_C < Celsius(Integer'Last - 273);

Avec cette précondition, gnatprove accepte notre programme.

Une deuxième possibilité, si on n'utilise pas les °C par ailleurs, est de contraindre un peu plus le type:

   type Celsius is range Kelvin'First - 273 .. Integer'Last - 273;

Cela suffit aussi.

Il faut noter que le code mis ici est du code Ada valide et que la précondition est utilisée pour placer un runtime check dans le code final.

Voilà pour une première prise de contact avec Spark qui vous donnera quelques clés pour lire la suite.

TweetNaCl

TweetNaCl est une bibliothèque de cryptographie écrite en C et optimisée pour tenir dans 100 tweets.

Rod Chapman, un habitué de Ada et de Spark, a commencé à porter la bibliothèque en Spark en 2019, le confinement a semble-t-il aidé à avancer sur le sujet.

Plusieurs phases ont été nécessaires afin d'écrire les contrats permettant de prouver puis d'optimiser le code pour améliorer les performances mais le résultat est là.
Au final, après pas mal de boulot, l'intégralité du code est prouvé (pas mathématiquement hein, n'exagérons rien).

Un des avantages qui ressort est, qu'à l'instar des tests unitaires, la preuve de code a permis de faire du refactor lors de l'optimisation tout en garantissant que le code fonctionnait toujours.

Vous retrouverez tout ça dans cet article qui contient une vidéo explicative ainsi que tous les liens vers les précédents articles écrits au fil de l'eau par Rod.

C'est souvent complexe mais super intéressant.

Commentaires : voir le flux Atom ouvrir dans le navigateur

par Blackknight