212 lines
11 KiB
Markdown
212 lines
11 KiB
Markdown
## Allow List over PC
|
||
|
||
### Modele
|
||
|
||
**Base de Mathieu**
|
||
|
||
Soit $\\Pi$ l'ensemble des processus $p_1, ... p_N$
|
||
$\\Pi_M \\subseteq \\Pi$ les processus autorisés à $APPEND(x)$
|
||
$\\Pi_V \\subseteq \\Pi$ les processus autorisés à $PROVE(x)$
|
||
|
||
Chaque processus est séquentiel mais le système est asynchrone (le $\\Delta$ de vitesse d'horloge relative est inconnue par les processus) Le système est crash prône
|
||
|
||
Tous les processus ont un identifiant et les IDs sont connues de tous les processus.
|
||
|
||
**Spécificité Message-Passing**
|
||
|
||
2 opérations possibles:
|
||
|
||
- $send(O, p_i)$
|
||
- $recv(O, p_i)$
|
||
|
||
$H$ l'ensemble des séquences d'opérations $H|p_i$ les opérations relatives à $p_i$ $H|x$ l'ensemble des séquences d'opérations relatives à l'objet $x$ Les processus peuvent être byzantin en ne suivant pas le protocole définit. On admet que la transmission des message respecte les propriétés de reliable broadcast. C'est a dire que tous les messages envoyés sont reçu par tous. Et que pour deux message envoyé dans un ordre précis par un même processus ils seront reçu dans ce même ordre par tous les autres processus.
|
||
|
||
### Problematique
|
||
|
||
$O$ ensemble des types d'opérations :
|
||
|
||
- $APPEND(x)$
|
||
- $PROVE(x)$
|
||
- $READ()$
|
||
|
||
On veut remplir les propriétés suivantes :
|
||
|
||
- Termination: toutes les opérations terminent par un "return"
|
||
- APPEND validity: Un APPEND(x) est valide ssi $\\forall p_i$ t.q. $send(APPEND(x)) \\in H| p_i$. $p_i \\in \\Pi_M \\subseteq \\Pi$
|
||
- PROVE validity: Un PROVE(x) est valide ssi $\\forall p_i$ t.q. $send(PROVE(x)) \\in H| p_i$. $p_i \\in \\Pi_V \\subseteq \\Pi$ ET un $APPEND(x)$ apparait dans $\\Pi_V$
|
||
- Progress: si un $APPPEND(x)$ est valide alors il exist $\\forall p_i$ un point dans $H|p_i$ tel que tous les $PROVE(x)$ sont valident.
|
||
- READ validity: $\\forall p_i$ l'opération $READ()$ doit retourner toutes les opérations $PROVE(...) \\in H|p_i$
|
||
|
||
### Algo
|
||
|
||
```
|
||
appends a set of objetcs
|
||
proves a set of tuples of (objetc, process id)
|
||
|
||
recv(APPEND(x), p_j)
|
||
if p_j \in \Pi_M
|
||
appends += x
|
||
return
|
||
|
||
recv(PROVE(x), p_j)
|
||
if p_j \in \Pi_V
|
||
if x \in appends
|
||
proves += (x, p_j)
|
||
return
|
||
|
||
APPEND()
|
||
if p_i \in \Pi_V
|
||
appends += x
|
||
send(APPEND(x), p_i)
|
||
return
|
||
|
||
PROVE(x)
|
||
if p_i \in \Pi_M
|
||
if x \in appends
|
||
proves += (x, p_i)
|
||
send(PROVE(x), p_i)
|
||
return
|
||
|
||
READ()
|
||
return proves
|
||
```
|
||
|
||
### Preuve
|
||
|
||
**Termination**
|
||
|
||
Toutes les fonctions sont séquentiels et synchrones. Il n'y a aucune boucle, les fonctions terminent forcements.
|
||
|
||
**APPEND Validity**
|
||
|
||
La condition `if p_j \in \Pi_M` dans la fonction APPEND(x) garantit qu'aucun processus légitime ne peut ajouter d’élément dans la whitelist si il n'est pas manageur. Cette même condition dans recv(APPEND(x)) garantit qu'aucun processus légitime n'acceptera d'ajout d'élément soumis par un processus non manageur. Cette garantit repose sur le fait que les identifiants sont infalsifiables.
|
||
|
||
**PROVE Validity**
|
||
|
||
La condition `if p_j \in \Pi_V` dans la fonction PROVE(x) garantit qu'aucun processus légitime ne peut ajouter d’élément dans la whitelist si il n'est pas validateur. Cette même condition dans recv(PROVE(x)) garantit qu'aucun processus légitime n'acceptera d'ajout d'élément soumis par un processus non validateur. Cette garantit repose sur le fait que les identifiants sont infalsifiables.
|
||
|
||
De même la condition `if x \in appends` dans PROVE(x) assure que le processus courant a déjà reçu ou émis lui même un APPEND(x), puisque la seule manière d'ajouter un élément a l’ensemble `appends` est via les fonctions recv(APPEND(x)) et APPEND(x) une fois que les conditions de APPEND Validity sont respectés. De la même manière cette condition dans recv(PROVE(x)) assure qu'une requête PROVE(x) envoyé par un validateur malveillant ne faisant pas suite à un APPEND(x) ne soit pas considéré par les processus légitimes.
|
||
|
||
**PROGRESS**
|
||
|
||
Étant donné que tout message est eventually reçu. Tout APPEND(x) valide sera envoyé via la fonction `send` et sera reçu dans un temps $\\delta t$ par tous les processus. Avec $\\delta t$ étant le temps de transmission le plus long entre deux processus. Cette borne supérieur $\\delta t$ peut etre définit dans un système synchrone en admettant une borne maximal pour la transmission la plus lente entre deux `p`. Assurant ainsi que chaque APPEND(x) valide sera considéré par l'ensemble du système à $t + \\delta t$.
|
||
Cependant dans un système asynchrone ce $\\delta t$ est par définition non définit, rendent la propriété de PROGRESS insatisfaisable.
|
||
|
||
**READ Validity**
|
||
|
||
Pour ce point il convient de démontrer que tout tuple dans proves se trouve bien dans $\\forall PROVE(..) \\in H|p_i$ tel que $p_i$ le processus invoquant le READ. L'ajout a l'ensemble proves dépend des fonctions PROVE() et recv(PROVE()).
|
||
Dans ces deux fonctions on assure déjà la validité des PROVE pour $p_i$. Tout PROVE valide reçu ou émis par p_i est donc ajouté dans proves, ce qui correspond bien aux opérations proves de $H|p_i$.
|
||
|
||
## Deny List over PC
|
||
|
||
### Modele
|
||
|
||
__Base de Mathieu__
|
||
|
||
Soit $\\Pi$ l'ensemble des processus $p_1, ... p_N$
|
||
$\\Pi_M \\subseteq \\Pi$ les processus autorisés à $APPEND(x)$
|
||
$\\Pi_V \\subseteq \\Pi$ les processus autorisés à $PROVE(x)$
|
||
|
||
Chaque processus est séquentiel mais le système est asynchrone (le $\\Delta$ de vitesse d'horloge relative est inconnue par les processus) Le système est crash prône
|
||
|
||
Tous les processus ont un identifiant et les ids sont connues de tous les processus.
|
||
|
||
**Spécificité Message-Passing**
|
||
|
||
2 opérations possibles:
|
||
|
||
- $send(O, p_i)$
|
||
- $recv(O, p_i)$
|
||
|
||
$H$ l'ensemble des séquences d'opérations $H|p_i$ les opérations relatives à $p_i$ $H|x$ l'ensemble des séquences d'opérations relatives à l'objet $x$ Les processus peuvent être byzantin en ne suivant pas le protocole définit. On admet que la transmission des message respecte les propriétés de reliable broadcast. C'est a dire que tous les messages envoyés sont reçu par tous. Et que pour deux message envoyé dans un ordre précis par un même processus ils seront reçu dans ce même ordre par tous les autres processus.
|
||
|
||
### Problématique
|
||
|
||
$O$ ensemble des types d'opérations :
|
||
|
||
- $APPEND(x)$
|
||
- $PROVE(x)$
|
||
- $READ()$
|
||
|
||
On veut remplir les propriétés suivantes :
|
||
|
||
- Termination: toutes les opérations terminent par un "return"
|
||
- APPEND validity: Un APPEND(x) est valide ssi $\\forall p_i$ t.q. $send(APPEND(x)) \\in H| p_i$. $p_i \\in \\Pi_M \\subseteq \\Pi$
|
||
- PROVE validity: Un PROVE(x) est __invalid__ ssi $\\forall p_i$ t.q. $send(PROVE(x)) \\in H| p_i$. $p_i \\in \\Pi_V \\subseteq \\Pi$ ET un $APPEND(x)$ apparait dans $\\Pi_V$
|
||
- PROVE Anti-Flickering: Si une opération PROVE(x) invalide est soumise ou recu par un processus alors toutes les opérations PROVE(x) futur seront invalides
|
||
- READ validity: $\\forall p_i$ l'opération $READ()$ doit retourner toutes les opérations $PROVE(...) \\in H|p_i$
|
||
|
||
### Algo
|
||
|
||
```
|
||
appends a set of objetcs
|
||
proves a set of tuples of (objetc, process id)
|
||
|
||
recv(APPEND(x), p_j)
|
||
if p_j \in \Pi_M
|
||
appends += x
|
||
return
|
||
|
||
recv(PROVE(x), p_j)
|
||
if p_j \in \Pi_V
|
||
if x \neg\in appends
|
||
proves += (x, p_j)
|
||
return
|
||
|
||
APPEND()
|
||
if p_i \in \Pi_V
|
||
appends += x
|
||
send(APPEND(x), p_i)
|
||
return
|
||
|
||
PROVE(x)
|
||
if p_i \in \Pi_M
|
||
if x \neg\in appends
|
||
proves += (x, p_i)
|
||
send(PROVE(x), p_i)
|
||
return
|
||
|
||
READ()
|
||
return proves
|
||
```
|
||
|
||
### Preuve
|
||
|
||
**Termination**
|
||
|
||
Toutes les fonctions sont séquentiels et synchrones. Il n'y a aucune boucle, les fonctions terminent forcements.
|
||
|
||
**APPEND Validity**
|
||
|
||
La condition `if p_j \in \Pi_M` dans la fonction APPEND(x) garantit qu'aucun processus légitime ne peut ajouter d’élément dans la whitelist si il n'est pas manageur. Cette même condition dans recv(APPEND(x)) garantit qu'aucun processus légitime n'acceptera d'ajout d'élément soumis par un processus non manageur. Cette garantit repose sur le fait que les identifiants sont infalsifiables.
|
||
|
||
**PROVE Validity**
|
||
|
||
La condition `if p_j \in \Pi_V` dans la fonction PROVE(x) garantit qu'aucun processus légitime ne peut ajouter d’élément dans la whitelist si il n'est pas validateur. Cette même condition dans recv(PROVE(x)) garantit qu'aucun processus légitime n'acceptera d'ajout d'élément soumis par un processus non validateur. Cette garantit repose sur le fait que les identifiants sont infalsifiables.
|
||
|
||
De même la condition `if x \neg\in appends` dans PROVE(x) assure que le processus courant n'a pas déjà reçu ou émis lui même un APPEND(x), puisque la seule manière d'ajouter un élément a l’ensemble `appends` est via les fonctions recv(APPEND(x)) et APPEND(x) une fois que les conditions de APPEND Validity sont respectés.
|
||
De la même manière cette condition dans recv(PROVE(x)) assure qu'une requête PROVE(x) envoyé par un validateur malveillant faisant suite à un APPEND(x) ne soit pas considéré par les processus legéitimes.
|
||
|
||
**ANTI-FLICKERING**
|
||
|
||
Étant donné que tout message est eventually reçu. Tout APPEND(x) valide sera envoyé via la fonction `send` et sera reçu dans un temps $\\delta t$ par tous les processus. Avec $\\delta t$ étant le temps de transmission le plus long entre deux processus. Cette borne supérieur $\\delta t$ peut etre définit dans un système synchrone en admettant une borne maximal pour la transmission la plus lente entre deux `p`. Assurant ainsi que chaque APPEND(x) valide sera considéré par l'ensemble du système à $t + \\delta t$.
|
||
Cependant dans un système asynchrone ce $\\delta t$ est par définition non définit, rendent la propriété d'anti-flickring insatisfaisable.
|
||
|
||
__READ Validity__
|
||
|
||
Pour ce point il convient de démontrer que tout tuple dans proves se trouve bien dans l'ensemble $E$, tel que $\\forall e \\in E$, $e = PROVE(x)$ et tel que $H'|p_i$ l'ensemble des opérations reçu et émise avant l'opération $e$, alors $\\nexists e' \\in H'|p_i$ t.q. $e' = APPEND(x)$ avec $p_i$ le processus invoquant le READ.
|
||
L'ajout a l'ensemble proves dépend des fonctions PROVE() et recv(PROVE()). Dans ces deux fonctions on assure déjà la validité des PROVE pour $p_i$. Tout PROVE valide reçu ou émis par p_i est donc ajouté dans proves, ce qui correspond bien aux opérations proves de $H|p_i$.
|
||
|
||
## Discussion
|
||
|
||
Il est impossible d’implémenter une AllowList ou DenyList dans un système asynchrone, ce qui conditionne déjà notre model sur ce point. Les propriétés de PROGRESS et d'ANTIFLICKERING étant directement lié à ce point.
|
||
|
||
Les points facilitant la résolution de notre problème sont d'une part la présence du ReliableBroadcast et d'autre part d'un identifiant infalsifiable. Les deux points étant lié puisque nous pouvons admettre que le reliable broadcast peut aussi s'occuper de l'authentification des messages, et de leur non répudiabilité.
|
||
|
||
Un axe d'amélioration est donc d'affaiblir le reliable broadcast pour ça il faut définir les propriétés essentiels a l’exécution de notre algorithme.
|
||
|
||
### RB
|
||
|
||
- Non répudiabilité (une fois que le message ets envoyé il est impossible pour un processus de le nier)
|
||
- Tout message envoyé est recu par tout le monde(eventual delivery)
|
||
- Immutabilité du message une fois qu'il est émis |