\documentclass[titlepage,a4,landscape]{slides}
\usepackage{isolatin1}
\usepackage{epsf}

\newcommand\titre[1]{{\large\bf {#1}}}

\title{Sécurité du code mobile : \\ problèmes et approches}
\author{François Rouaix  \\
INRIA Rocquencourt \\
Projet Cristal}
\date{Février 1997}

\begin{document}
\maketitle

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Plan}

\begin{itemize}
\item Terminologie, applications
\item Définition de la sécurité
\item Approches pour les systèmes d'applets
\item Java, ActiveX
\item Sémantique de la mobilité, Perspectives
\end{itemize} 
\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Terminologie}
\begin{description}
\item[code mobile:] programme, partie de programme ou processus, déplacé ou se déplaçant sur le réseau

\item[applet (Java):]
petit programme inerte, résidant sur un serveur, téléchargé
et exécuté dans un client (navigateur Web)

\item[agent mobile (Telescript):]
programme se promenant sur le réseau au cours de son
exécution (recherche d'informations, transactions)
\end{description}

{\em agent:}
programme résidant sur un client, qui interroge des serveurs à travers 
le réseau
\end{slide}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Applications}

{\bf Documents web interactifs (applets):}
\small{
\begin{itemize}
\item faiblement interactifs: animations programmées
\item programmes éducatifs, animation d'algorithmes
\item visualisation scientifique, simulation
\item outils de productivité (portfolio)
\item applications client-serveur, logiciels collaboratifs
\end{itemize} 
}

{\bf Distribution de logiciels complets(NC)}

{\bf Agents:}
\small{
\begin{itemize}
\item recherche d'information dans les bases de données
\item lieux de rencontres pour les transactions (financières, petites
 annonces, réservations, commerce électronique)
\end{itemize} 
}

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Contraintes pour un système d'applets}
\begin{list}{\labelitemi}{\itemsep 0cm}
\item portabilité (machines et systèmes d'exploitation)
\item performances
\item champ d'application (environnement d'exécution)
\item {\bf sûreté et sécurité}
\item évolutivité (changements de version)
\item calcul distribué
\end{list} 

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Sécurité}

{\bf Politique de sécurité:}\\
{\small description de ce qui est ou n'est pas autorisé pour le code étranger :
entrées/sorties réseau ou fichiers, interactions avec l'environnement d'exécution (OS ou navigateur).}\\
Actuellement : simpliste; chaque applet est considérée isolément.

{\bf Moyens pour garantir la conformité 
à la politique de sécurité:}\\
{\small modèle du bac à sable : {\em confiner} le code étranger
\begin{list}{\labelitemi}{\itemsep 0cm}
\item environnements d'exécution spécialisés
\item tests à l'exécution
\item propriétés de typage 
\end{list}

}

{\bf Objectif:}\\
Étude formelle des moyens pour {\bf prouver} qu'ils garantissent la politique de sécurité
\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Approches}

\begin{itemize}
\item OS, Fault isolation \\
Couche intermédiaire entre l'OS et l'application, similaire à la protection mémoire (Colusa)

\item Propriétés ou implémentation des langages \\
{\small 
\begin{itemize}
\item code source testé à l'exécution (Perl, Tcl, Python)
\item code compilé testé au chargement (Java)
\item code compilé signé (Caml, ActiveX)
\item code auto-certifié (Oberon, {\em SCC à CMU}, {\em BULL/INRIA Dyade VIP})
\end{itemize}
}
\end{itemize}
\end{slide}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Code source}

\begin{list}{}{\labelwidth 5cm \leftmargin 5cm \itemsep 0cm}

\item[{\bf Principe}]
Le code mobile est un programme quelconque. Sur le client, un interprète
spécialisé en fonction de la politique de sécurité vérifie chaque instruction
lors de l'exécution du programme.
\item[{\bf Exemples}] 
Perl ({\em Penguin}), Tcl ({\em Surfit, Plugin Tcl, Safe mail}),
Python ({\em Grail})
\item[{\bf Analyse}] 
{\small
\begin{list}{}{\itemsep 0cm}
\item[{\tt +}] le client décide de la quantité de tests
\item[{\tt -}] non confidentialité du source
\item[{\tt -}] performances (interprétation, tests)
\item[{\tt -}] multiplication des coûts de vérification
\item[{\tt -}] formalisation de la sécurité par tests (statique / dynamique)
\end{list}
}
\end{list}


\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Code compilé analysé au chargement}

\begin{list}{}{\labelwidth 5cm \leftmargin 5cm \itemsep 0cm}

\item[{\bf Principe}] Le client procède à une analyse du code avant de le charger et de l'exécuter.
\item[{\bf Exemples}]  Java
\item[{\bf Analyse}] 
{\small
\begin{list}{}{\itemsep 0cm}
\item[{\tt +}] le client décide de la quantité de vérification
\item[{\tt +}] aucune hypothèse sur l'origine du code
\item[{\tt -}] difficulté de l'analyse au niveau bytecode/code natif
\item[{\tt -}] aucune hypothèse sur l'origine : mêmes droits minimaux pour tout le monde
\end{list}
}
\end{list}

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Code signé}

\begin{list}{}{\labelwidth 5cm \leftmargin 5cm \itemsep 0cm}

\item[{\bf Principe}] Les propriétés de sécurité sont {\em affirmées} par l'auteur du code (de la signature). Le client décide d'accepter le code en fonction de la confiance accordée à l'auteur.
\item[{\bf Exemples}]  Caml ({\em MMM}), ActiveX ({\em Microsoft})
\item[{\bf Analyse}] 
{\small
\begin{list}{}{\itemsep 0cm}
\item[{\tt +}] faible coût de vérification (signature)
\item[{\tt +}] évolutivité (langage, analyse)
\item[{\tt +}] flexibilité (authentification de l'origine)
\item[{\tt -}] infrastructure de certification
\item[{\tt -}] non vérifiabilité des propriétés de sécurité par le client
\end{list}
}
\end{list}

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Code auto-certifié}

\begin{list}{}{\labelwidth 5cm \leftmargin 5cm \itemsep 0cm}

\item[{\bf Principe}] Le code voyage avec une preuve de ses propriétés de
sécurité. Le client 
vérifie cette preuve sur le code, et décide de l'accepter en fonction de la
conformité à la politique de sécurité choisie.

\item[{\bf Exemples}]  Oberon ({\em Juice}), {\em CMU, VIP}
\item[{\bf Analyse}] 
{\small
\begin{list}{}{\itemsep 0cm}
\item[{\tt +}] coût de la preuve supporté par l'auteur
\item[{\tt +}] flexibilité dans la spécification des propriétés, de la politique de sécurité
\item[{\tt +}] vérification par le client
\item[{\tt -}] difficulté de la spécification des propriétés
\item[{\tt -}] difficulté de l'établissement des preuves
\end{list}
}
\end{list}
\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Rôle du typage}

Analyse statique des programmes

\begin{list}{}{\labelwidth 5cm \leftmargin 5cm \itemsep 0cm}
\item[{\bf Propriétés}] 
{\small\begin{list}{\labelitemi}{\itemsep 0cm}
\item intégrité de la mémoire
\item contrôle de l'environnement d'exécution (portée lexicale)
\end{list}}


\item[{\bf Difficultés}]
{\small \begin{list}{\labelitemi}{\itemsep 0cm}
\item Édition de liens compatible avec la compilation 
séparée (et donc le typage de chaque unité)
\item Ne traite pas les systèmes de {\em droits d'accès}, pour les politiques de sécurité variables
\item Typage du source ou du code compilé ? 
\begin{description}
\item[Java] Typage du bytecode, pas de formalisation disponible
\item[Caml] Typage du source (comme pour les programmes normaux) + signature
\item[Oberon] Code intermédiaire explicitement typé; formalisation ?
\end{description}
\end{list}
}

\end{list}



\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Sécurité de Java}
\begin{list}{}{\labelwidth 6cm \leftmargin 6cm \itemsep 0cm}
\item[Principe]
{\small
\begin{itemize}
\item vérification de type sur le bytecode au chargement
\item environnement d'exécution protégé (SecurityManager, ClassLoader,
espaces de noms)
\end{itemize}
}

\item[Problèmes]
{\small
\begin{itemize}
\item  Distance entre la sémantique du typage au niveau bytecode et au niveau source
\item Edition de liens compatible avec le typage (trous connus)
\item Complexité du système de chargement
\end{itemize}
}

\item[Situation]
{\small
\begin{itemize}
\item Pas de formalisation (tentatives en cours)
\item Système de chargement dépendant du vendeur
\item Trous connus : pas de sécurité garantie
\item Système de signature de code
\end{itemize}
}
\end{list}

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{ActiveX}

Qu'est ce ? OLE + HTTP (+ DCOM ?)

Sécurité ?
\begin{itemize}
\item code binaire
\item signature (CA)
\item quel modèle pour les communications inter-processus ?
\end{itemize} 

Aucun élément aujourd'hui.

\end{slide}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Sémantique de la mobilité}
\begin{description}
\item[Limite des Applets] \mbox{}\\
Code {\bf mort}. N'intègre pas la mobilité ou la distribution.

\item[Vrai code mobile]\mbox{}
{\small
\begin{itemize}
\item le code {\em vivant} se déplace
\item distribution et mobilité {\bf intégrés} dans la sémantique du langage
\item possibilité de raisonner sur les programmes mobiles
\end{itemize}
}

\item[Travaux] \mbox{}
{\small
\begin{itemize}
\item Obliq (Luca Cardelli, DEC SRC)
\item Join-calculus (Projet Para, INRIA Rocquencourt)
\end{itemize}
}
\end{description}


\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\titre{Perspectives pour le Web}

Constat pessimiste sur la situation actuelle
\begin{itemize}
\item calcul distribué: programmation de bas-niveau
\item approche ad-hoc de la sécurité (cf. Unix)
\item mise en oeuvre des outils (Java, Telescript) peu convaincante
\item manque de sérénité
\end{itemize}

\end{slide}
\end{document}

