Machine De Marque De Données De Fenton`s

Fenton a créé une machine abstraite appelée la machine de marque de données pour étudier la manipulation des écoulements implicites au temps d'exécution. Chacun variable dans cette machine a eu une classe associée de sécurité, ou l'étiquette. Fenton a également inclus une étiquette pour le compteur de programme (PC).

L'inclusion du PC a permis à Fenton de traiter des écoulements implicites en tant qu'écoulements explicites, parce que les branches sont simplement des tâches au PC. Il a défini la sémantique de la machine de marque de données. Dans la discussion suivante, le saut signifie que l'instruction n'est pas exécutée, push(x, x) signifie pour pousser le x variable et sa classe de sécurité X sur la pile de programme, et pop(x, x) des moyens de sauter la valeur et la classe supérieures de sécurité outre de la pile de programme et de les assigner à x et à x, respectivement.

Fenton a défini cinq instructions. Les rapports entre l'exécution des instructions et les classes des variables sont comme suit.

L'instruction d'incrément

X : = X + 1

est équivalent à

si PC < = x puis x : = X + 1 ; saut 
d'autre

L'instruction conditionnelle
```
si x = 0 puis n goto x d'autre : = X 1  
```
est équivalent à
```
si x = 0 puis {push(PC, PC) ; PC = lub(PC, 
x) ; PC : = n ; } autrement {si PC < = x puis {x : =
X 1 ; } saut d'autre}  
```
Ceci s'embranche, et pousse le PC et sa classe de sécurité sur la pile de programme. (comme à l'accoutumée, le PC est incrémenté de sorte que quand il est sauté, suivre d'instruction si le rapport est exécuté.) Ceci capture le PC contenant l'information de x (spécifiquement, ce x est 0) tout en suivant le goto.
Le retour
```
retour  
```
est équivalent à
```
pop(PC, PC) ;  
```
Ceci renvoie la commande au rapport suivant le bout si rapport. Puisque l'écoulement de la commande serait arrivé à ce rapport, le PC ne contient plus des informations sur x, et la vieille classe peut être reconstituée.
L'instruction de branchement
```
si 'x = 0 puis n goto x d'autre : = X 1  
```
est équivalent à
```
si x = 0 puis {si x < = PC puis {PC : = n ; 
} saut d'autre} autrement {si PC < = x puis {x : = X 1 ; 
} saut d'autre}  
```
Ceci s'embranche sans sauver le PC sur la pile. Si la branche se produit, le PC est dans une classe plus élevée de sécurité que la variable conditionnelle X, ainsi ajouter l'information de x au PC ne change pas la classe du degré de sécurité du PC.
L'instruction de halte
```
halte  
```
est équivalent à
```
si la pile de programme vide stoppent alors 
l'exécution  
```
La pile de programme étant vide s'assure que l'utilisateur ne peut pas obtenir l'information en regardant la pile de programme après que le programme ait stoppé (par exemple, pour déterminer quel si le rapport était pour la dernière fois pris).

EXEMPLE : Considérez le programme suivant, dans lequel x contient au commencement 0 ou 1.

1. si x = 0 puis 4 goto x d'autre : = X 1 2. 
si z = 0 puis 6 goto z d'autre : = halte 3. 4 de z 1. 
z : = z + 1 5. retours 6. y : = y + 1 7. 
retours

Ce programme copie la valeur de x à y. supposent le ce x = 1 au commencement. La table suivante montre le contenu de la mémoire, de la classe de sécurité du PC à chaque étape, et du contrôle correspondant de certification.

X	y	z	PC	PC	pile	contrôle de certification
1	0	0	1	Bas
0	0	0	2	Bas		Bas < = x
0	0	0	6	X	(3, bas)
0	1	0	7	X	(3, bas)	PC < = y
0	1	0	3	Bas

La machine de Fenton manipule des erreurs en les ignorant. Supposez cela, dans le programme ci-dessus, y < = x. Alors à la cinquième étape, le contrôle de certification échoue (parce que PC = x). Ainsi, la tâche est sautée, et à l'extrémité y = 0 indépendamment de la valeur de x. Mais si la machine rapporte des erreurs, le message d'erreur informant l'utilisateur de l'échec du contrôle de certification signifie que le programme a essayé d'exécuter l'étape 6. Il pourrait faire ainsi seulement s'il avait pris la branche dans l'étape 2, signification cette z = 0. Si z = 0, alors la branche d'autre du rapport 1 ne pourrait pas avoir été pris, signification cette x = 0 au commencement.

Pour empêcher ce type de déduction, la machine de Fenton continue de s'exécuter face aux erreurs, mais ignore le rapport qui causerait la violation. Ceci répond aux exigences. Avorter le programme, ou créer une exception évidente à l'utilisateur, ferait également couler l'information contre la politique.

Le problème avec le reportage des erreurs est qu'un utilisateur avec le dégagement inférieur que l'information causant l'erreur peut déduire l'information de savoir qu'il y a eu une erreur. Si l'erreur est entrée une telle manière dont les entrées dans la notation, et l'action de la notation, sont évidentes seulement à ceux qui ont à dégagement proportionné, alors aucune violation de la politique ne se produit. Mais si le dégagement de l'utilisateur est suffisamment haut, alors l'utilisateur peut voir l'erreur sans violation de la politique. Ainsi, l'erreur peut être notée pour l'interface gestionnaire (ou tout autre utilisateur approprié), même si elle ne peut pas être montrée à l'utilisateur qui exécute le programme. Les commentaires semblables s'appliquent à n'importe quelle action d'exception, telle que la fin anormale.

c'est un article supplémentaire par Fred Foster