# Ale & Théo : Synthèse TAS ###### tags: `TAS` `Equipe Partielle` ## Glossaire - **IRIS** : Iris est un framework qui peut être utilisé pour raisonner sur la sécurité des programmes concurrents, comme la logique des relations logiques, pour raisonner sur les systèmes de types, l'abstraction de données, etc. - **Coq** : Coq est un assistant de preuve qui permet à son utilisateur de construire des démonstrations de façon semi-automatique, tout en garantissant la correction de ces démonstrations. Ce type d'outil est utile à la vérification de logiciel critique. Coq est l'un des outils de ce type les mieux considéré. ## Contexte Bien que le C ait été créé en 1972 de nombreux systèmes critiques ont été développés et surtout sont toujours développés dans ce langage. La raison de ce choix vient de l'important contrôle qu'offre le C sur la mémoire de la machine permettant une optimisation très fine de cette dernière. Néanmoins ce contrôle excercé par le développeur est aussi une source importante de bug grave pouvant toucher des systèmes particulièrement important. En effet le langage C est utilisé aujourd'hui pour de nombreuses applications critiques comme les systèmes d'exploitations ou les compilateurs et interpréteurs comme celui de python. Des générations de chercheurs et d'ingénieurs ont donc cherché a avoir des outils permettant de réduire les risques que de tel problèmes arrivent et ReffinedC est l'un de ces outils. ReffinedC a donc été créé pour répondre a une simple question : **Ce code source en C est t-il fiable ?** ## La solution proposée dans l'article de référence ### RefinedC RefinedC est en outils permettant, au travers des deux approches "fondamentale" et "automatique" (les deux grandes variétés d'outils dep reuve formelle du C), de fournir les preuves matématiques afin de montrer la fiabilité des programmes écrits en C, utile nottament dans les contextes les plus délicats. | | Pour | Contre | | ----------- | -------------------------------------------------------------------------------------------------------------- |:-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------:| | Fondamental | Limite l'automatisme et est donc plus fiable | Demande une création de preuve importante à la main, l'utilisateur dois créer la preuve a la main | | Automatique | La preuve se créer automatiquement <br> Génère des preuves relativement fiables dépendante de l'implémentation | Ecrire spécifications <br> Ajouter des annotations <br> Ne fournit pas de preuve vérifiable indépendante il est nescessaire de faire des preuves à la main pour contrôler. On est obligés de faire totalement confiance au système automatique. | Les syntèse de ces deux approches va permettre a RefinedC d'avoir les avantages des deux tout en limitant les désavantages. Par exemple refinedC tout en autorisant une importante dose d'automatisme et en limitant l'impact sur le code original va permettre à l'utilisateur de pouvoir suivre l'ensemble des raisonnements appliqués à son programme. #### La toolchain ![](https://i.imgur.com/tj7MSUY.png) La figure 2 de l'article (*Fig 2: The architecture of RefinedC*) nous offre une vue d'ensemble sur ce qu'est RefinedC. On peut observer que la *toolchain* est découpée en deux grandes parties elles même subdivisées. La première représente tout simplement le code source en C que l'on souhaite tester, code source auquel on a ajouté des annotations et specifications qui serviront a aider le système de preuve. Deux exemples sont donnés dans les figures 1 & 3 (Fig1: *Memory allocator example in RefinedC*, Fig3: *Example of an allocator with a freelist*) de l'article. La seconde partie est subdivisée en trois sous-parties : - Le front-end qui permet de convertir le code source C et ses annotations dans un langage nommé Caesium qui permet que l'ensemble soit intelligible pour Coq. - Ensuite Lithium va executer les règles de typages du RefinedC sur le code écrit en Caesium pour prouver les spécifications dans Coq. - Durant le précédent processus des éléments nommés "condition de vérification" qui sont des éléments de Coq pur sont générés. Ces éléments sont soit gérés directement dans Coq soit fournient a part pour que l'utilisateur puissent vérifier les preuves à la main. #### Anotations et spécifications Les annotations sont ajoutées au code source écrit en C pour permettre de rajouter des détails au code C pour faciliter la création de preuve. Ces annotations peuvent être divisées en deux grandes "familles", les annotations servant a décrire une structure et celle, nommée spécifications, permettant la description des actions d'une fonction ou d'une boucle. Nous pouvons les oberver dans deux exemples : la figure 1 (fig 1: *Memory allocator example in RefinedC*) et la figure 3 (Fig 3: *Example of an allocator with a freelist.*) de l'article de référence et évidemment un exemple propre a cette synthèse : ```c= typedef struct [[rc::refined_by("xs: {list Z}")]] [[rc::ptr_type("node_t : {xs <> []} @ optional<&own<...>, null>")]] [[rc::exists("v : Z", "vs: {list Z}")]] [[rc::constraints("{xs = v :: vs}")]] [[rc::constraints("{v ≤ max_int i32}")]] node { [[rc::field("v @ int<i32>")]] int val; [[rc::field("vs @ node_t")]] struct node * next; } node_t; ``` Il s'agit ici d'une liste de int chainée composée d'éléments nommés des `node_t`. Cet exemple est inspiré par celui de la queue disponible sur le [dépôt git du projet](https://gitlab.mpi-sws.org/iris/refinedc). On peut y observer 7 annotations de 5 types différents - `[[rc::refined_by("xs : {list Z}")]]` : Cette annotation n'existe que pour les structures et elle permet d'associer une structure, ici `node_t` a un type dit "raffiné", tout simplement un type coq. Ici il s'agira donc d'une liste de type "Z". En coq le type Z correspond aux entiers signés non-bornés, soit exactement ce que l'on veut car il s'agira d'une liste d'entier 32 bits. - `[[rc::ptr_type("node_t : {xs <> []} @ optional<&own<...>, null>")]]` : Il s'agit de la description permettant à RefinedC de générer un type "raffiné" pour le pointeur de la structure designée a gauche (le nom doit correspondre au "typedef"). On définit donc ici le pointeur de la structure node_t en explicitant que si la liste n'est pas vide *xs* sera une liste de pointeur de node_t sinon *xs* sera égal à null. - `[[rc::exists("v : Z", "vs: {list Z}")]]` : On signifie l'existence d'une variable et de son type coq. Ici on définit donc deux variables : v et vs qui sont respectivement de types "Z" et "list Z". - `[[rc::constraints("{xs = v :: vs}")]]` & `[[rc::constraints("{v ≤ max_int i32}")]]` : Il s'agit des contraintes que doivent respecter les différentes variables à chaque utilisation de la structure. Ici les deux contraintes sont : que "xs" soit une liste constituée de la concaténation de la valeur courante avec les pointeurs des blocs suivants et que v ne soit jamais supérieur à la valeur max autorisée par un int de 32 bits. - `[[rc::field("v @ int<i32>")]]` & `[[rc::field("vs @ node_t")]]` : Cette annotation permet de décrire chacun des champs d'une structure avec ses types "raffinés". Ici v est donc un int de 32 bits tandis que vs est un pointeur node_t. Ces annotations ne représentent qu'une partie de celle disponible. (https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/ANNOTATIONS.md) ### Caesium Grâce a son frontend écrit en Ocaml refinedC va traduire automatiquement le code C annoté un langage parfaitement intelligible pour Coq nommé Caesium. Ce langage va avoir nettement moins de comportement indéfini que l'ISO C et avoir une sémantique plus permissive. Néanmoins il ne couvre pas encore 100% des fonctionnalités de l'ISO C tel que le cast de pointeur d'entier dont la sémantique n'est pas spécifié formellement en ISO C. Un des autres point positifs apportés par ce frontend est l'émission de warning si une expression est non déterministe ou si une fuite mémoire est possible. ### Lithium Lithium est un langage de "separation logic programming", soit un langage permettant de raisonner sur la correction de programmes en suivant un formalisme précis. Ce langage permet de décrire les types et les règles de typage officiant lors de la génération de preuve par RefinedC. Pour que les preuves générées par RefinedC soit aussi générée en lithium il est néscessaire d'ajouter l'annotation : `[[rc::manual_proof("refinedc.tutorial.lithium:lithium, type_lithium_test")]]` à la fonction visée. Il va alors générer un fichier écrit en lithium décrivant l'approche de la recherche de preuve et comment cette recherche est implémantée en Coq (https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/tutorial/lithium.c & https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/tutorial/proofs/lithium/lithium.v) La génération du code lithium va chercher a limiter les erreurs possible. Une fois généré cela permet a l'utilisateur de constater le fonctionnement de refinedC et possiblement refaire la preuve à la main. Le lithium autorise donc une certaine transparence dans le fonctionnement de RefinedC et permet donc à l'utilisateur de ne pas a avoir à croire sur parole le système. ### Règles de typages **RefinedC** a des "jugements" de type pour chaque construct,(tous les elesments du c ex. boolean, entiers et ainsi suite) comme par exemple - `⊢if` pour les conditions booleennes - `⊢binop`pour les opérateurs binaires selon le type de condition une règle de typage différente est appliqué et le typage est par conséquent effectué différemment selon le contexte, ce qui est important car <mark>en C le même construct peut-être utilisé pour des fins différentes</mark>. Les jugements spécifiques à un construct apparaissent dans la structure des règles pour les jugements généraux d'énoncés et d'expressions: #### Règles de typage optionnelles : Le type optionnel de **RefinedC** joue un rôle clé dans la gestion du modèle de programmation de bas niveau courant qui consiste à coder une valeur d'erreur comme `NULL` (`e=NULL`). La plupart des utilisations de ce modèle peuvent être gérées par trois règles de typage du RefinedC : * Par les règles `S-null` et `S-own` pour introduire un type optionnel * Par la règle `O-optional-eq` pour comparer une option avec `NULL` comme dans la figure ci-dessous : ![](https://i.ibb.co/Gpk2yzt/Schermata-2021-10-30-alle-15-59-04.png) La règle `O-optional-eq` est utilisée pour prouver : ![](https://i.imgur.com/0MDVbvu.png) Afin de le prouver Lithium : 1. Applique `t-if` dont l'expression demande de typer e =null `if (e=NULL)` 2. Applique `t-binop` qui demande de typer e `then s1 else s2` La règle `^` permet de spécifier deux cas: * Quand le type`𝜙` est contenu dans l'expression: `v1` doit être un pointeur `&own`, qui ne peut pas être égal à `NULL`, donc on renvoit faux. ![](https://i.imgur.com/8f9ElqS.png) * Si le type `𝜙` n'est pas contenu: `v1`doit forcement être égal à `NULL` car il est égal à `v2` qui vaux lui-même déjà `ǸULL`. G est vérifié comme `true` et `¬𝜙` est ajouté au contexte. ![](https://i.imgur.com/pGXFpOl.png) Dans les deux cas l'expression vérifiée par `O-optional-eq` continue le typage en appliquant la règle `If-BOOL` instanciée à `true` ou `false` selon le résultat précedent. ![](https://i.imgur.com/WLXDpGJ.png) #### Raisonnement sur la propriété : La règle `O-ADD-UNIT` explique comment la syntaxe du programme guide le raisonement des proprietés sur **RefinedC**: ![](https://i.imgur.com/hmpjcFd.png) `O-ADD-UNIT` type l'addition d'un entier `𝑛2` avec `v1` en un pointeur d'une mémoire non initialisée de longueur `𝑛1`. La règle vérifié que `0 ≤ 𝑛2 ≤ 𝑛1` et ensuite divise `uninit(𝑛1)` en deux petits morceaux `uninit(𝑛2)` et `uninit(𝑛1 - 𝑛2)`. Comme dans la figure ci-dessus. `O-add-uninit` peut être utilisé dans d'autres contextes où les programmes ajoutent des valeurs de type `&own(uninit(𝑛))` et `int(size_t)`. #### Concurrence : RefinedC peut également vérifier automatiquement du code concurrent. Nous illustrons cela avec le type atomicbool(𝐻⊤, 𝐻⊥), qui représente un booléen auquel on peut accéder de manière atomique. Le type détient la propriété de * 𝐻⊤ booléen $\to$ vrai * 𝐻⊥ booléen $\to$ faux La principale opération atomique supportée par le type atomicbool est l'opération `atomic_compare_exchange_strong`, correspondant à l'opération `CAS(l𝑎𝑡𝑜𝑚,l𝑒𝑥𝑝,v𝑑𝑒𝑠)` de Caesium. * `l𝑎𝑡𝑜𝑚` est un pointeur sur la valeur a modifier de manière atomique. * `l𝑒𝑥𝑝` est un pointeur vers la valeur actuelle attendue de `l𝑎𝑡𝑜𝑚` . * `v𝑑𝑒𝑠` est la valeur à attribuer à `l𝑎𝑡𝑜𝑚`. CAS est vérifiée à l'aide de la règle Cas-bool. Les deuxième et troisième arguments de CAS ont des types booléens singuliers qui déterminent si la prémisse utilise 𝐻⊤ ou 𝐻⊥. Cas-bool a deux cas correspondant au fait que le CAS échoue ou réussit. ![](https://i.imgur.com/dFa6DcB.png) * **Premier cas:** Lorsque le CAS échoue, le second argument est mis à jour en ¬𝑏1, et false est retourné. * **Deuxième cas:** Lorsque le CAS réussit, nous recevons la propriété stockée avec le booléen atomique avant le CAS, et nous devons prouver la propriété stockée après le CAS. Par la suite, nous recevons la propriété de v2 , et le CAS renvoie true. ## Résultats Pour mener l'évaluation du refinedC l'équipe de chercheur a mené des tests sur un ensemble de cas jugés représentatifs. ### Les métriques Ces cas vont être évalués aux travers de différentes métriques permettant de constater l'étendue des fonctionnalités du refinedC : - Listes des types refinedC utilisés comme par exemple *wand* ou *alloc* - Le nombre de règles de typages utilisées pour prouver les types dans l'exemple qu'ils soient déjà présent dans la bibliothèque standard ou définient par l'utilisateur - Nombre de quantifieurs instanciés automatiquement. Cette valeur permet donc d'évaluer son l'efficacité par rapport a d'autres outils où il aurait fallu manipuler manuellement les différents éléments. - Nombre de condition prouvées automatiquement par le solveur par défaut de refinedC et celle restant à prouver manuellement. - Le nombre de ligne de code écrite en C composant le code source de l'exemple. - Nombre de lignes de spécifications écrites dans le code en C. - Nombre d'annotations dans le code source détaillées entre celle dans les structures de données, les boucles et les autres annotations. - Nombre de lignes de raisonnements Coq pur incluant les définitions et les lemmes servant à prouver les conditions manuellement. - Somme des annotations et des lignes de pur Coq divisés par le nombre de ligne en C. Servant a mesurer la proportion de lignes de codes ajoutées par l'utilisateur à un code C pour le prouver. ### Les cas Les programmes sur lesquels vont être évalués le refinedC sont au nombre de onze comme il est possible de le voir sur la Figure 7 de l'article de référence (*Fig 7: Evaluation of RefinedC.*), ils vont être répartis en six familles : - **Les cas d'études dis "communs" :** Ces sont trois exemple qu'il n'est vraiment pas rare de croiser dans de nombreux outils de verifications. Ils couvrent les usages basiques du C et de RefinedC et permettent donc d'avoir un bon point de comparaison. - **Les cas exposant le système de propriété de RefinedC :** Ces cas permettent de mettre en valeur toutes les annotations permettant la manipulation de la propriété des pointeurs. - **Verification directs et indirects :** Une des approches les plus populaires dans la vérification est le fait de découper les différentes tâches en plusieurs couches de specifications intermédiaires. Pour mesurer la performance de refinedC avec ces deux approches deux arbres binaires de recherches ont été implémantés, l'un suivant l'approche dites "indirect" ou "par couche" alors que l'autre suit une approche direct. Bien que les deux approches soient viables, en regardant les chiffres on observe alors des valeurs relativement similaire dans les différentes métriques concernant les règles. Par contre l'approche par couches requiert 13 fois plus de lignes de Coq pur ce qui implique donc une complexité importante. - **Les raisonnements fonctionnels complexes :** Ce cas permet de mettre en exergue que le refinedC va réduire la vérification de la fiabilité d'opération sur une "hashmap avec linear probing" a un pur raisonnement logique qui va être déchargé dans Coq et écrit dans ce dernier. C'est pour cela qu'il s'agit du cas avec le plus de ligne de pur coq. - **Le code issus de véritables utilisation industrielle :** Ce cas permet de mettre en évidence le fait que RefinedC peut servir a prouver du code source issu d'une utilisation plus industrielle. Ici refinedC a été utilisé pour vérifer l'"allocator" de l'hyperviseur Hafnium et montre des résultats brillament proche des métriques obersvables dans les cas dit "communs" d'autant qu'aucun nouveau type n'a eu a être déclaré dans refinedC. - **Abstraction concurrente :** Ces cas montrent que RefinedC peut être utilisé dans un cas qui était resté hors de porté de beacoups d'autre outils de preuves automatiques, la programmation concurentielle. ## Travaux liés Malgré le fait que RefinedC soit un outil très puissant permettant de prouver la fiabilité du code C, il existe plusieurs projets alternatifs qui ont plus ou moins les même objectifs en présentant bien entendu, des avantages et des inconvenients par rappport à la technologie analysée dans le cadre de cette synthèse: En particulier nous avons : * **Bedrock** : outils permettant la verification "fondamentale" et "automatique" comme en RefinedC et tout comme ce dernier a pour objectif de pouvoir tester les programmes de bas niveau. Il code les spécifications et les prédicats abstraits dans une logique de séparation simple. Au contraire RefinedC exploite des abstraction de haut niveau pour un système de type rafiné pour conduire l'automatisation. Bedrock n'est pas non plus capable de représenter des règles tel que `CAS_Bool` comme en Refined C. * **VST** : basé sur la logique de séparation pour la vérification des programmes C. Les utilisateurs de VST déploient: * un ensemble de tactiques semi-automatiques pour construire des preuves de correction fonctionnelle dans Coq * un fronend qui utilise l'annotation du code source pour réduire la vérification à un ensemble d'entraînements qui doivent être prouvés dans Coq. Dans les deux cas, l'utilisateur doit guider manuellement la preuve en en appliquant des lemmes, etc. - Vérification fondamentale des programmes C à grande échelle | | Pour | Contre | | ----------- | ------------------------------------------------------------------ | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | **seL4** | seL4 a démontré la première preuve formelle de la correction fonctionnelle d'un noyau complet de système d'exploitation à usage général et est accompagné d'une procédure de traduction-validation permettant de transférer les preuves au code assembleur généré. | <ul> <li> La plupart des preuves de seL4 concernant le code C sont manuelles et ne reposent que sur un support tactique de base.</li> <li> Cette automatisation, ne supporte pas des aspects du C comme la concurrence</li> </ul> | | **CertiKOS** | La vérification de CertiKOS est intégrée au compilateur C, de sorte que la preuve s'applique au code d'assembleur généré. La technique de preuve utilisée est basée sur l'écriture de programmes à différents niveaux d'abstraction et la preuve des raffinements entre ces niveaux. | Les preuves de raffinement sont déchargées en guidant manuellement des tactiques spécialisées dans Coq - Vérification du c par les outils non fondamentels | | Dans cette technologie | En RefinedC | ------------ | ---------- | --- | **VCC** | utilise des solveurs SMT (Vérificateurs de formules) pour vérifier les programmes C et a été utilisé sur de grands programmes C en pratique. | il manque un bon support pour le raisonnement de propriété dynamique. Par exemple, un prédicat de liste liée qui prend en charge le test des membres nécessite trois champs fantômes, qui doivent tous être mis à jour manuellement dans la fonction d'ajout. De tels champs fantômes et annotations ne sont pas nécessaires dans RefinedC. | **VeryFast** | <li>fournit des heuristiques pour déduire automatiquement les annotations afin de réduire la charge de la preuve.</li><li> L'approche d'exécution symbolique de VeriFast utilise une règle fixe pour chaque construction de programme</li> | <li>bénéficie également des bibliothèques Coq existantes comme std++ par exemple l'arbre de recherche binaire nécessite environ la moitié du nombre de lignes de raisonnement pur par rapport à un exemple similaire dans VeriFast par une utilisation judicieuse des lemmes et tactiques existants.</li> | **MatchC** |<li>Son approche basée sur la réécriture fournit une bonne automatisation pour les programmes non triviaux manipulant des pointeurs et peut être étendue avec de nouvelles abstractions et des règles personnalisées</li> |les abstractions de MatchC et leurs règles ne sont pas prouvées par rapport à un modèle, et doivent être fiables. MatchC ne supporte pas non plus la concurrence. - Vérification de crypto - **Fiat Crypto** fournit un langage pour la cryptographie en Coq, qui est compilé en C. En raison de la concentration exclusive sur la cryptographie, ces projets ne supportent pas certaines caractéristiques du C qui sont supportées par RefinedC, comme les types de données récursifs, les pointeurs de fonction et la concurrence. - Sécurité de la mémoire dans les langages de programmation de bas niveau. - De nombreux travaux antérieurs à RefinedC se concentrent plutôt sur le problème différent de la vérification automatique de la sécurité de la mémoire. RefinedC vise la vérification sans affecter la sémantique dynamique du programme. **Low-Level Liquid Types** vérifie la sécurité mémoire du code C en utilisant une combinaison de types de raffinement et de types d'alias . L'objectif de ces outils est uniquement la sécurité de la mémoire. RefinedC vise une vérification fonctionnelle complète, et nécessite donc plus d'annotations mais peut également vérifier plus de programmes. - Typage sémantique. - L'approche de typage sémantique de RefinedC comme la construction d'un modèle sémantique de types au-dessus d'Iris est modelée sur celle de RustBelt. - Cependant, la conception concrete du système de type de RefinedC diffère de RustBelt dans plusieurs aspects clés : - RefinedC inclut des types de raffinement en plus des types de propriété - RefinedC supporte la vérification automatique des types, ce que RustBelt ne fait pas ## Perspective et limite RefinedC, malgré l'automatisation efficace de la vérification du code C, reste un outil assez récent et par conséquent présente encore un certain nombre de limitations que les auteurs prevoient de dépasser dans le futur: - Caesium et le front-end ne supportent pas certaines caractéristiques du langage C comme les flottants ou les conversions entiers-pointeurs qui nécessite plus de recherche pour trouver la bonne sémantique. - RefinedC ne supporte pas actuellement le raisonnement sur les appels de fonctions externes et le comportement entrée-sortie des programmes - Il existe des idiomes de programmation C qui ne sont pas encore couverts par les règles de typage existantes. Par exemple, bien que les accès aux tableaux soient déjà bien supportés, des règles de typage pour les pointeurs sur les éléments de tableaux ne sont toujours pas supportées ## Conclusion En conclusion nous pouvons dire que les rédacteurs de cet article ont créé un outils particulièrement puissant notament par rapport aux outils concurrent qui se limites à certaines approches, pour pouver la fiabilité du code C. La toolchain sur laquelle repose tout l'article propose une grande adaptabilité et une importante transparence pour l'utilisateur tout en limitant son action autant sur le code source que sur la génération de preuve. Bien que cet outil soit encore récent et nécessite des ameliorations dans les années à venir, il représente déjà une solution permettant d'augmenter la production des logiciels pour lesquels une vérification de fiabilité est fondamentale.