|
Sécurité
des logiciels et des contenus
Ecole
chercheurs 2008 - Liffré
Irisa
- 28 au 30 janvier 2008
Du 28 au 30 janvier 2008,
à Liffré, l'école chercheurs, organisée
dans le cadre de la formation permanente de l'Irisa, a eu pour thème
la sécurité des logiciels et des contenus. Les exposés
qui suivent retracent la diversité des problématiques
à l'oeuvre dans ce domaine.
Certains intervenants ne
souhaitant pas voir leur exposé diffusé en externe,
vous trouverez l'ensemble
des présentations de l'école chercheurs 2008 sur l'intranet
de l'Irisa.
Avant-propos:
Dans le cadre de la formation
permanente de l'Irisa, la notion d'école chercheurs a été
mise en place pour permettre à des chercheurs de suivre une
formation dans un domaine qu'ils ne connaissent pas et pour lequel
ils ont un attrait scientifique. Le but est, pour un thème
fixé, de faire découvrir ce sujet à des chercheurs
qui souhaitent acquérir des compétences transversales
à leur domaine de recherche.
La première école
chercheurs a eu pour thème le "data Mining" (non
enregistrée). La deuxième, en 2004, a porté sur
le "Traitement
du Signal". La troisième, en 2005, a porté
sur la Bio-Informatique
; enfin, en 2006, la quatrième école chercheurs a porté
sur "Algorithmes
et systèmes répartis".
Les
exposés scientifiques
- Thomas Genet,
enseignant-chercheur à l'Irisa (équipe Lande)
Protocoles cryptographiques
et vérification logique
Résumé:
Nous utilisons tous quotidiennement des protocoles cryptographiques,
et ce sans même le savoir. Il faut dire que, malgré leurs
noms barbares, ils sont indolores. En revanche, si la sécurité
de ces protocoles est mise en défaut, et pour peu qu'un fraudeur
rôde, cela peut faire très mal à notre portefeuille.
Un protocole cryptographique est une succession d'échanges
de messages chiffrés par des méthodes cryptographiques.
De façon assez surprenante, il n'est généralement
pas nécessaire de comprendre tous les détails des algorithmes
de chiffrement pour saisir l'essence d'un protocole cryptographique.
A titre d'exemple, nous verrons un protocole que nous utilisons tous
régulièrement, le paiement par carte bancaire. Ce protocole
servira également à illustrer les différents
types d'attaques (logiques/cryptographiques) sur ces protocoles, ainsi
que les parades successives développées par les sociétés
de paiement par carte.
Nous verrons quels
sont les usages dans le monde industriel et dans le monde académique
pour modéliser et vérifier ce type de protocoles. Du
point de vue académique, on s'intéressera aux outils
de modélisation formelle et de vérification automatique.
Cette famille de techniques permet, à partir d'une description
formelle d'un protocole, de débusquer automatiquement les attaques
logiques lorsqu'elles existent et, dans le cas contraire, de prouver
leur absence. La puissance et la simplicité d'utilisation de
ces techniques de vérification formelle explique, en grande
partie, l'intérêt grandissant que lui porte l'industrie.
Avec des outils simples, il est également possible d'entrelacer
les étapes de conception, de modélisation et de vérification
formelle. Ceci permet de détecter automatiquement, pendant
la conception d'un protocole, les failles logiques potentielles, de
les corriger et de prouver que la correction est effective.
- protocoles
cryptographiques et exemples [37:09]
 la vidéo
(version Smil - transparents synchronisés)
- méthodes
formelles pour les protocoles cryptographiques [26:11]
la vidéo
(version Smil - transparents synchronisés)
- transfert
industriel des outils de vérification formelle [32:29]
la vidéo
(version Smil - transparents synchronisés)
les transparents
(pdf)
- Philippe Darrondeau,
directeur de recherche à l'Irisa (équipe S4)
Secrets concurrents
(étude effectuée avec Eric Badouel, Marek
Bednarczyk, Andrzej Borzyszkowski et Benoît Caillaud)
Résumé:
Etant donné un système d'états fini, un ensemble
d'observateurs partiels et pour chacun d'eux, un ensemble régulier
de trajectoires du système , capable de protéger les
secrets contre des observateurs connaissant ce contrôle. Nous
montrons qu'il existe toujours un contrôle optimal mais qu'il
n'est pas nécessairement régulier. Nous donnons des
conditions suffisantes pour le calcul de contrôleurs finis optimaux
protégeant les secrets concurrents.
-
la vidéo
[55:41] (version Smil - transparents synchronisés)
les transparents
(pdf)
- Caroline Fontaine,
chargée de recherche à l'Irisa (équipe Temics)
Sécuriser
la diffusion des documents multimédia grâce à
la dissimulation d'information?
Résumé:
La dissimulation d'information dans les documents multimédia
intervient comme un complément de techniques et outils plus
classiques tels la cryptographie. Elle peut prendre plusieurs formes,
selon les objectifs visés:
- stéganographie,
lorsqu'on recherche avant tout la furtivité.
- tatouage,
lorsque l'application requiert une robustesse maîtrisée
(protection du droit d'auteur, authentification, intégrité).
- fingerprinting,
lorsque l'on souhaite pouvoir tracer les différentes copies
diffusées.
Dans tous les
cas, différentes contraintes doivent être gérées
simultanément, avec des compromis adaptés: imperceptibilité,
robustesse, capacité (longueur du message transmis), sécurité.
Ces techniques
ont tout d'abord été discutées et présentées,
cette introduction étant illustrée par quelques exemples
de techniques d'insertion.
On a discuté
ensuite de l'étude récente de leur sécurité,
à la fois sur un plan théorique et sur un plan pratique.
0n a vu notamment que s'il est tentant d'établir un parallèle
avec la cryptographie, celui-ci est parfois justifié mais parfois
très hasardeux.
- Loïc Hélouët,
chargé de recherche à l'Irisa (équipe DistribCom)
 Non-interférence
et canaux cachés
Résumé:
Cet exposé aborde le thème de l'analyse formelle des
failles de sécurité permettant des fuites d'informations.
Nous avons étudié plus particulièrement deux
types de failles de sécurité: l'interférence
et les canaux cachés.
L'interférence
est le fait de pouvoir déduire par observation certaines données
ou actions qui devraient rester confidentielles. Les canaux cachés
sont des moyens détournés de créer des communications
entre des agents qui ne devraient pas être autorisés
à communiquer, ou qui ne devraient communiquer que par l'intermédiaire
de canaux connus et surveillés.
Nous avons vu
dans un premier temps comment ces failles ont été caractérisées
à partir de modèles comportementaux depuis les années
70. Après ce rapide historique, nous sommes revenus en détail
sur la propriété de non-interférence introduite
par Goguen et Messeger, qui est l'une des manières les plus
classiques et les plus populaires de caractériser formellement
une faille de sécurité. Nous avons vu sur un modèle
simple comment cette propriété peut être définie
en termes d'équivalence(s) de comportements. Nous avons vu
ensuite les problèmes posés par la non-interférence,
les limites de l'approche, et pourquoi la sévérité
d'une interférence varie selon les systèmes et les situations
que l'on considère.
Nous avons ensuite
étudié la formalisation d'un autre type de faille de
sécurité, à savoir les canaux cachés.
Nous avons montré que contrairement à ce qui est souvent
écrit, canaux cachés et interférence sont deux
propriétés différentes. Nous sommes revenus notamment
pour justifier cela sur la notion de quantité d'information
transmise sur un canal, ainsi que sur la notion de dynamicité,
qui sont absentes des définitions classiques de la non-interférence.
Pour terminer
cet exposé, nous avons montré une approche basée
sur la théorie des jeux qui permet de tenir compte de l'aspect
dynamique des canaux cachés, et avons évoqué
plusieurs pistes de recherche dans cette direction.
- Introduction
et Sécurité multi-niveaux [22:25]
la vidéo
(version Smil - transparents synchronisés)
- Non interférence
[43:44]
la vidéo
(version Smil - transparents synchronisés)
- Canaux cachés
[30:58]
la vidéo
(version Smil - transparents synchronisés)
les transparents
(pdf)
- David Pichardie,
chargé de recherche à l'Irisa (équipe Lande)
Proof carrying code:
a quick tour
- Motivations
[11:42]
la vidéo
(version Flash)
- Seminal work
[22:39]
la vidéo
(version Flash)
- L'interprétation
abstraite [13:02]
la vidéo
(version Flash)
les transparents
(pdf)
Retour
vers l'ensemble des exposés scientifiques de la vidéothèque
de l'Irisa
 Pour
lire les présentations audio/vidéo vous devez disposer
de RealPlayer.
Vous pouvez télécharger une version gratuite sur le
site de Real
(c)
pôle audiovisuel de l'Irisa
(février 2008)
|
"Analyse
statique pour la sécurité"