Journal Re-implémentation de TweetNaCl en Spark

Posté par  (site web personnel, Mastodon) . Licence CC By‑SA.
Étiquettes :
28
26
jan.
2022

Sommaire

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.

  • # Spark

    Posté par  . Évalué à 5.

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

    À ne pas confondre avec Spark

    « Rappelez-vous toujours que si la Gestapo avait les moyens de vous faire parler, les politiciens ont, eux, les moyens de vous faire taire. » Coluche

    • [^] # Re: Spark

      Posté par  (site web personnel, Mastodon) . Évalué à 2. Dernière modification le 26 janvier 2022 à 11:21.

      Ça explique la montée du score du journal puis sa descente :D

      Alors effectivement, après vérification, l'orthographe correcte est SPARK.

      C'est parce qu'Ada est insensible à la casse que je n'y pense jamais :)

      Après, si je voulais être mauvais joueur, je dirai que SPARK existant depuis la version Ada 83, on peut estimer qu'il y a antériorité et que de toutes façons, on devrait dire Apache Spark ;)

      • [^] # Re: Spark

        Posté par  . Évalué à 4.

        Je ne dis pas le contraire, mais j'ai plutôt entendu parler d'Apache Spark, du coup, je me posais la question de l'intérêt d'implémenter TweetNaCl dans celui-ci.

        « Rappelez-vous toujours que si la Gestapo avait les moyens de vous faire parler, les politiciens ont, eux, les moyens de vous faire taire. » Coluche

        • [^] # Re: Spark

          Posté par  (site web personnel, Mastodon) . Évalué à 2.

          Je suis bien d'accord avec toi, la popularité n'est pas la même du tout ;)

          Les recherches sur Spark dans les moteurs sont toujours un peu ardues du coup.

  • # Commentaire pédantique

    Posté par  . Évalué à 3.

    pour dire que c'est simplement "Kelvin" l'unité, et pas "degré Kelvin".

    Je sais où se trouve la sortie, merci :D

  • # Tweet ?

    Posté par  . Évalué à 4. Dernière modification le 28 janvier 2022 à 09:22.

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

    C'est quoi l'intérêt? on envoie la bibliothèque par tweets ? ;-)
    Le tweet est devenu une unité de mesure ? Et tout programme dont le code source tient en n tweets peut/doit être nommé avec tweet comme préfixe ? (du coup il faudrait tout renommer parce qu'il suffit de prendre un n suffisamment grand, on aurait ainsi un tweetWindows par exemple)

    Au fait on parle d'anciens ou de nouveaux tweets (140 ou 280 caractères) ? ;-)

    • [^] # Re: Tweet ?

      Posté par  (site web personnel, Mastodon) . Évalué à 2. Dernière modification le 28 janvier 2022 à 09:40.

      C'est quoi l'intérêt? on envoie la bibliothèque par tweets ? ;-)

      Oui, c'est l'intérêt car cela permet, me semble-t-il, de s'affranchir de certaines restrictions dans les règles d'export control américains en termes de matériel cryptographique.
      Enfin, y a rien de moins sûr parce qu'il semble que les softs en domaine publique soient épargnés par ces règles… Sauf peut-être si on exporte vers un pays soumis à embargo US.

      Au fait on parle d'anciens ou de nouveaux tweets (140 ou 280 caractères) ? ;-)

      Comme les anciens et les nouveaux francs ? :D

      • [^] # Re: Tweet ?

        Posté par  . Évalué à 3.

        Oui, c'est l'intérêt car cela permet, me semble-t-il, de s'affranchir de certaines restrictions dans les règles d'export control américains en termes de matériel cryptographique.

        Je suis très curieux, il y a un nombre incalculables de projets qui ne semble pas rencontrer le problème (gpg, linux, openssl, libressl, gnutls, java, clr, bouncy castle, windows, les cpu intel,…).

        https://linuxfr.org/users/barmic/journaux/y-en-a-marre-de-ce-gros-troll

        • [^] # Re: Tweet ?

          Posté par  . Évalué à 3.

          https://tweetnacl.cr.yp.to/tweetnacl-20140917.pdf

          TweetNaCl is human-readable C code; it is the smallest readable implementation of a high-security cryptographic library.

          Je pense que le truc des 100 tweets c'est surtout pour montrer la performance de taille. Après ils ont brodé sur «the tweets are available from anywhere, any time, in an unsuspicious way. Distribution via other social media, or even printed on a sheet of A4 paper, is also easily possible.»

          • [^] # Re: Tweet ?

            Posté par  (site web personnel, Mastodon) . Évalué à 2.

            Merci, ça explique l'aspect pouet dans le nom. Et pour l'aspect salin ou salant ?

            “It is seldom that liberty of any kind is lost all at once.” ― David Hume

            • [^] # Re: Tweet ?

              Posté par  (site web personnel, Mastodon) . Évalué à 2. Dernière modification le 28 janvier 2022 à 17:32.

              From Wikipedia:

              NaCl (pronounced "salt") is an abbreviation for "Networking and Cryptography library"

              TweetNaCL est une ré-écriture de NaCL dont une implémentation alternative est libsodium :)

              • [^] # Re: Tweet ?

                Posté par  (site web personnel, Mastodon) . Évalué à 2.

                Merci pour l'info, c'est un sigle et acronyme fort élégant je trouve.
                Par contre l'autre implémentation a oublié le chlorure dans son bain, si j'en crois le nom. :-)

                “It is seldom that liberty of any kind is lost all at once.” ― David Hume

        • [^] # Re: Tweet ?

          Posté par  (site web personnel, Mastodon) . Évalué à 2.

          En fait, ça s'est très assoupli vu qu'il ne faut plus que faire une déclaration sans revue mais il reste encore quelques petits trucs et dixit Wikipedia, cela reste complexe.

          Donc j'ai dit des conneries :D

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.