# Ale & Théo : Plan de synthèse
###### tags: `TAS` `Equipe Partielle`
@theOnlyAlex @sroFAHGMRJaJlDo7cVYdbw

*Lien :* https://plv.mpi-sws.org/refinedc/paper.pdf

Gilab du projet a priori : https://gitlab.mpi-sws.org/iris/refinedc

# Glossaire
- Preuve fondamentale :
- Preuve automatique :
- IRIS : Iris is a framework that can be used for reasoning about safety of concurrent programs, as the logic in logical relations, to reason about type-systems, data-abstraction etc.
- Coq :

# Résumé chapitre par chapitre :

## Introduction
Le C est toujours un des langages les plus utilisés dans les applications critiques, principalement du système. La gestion de la mémroire offerte par le C peut mener a des bugs critiques grave qui doivent être évités.
Pour cela il existe des outils permettants de créer des preuves formelles, ils peuvent se découper en deux grandes catégories : fondamentale et automatique

| / | 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 fiables | 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 obliger de faire totalement confiance au système automatique. |

Le **RefinedC** est donc un nouvel outils pour vérifier le C qui mixe les deux approches.

**Automatique :**
- *Refinement Type*
- *Ownership Types*

## RefinedC By example

Dans cette deuxième partie nous allons voir deux examples pour introduire redefined C du point de vu de l'usager:

### Un simple allocateur de memoire

`[[rc:: valeur]]`répresent l'annotation du refined C

- concernant la structure `mem_t`
- `refined_by(("a: nat"))` exprime une version refinie (refined) de mem_t
et une spécification comportamental de l'`alloc`
- `field((a @ int<size_t>"))`ici le refiné mem_t est indexé par le nb naturel a (le nb d'octet disponibles pour l'allocator) cette valeur doit matcher la valeur stockée dans le champs `len`
- `field("&own<uninit<a>>")` indique que le champs buffer est un pointeur d'un bloc possedu `(&own)` de mémoire de taille a

- Concernant l'`alloc`
- `rc::args` l'argument `d` point `struct mem_t` avec a comme nb d'octets disponibles et l'argument sz qui est égal a un entier `n`
- `rc::returns("{n≤a} @ optional<&own<uninit<n>>, null>") ` spécifique que le type refinie de la valeur `alloc` return une valeur optionelle (`optional`) qui point un bloque non initialisé de taille `n` si `n≤a`sinon il return `NULL`
- `rc::ensures("ownp:{n ≤ a?a-n:a}@mem_t")` après le retour àlloc`renvoie la proprieté de `p`(le pointeur passé en argument de d) mainenant il point à `mem_t` de la taille appropriée réduite

//l'état de l'allocateur de mémoire 
struct [[rc::refined_by("a: nat")]] mem_t { 
//la taille du buffer c'est len
[[rc::field("a @ int<size_t>")]] size_t len; 
//un bloque de mémoire point sur buffer
[[rc::field("&own<uninit<a>>")]] unsigned char* buffer;
};


[[rc::parameters("a: nat", "n: nat", "p: loc")]]
[[rc::args ("p@&own<a@mem_t>","n@int<size_t>")]]
[[rc::returns("{n≤a} @ optional<&own<uninit<n>>, null>")]] 
[[rc::ensures("ownp:{n ≤ a?a-n:a}@mem_t")]] 

/* la fonction alloc essaye de stocker sz (le param) en mémoire par 
la structure mem_t */
void* alloc(struct mem_t* d, size_t sz) {

/* en utilisant len il vérifie d'abord si la mémoire est disponible en renvoyent 
null s'il n'y a pas assez */
if(sz > d->len) return NULL;

/* si buffer est assez large ces derniers sz octets sont stockés 
en utilisant le pointeur aritmethique et len est mis à jour */
d->len -= sz;
return d->buffer + d->len;
}

## RefinedC front end and Caesium
Avant d'être verifié par RefinedC le programme C va être "convertit" dans un autre langage dénommé *Caesium* par le front refinedC. *Caesium* est un langage fortement prouvé avec Coq.
Sa sémantique est plus permissive que celle du ISO C et a moins de comportement indéfini, néanmoins certaine fonction avancée du C ne sont pas disponible avec Caesium.
=> Cela permet d'émettre des warning si une expression en C n'est pas déterministe o usi une fuite de bloc mémoire est possible.

La base de confiance du RefinedC inclus l'implem de son front en Ocaml et la sémantique de Caesium.

Et le générateur de code *Lithium* n'a pas besoin d'être cru "sur parole" tout comme les preuves en Coq car il génère des preuves lisible et indépendante dans Iris (un outils de visualisation de preuve ?)
## RefinedC Types and spec

La plupart des types peuvent avoir un predicat logique sur les valeurs du type appellé "raffinement" un paramètre optionnel qui limite les valeurs du type, dont le tri de niveau et du prédicat varie d'un type à l'autre.
Les fonctions quant a elles, ont un type en RefinedC de la forme fn(expression) -> expression du resultat. Le type des fonctions sont générés par les annotations du code source qu'on a déjà rencontrés.

## Lithium: Separation logic programming
Lithium est un langage permettant de décrire comment les preuves sont cherchées et comment cette recherche est implémentée dans Coq.
Lithium cherche donc a montrer le déroulement de recherche de preuve sans *backtracking* sans retour en arrière.
Il a une syntaxe très mathématique (que je ne résumerais pas ici, elle est diapo 7).
La force de Lithium est d'éviter les retour en arrière, les backtrackings.
L'un des points les plus importants de lithium est la gestion des *evars*(?) et sa capacité a éviter les erreurs en les traitant.
Il est implémenté en LTac et est lié structurelement a Coq et IRIS.
Il est aussi extensible via les types définis par l'utilisateurs

## Examples of RefinedC typing rules
Toute règle de typage est de la forme $\frac{G}{F}$ ou G c'est l'objectif Lithium et F c'est l'objectif basique Lithium qui encode un évaluations de typage en RefinedC.

RefinedC a des évaluations spécifiques de typage pour chaque construction du programme :
- `e.g., ⊢if` pour les conditions booleennes
- `⊢binop`pour les opérateurs binaires

### Les évaluations de base :
Selon le type de la condition une règle differente est appliquée et le typage procède donc différemment: par exemple selon le type de condition bool ou int de la figure ci-desous, une évaluation differente est appliqué.
Cette surcharge de types permet RefinedC de manipuler le même construct du program selon le contexte ce qui est très important car <mark> en C, la même "construct" peut servir à des fins différentes</mark>


Les évaluations spécifiques à la construction apparaissent dans les prémisses des règles pour les évaluations généraux d'énoncés et d'expressions.
Cette continuation a deux objectifs :
Tout d'abord, la saisie d'une expression infère un type 𝜏. Ce type, ainsi qu'une valeur inférée (symbolique) v pour le résultat, est passé comme argument à la continuation. Deuxièmement, la continuation est utilisée pour linéariser la vérification de type.
Ce style de passage de continuation assure que chaque prémisse de règle de typage a une formule logique, ce qui simplifie l'implémentation de Lithium.

### 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`.

La plupart des utilisations de ce modèle peuvent être gérées par trois règles de typage du RefinedC :
* la règle `O-optional-eq` pour comparer une option avec `NULL`
* pour introduire un type optionnel :
* `S-null`
* `S-own`

comme dans la figure ci-dessous :


la règle `O-optional-eq` est utilisée pour prouver `⊢Σ STMT`? `if(r=NULL) then s1 else s2`. Pour le prouver :
1. il applique `t-if`dont la promesse require de typer l'expression booleene `e= NULL`
2. il applique `t-binop` qui require de typer e.

#### Expression `O-optional-EQ` :
la règle distingue deux cas à travers l'expression `^` quand `𝜙` est contenu ou pas:
* quand `𝜙` est contenu , `v1` doit être un pointeur possédé, qui ne peut pas être égal à `NULL`, donc le résultat de la vérification de l'égalité dans la conclusion de la règle doit être faux.

* si `𝜙` n'est pas contenu `v1`doit forcement être `NULL`égal à `v2` G est vérifié comme `true` et `¬𝜙` est ajouté au context


Dans les deux cas l'expression `⊢Σ STMT`? `if(r=NULL) then s1 else s2` continue avec la règle `If-BOOL` instincié à true ou false selon le résultat précedent.

En suite il est expliqué commment Lithium étabilie si si une valeur `v` a le type
`𝜙 @ optional(&own(𝜏),null)`

#### Raisonnement sur la propriété :

Le raisonement sur comment la syntaxe du program guide le raisonement sur la proprieté est réalisé dans la règle `O-ADD-UNIT`:

Cette règle type l'addition d'un entier `𝑛2` à un pointeur vers une mémoire non initialisée de longueur `𝑛1` (le type de RefinedC `uninit(𝑛1)`). La règle vérifié que `𝑛2 ≤ 𝑛1` et ensuite divise `uninit(𝑛1)` en deux petits morceaux `uninit(𝑛2)` et `uninit(𝑛1 - 𝑛2)`.

<mark>`O-add-uninit` peut être réutilisé dans d'autres contextes où les programmes ajoutent des valeurs de type `&own(uninit(𝑛))` et `int(size_t)`.</mark>

#### Concurrence à grain fin :

RefinedC peut également vérifier automatiquement du code concurrent à grain fin. 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 -> vrai
* 𝐻⊥ booléen -> 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. Le premier argument
1. `l𝑎𝑡𝑜𝑚` est un pointeur sur la valeur à modifier de manière atomique,
1. `l𝑒𝑥𝑝` est un pointeur vers la valeur actuelle attendue de `l𝑎𝑡𝑜𝑚`, et
1. `v𝑑𝑒𝑠` est la valeur à attribuer à `l𝑎𝑡𝑜𝑚`.

CAS est vérifié à 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.


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

(Regarder l'image ci-dessus )

## Evaluation and case studies
Dans ce chapitre sont décrit 6 cas de tests différents et comment ReffinedC arrive a les traiter.
Le tableau de la Fig.7 résume tout très bien :

## Related Work
Dans ce paragraph nous allons voir les projets alternatifs à **RefinedC** et pourquoi cette téchno est bien meilleure que les autres :

Il exists plusieurs projets nés dans les dernières années ayant plus ou moins le
même objectif que **RefinedC**:

- **Badrock** est basé sur un langage similaire à assembly differemment de `RefinedC`qui s'applique au code C existant qui peut être compilé à l'aide de compilateurs C optimisants disponibles dans le commerce.
**Bedrock** contrairement à **RefinedC** qui exploite les abstractions de plus haut niveau d'un système de types raffinés pour piloter l'automatisation, encode les spécifications et les prédicats abstraits dans une logique de séparation simple dont le format des hints est moins expressif que Lithium. De plus, à la différence des règles de typage de RefinedC, les indices de **Bedrock** ne peuvent pas être liés à des constructions de programme spécifiques et, par conséquent, ne peuvent pas être dirigés par la syntaxe du programme.

- **VST** est un framework basé sur la logique de séparation pour la vérification des programmes.
Les utilisateurs de **VST** déploient un ensemble de tactiques semi-automatiques pour construire des preuves de correction fonctionnelle dans Coq, ou un front qui utilise l'annotation du code source.
Cependant, dans les deux cas, l'utilisateur doit guider manuellement la preuve en effectuant des distinctions de cas, en appliquant des lemmes, en dépliant des prédicats et en instanciant des quantificateurs existentiels - des tâches que l'automatisation basée sur Lithium de RefinedC gère automatiquement dans la plupart des cas.

- Vérification foundamentelle? (foundational) 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 ou les variables locales</li> </ul> |
| **CertiKOS** | Preuve de la correction d'un noyau de système d'exploitation concurrent polyvalent avec verrouillage à grain fin. La vérification de CertiKOS est intégrée au compilateur C, de sorte que la preuve s'applique au code d'assembly 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 téchnologie | En RefinedC
| ------------ | ---------- | ---
| **VCC** | utilise des solveurs SMT 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>permet la surcharge basée sur le type</li> <li>bénéficie également des bibliothèques Coq existantes comme std++ par exemple l'arbre de recherche binaire (search binary tree layered de la figure ci-dessus 7) 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>basé sur le framework K et la logique de correspondance</li> <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 <mark>Coq</mark>, 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. Une approche populaire consiste à combiner des vérifications statiques et dynamiques pour renforcer la sécurité des programmes C. 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 . La charge d'annotation est faible,<mark> l'objectif est uniquement la sécurité de la mémoire</mark>. RefinedC vise une vérification fonctionnelle complète, et nécessite donc plus d'annotations mais peut également vérifier plus de programmes. Cependant, ces langages reposent sur des vérifications à l'exécution et, contrairement à RefinedC, ne peuvent pas garantir la correction fonctionnelle.

- Vérification fondamentale des algorithmes concurrents à grain fin
- Il existe une abondance de travaux connexes sur la vérification fondamentale des algorithmes concurrents à grain fin en utilisant des preuves interactives, par exemple, dans FCSL, VST, et Iris
- Dans les travaux futurs, les chercheurs essayerons d'étudier si développer des types autres que le type booléen atomique qui permettraient la vérification automatique d'algorithmes concurrents plus sophistiqués est possible.

- 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 utilise des types d'alias de type Mezzo au lieu des durées de vie et des références mutables de Rust
- 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

## Limitations and Future Work
Ses limitations et ses évolutions sont :
- Le fait qu'un certain nombre d'élément présent en C ne sont pas pris en compte par ReffinedC (entre autre a cause de Caesium qui ne prend pas tout C en compte) et des améliorations sont en cours de développement en ce sens
- Amlériorer encore les automatismes et les evars (?)
- Liveness properties. (là j'ai pas compris)

Tous les cas sont ensuite détaillés sur la diapo 11
# Plan de synthèse
Expliquer la question, pourquoi elle est importante et comment on a réussi a y répondre

## Glossaire
- **Preuve fondamentale :**
- **Preuve automatique :**
## Contexte
### Importance de la question

## Comment ils ont répondu à la question
### Les annotations
### Les Specs
### Caesium
### Lithium

## Résultats

## Travaux liés

## Perspective et limite
RefinedC, malgré l'automatisation efficace de la vérification du code C, reste un outil novice et par conséquent présente un certain nombre de limitations que les auteurs prevoient d'implementer 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 .Le premier point est principalement une question d'ingénierie puisque des bibliothèques mécanisées pour la sémantique des virgules flottantes existent, tandis que le second nécessite plus de recherche pour trouver la bonne sémantique.
- RefinedC s'appuie sur l'égalité syntaxique, et non sémantique, des pointeurs (voir le cas de Lithium. Cela suffit dans de nombreux cas parce que RefinedC est conçu de sorte que le calcul du même pointeur deux fois (par exemple, en prenant l'adresse du même champ deux fois) donne le même pointeur syntaxiquement. Cependant, certains codes C, en particulier ceux qui utilisent des castings entiers-pointeurs (qui ne sont pas actuellement gérés par RefinedC), ne sont pas pris en compte.
- RefinedC ne supporte pas actuellement le raisonnement sur les appels de fonctions externes et le comportement entrée-sortie des programmes. Nous pensons que l'automatisation fournie par Lithium peut également être utile pour une telle vérification des entrées-sorties.

# Plan de l'oral
## Contexte
1 A
## présentation de l'outil
### ReffinedC
1 T
### Caesium
1 T
### Lithium
1 T
### Règle de typage
1 A
## présentation des résultats
### Métrique
1 T
### Les cas
1 T
## Travaus liés
1 A
## Conclusion
1 A | T