Participants

IRCCyN (Nantes)

IRISA (Rennes)

LaBRI (Bordeaux)

LAMSADE (Paris)

LSV (Cachan)

Didier Lime

Ordre du jour

Contrôle de non-interférence (Franck Cassez).
Franck presente un problème de synthèse de controleur. L'idée est de synthétiser un contrôleur permettant d'eviter les comportements interférents, dans un cadre non temporisé. La définition d'interférence reprend des définitions inspirées des travaux de Focardi et Gorrieri.
Un ensemble d'actions sont classées comme "high", d'autres comm "low". Dans un système non-interférent, un utilisateur "low" ne peut observer que des actions de type "low", et ne doit pas pouvoir inférer les actions "high" qui se sont produites à partir de ses obsevrations.
La non interférence s'exprime comme un propriété d'équivalence des langages de deux systèmes:
L(A/Sigma_c) "=" L(A\Sigma_c) où
- A est le système considéré
- Sigma_c est l'ensemble des actions de type "high"
- A/Sigma_c est le système A dans lequel les actions de type "high" sont remplacées par des actions silencieuses
- A\Sigma_c est le système A dans lequel les transitions étiquetées par des actions de type "high" sont coupées.
La relation d'équivalence peut être l'équivalence de trace (le système satisfaisant la relation ci-dessus est alors dit SNNI), la bisimulation faible (le système satisfaisant la relation ci-dessus est alors dit BSNI).
Verifier SNNI est en PSpace, BSNI en Ptime.
Le problème posé ici est de trouver le controleur maximal C tel que CxA devienne SNNI (resp. BSNI). Cela revient à trouver un controleur pour A tel que les executions controlées de A satisfassent une formule phi dérivée de A\Sigma_c. On retombe alors sur un problème de controle classique.
D'autres relations d'équivalence existent: BNDC (Non disclosure on Composition), qui impose qu'un système reste non-interférent même lorsqu'il est composé avec un autre. C'est une propriété très forte: on peut être BSNI mais pas BNDC.
Les extensions naturelles de ce travail sont : étude avec d'autres relations d'équivalence, ou avec des modèles temporisés.
Controlling timed non-interference (Didier Lime).
L'objectif est de trouver un controleur qui permette d'éviter les interférences dans un systèmes temporisé.
Un système dont les comportements ne semblent pas interférents lorsqu'on abstrait le temps peut devenir interférent à cause du temps. Exemple (si l est tirable à la date t, cela signifie que l a été tiré depus un état s, accessible uniquement en tirant h).
Les règles du jeu sont les suivantes: trouver un controleur maximal C qui garantisse que le systeme CxA soit non interférent. C n'a pas le droit de bloquer le temps. Un tel controleur n'existe pas toujours, mais on sait décider s'il existe.
Différentes complexités selon les systèmes que l'on considère et les relations. On peut ainsi demander que le système soit déterministe, déterministe sur les actions high, low, etc.
Covert channels detection : using games with scenarios (Loïc Hélouët).
L'idée de ce travail est de trouver un moyen de faire passer un flot d'information (canal caché) à partir d'une spécification d'un système infini et asynchrone. La decription du système est donnée sous forme d'automates d'ordres (ou MSCs).
Ces automates sont transformés en arènes, et il existe un jeu pour lequel l'existence d'une stratégie gagnante implique l'existence d'un canal caché entre deux processus (émetteur et récepteur). Les canaux cachés détectés par ce jeu utilisent les choix d'un utilisateur pour coder de l'information. Les conséquences causales de ces choix sont observées par le récepteur du canal.
Le jeu présente ci-dessus peut être considéré comme un jeu discret, i.e chaque choix code un nombre entier de bits envoyés sur le canal. Des travaux sont en cours pour envisager le problème sous l'angle de la théorie de l'information. Il y a canal caché si l'information mutuelle entre ce que fait un utilisateur du système et ce qu'observe un autre n'est pas nulle. Cette notion devrait également permettre de quantifier l'importance des fuites.
Des travaux similaires sur d'autres modèles comme les automates communicants ont été effectués durant le stage de Master d'Aldric Degorre.
Discussion.
Il y a une différence entre les aproches présentées le matin BSNI, SNNI, timed ou untimed et l'après midi (MSCs + jeux). Au dela des modèles qui changent, c'est le type de propriété que l'on cherche à prouver qui diffère.
- Dans le premier cas, on cherche à montrer que le système modélisé ne laisse filtrer aucune information confidentielle (ie pas un seul bit), tandis que dans le deuxième cas, on veut montrer la vulnérabilité du système à un type particulier d'attaque.
- Dans le premier cas, la fuite d'un seul bit d'information suffit à considérer le système comme interférent, tandis que la deuxième approche regarde l'itération d'interférences.
- Enfin, dernière différence: dans le premier cas, la fuite d'information peut être accidentelle, alors que dans le cas des canux cachés, la fuite d'information est voulue: soit deux utilisateurs du système sont corrompus, soit un cheval de troie a été intégré au système pour transmettre de l'information.

Décisions

Faire un site web sur le sujet de la non-interférence dans le projet DOTS (Loïc).
Essayer de faire converger les deux approches (tous). Point de départ possible, le travail de Master d'Aldric Degorre, qui part d'automates et utilise la logique ATL pour caractériser les canaux cachés.

Prochaine réunion

Date à fixer lors de la prochaine réunion plénière du projet DOTS (à la rentrée), et en tout cas avant la fin de l'année.

Bibliography

	[BC01]	Gérard Boudol and Ilaria Castellani. Noninterference for Concurrent Programs. In ICALP'01, vol. 2076 of LNCS, p. 382-395. Springer, 2001.
	[CHM04]	David Clark, Sebastian Hunt, and Pasquale Malacaria. Quantified Interference: Information Theory and Information Flow (Extended Abstract). In WITS'04, Barcelona (Spain), 2004.
	[Deg05]	Aldric Degorre. Caractérisation des canaux cachés en logique temporelle alternante. Masters thesis, IRISA & ENS Cachan, 2005.
	[FG01]	Riccardo Focardi and Roberto Gorrieri. Classification of Security Properties (Part I: Information Flow). In FOSAD'00, vol. 2171 of LNCS, p. 331-396. Springer, 2001.
	[McL90]	John McLean. Security Models and Information Flow. IEEE Symposium on Security and Privacy, p. 180-189. IEEE Comp. Soc. Press, 1990.
	[SM03]	Andrei Sabelfeld and Andrew C. Myers. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications 21(1):5-19, 2003.
	[VSI96]	Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A Sound Type System For Secure Flow Analysis. Journal of Computer Security 4(3):167-187, 1996.

Page maintenue par Nicolas Markey.
Dernières modifications : 22 juin 2009.