URL: https://linuxfr.org/users/blackknight/journaux/re-implementation-de-tweetnacl-en-spark Title: Re-implémentation de TweetNaCl en Spark Authors: Blackknight Date: 2022年01月26日T00:07:21+01:00 License: CC By-SA Tags: ada, spark, preuves et compilation Score: 28 A l'origine, ce n'était qu'[un lien](https://linuxfr.org/users/blackknight/liens/re-implementation-de-tweetnacl-en-spark) mais finalement, cela méritait un journal sur [Spark](https://en.wikipedia.org/wiki/SPARK_(programming_language)). 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 : ```ada 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 ```ada 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. ```ada 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 : ```ada 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: ```ada 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](https://tweetnacl.cr.yp.to/) 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](https://blog.adacore.com/sparknacl-two-years-of-optimizing-crypto-code-in-spark-and-counting) 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.

AltStyle によって変換されたページ (->オリジナル) /