PARallélisme et SECurité – PARSEC

De nouvelles applications, comme le d´eveloppement de serveurs web, les jeux impliquant un grand nombre
de joueurs ou les applications de stockage de donn´ees `a l'´echelle d'Internet sont, de fa¸con inh´erente,
massivement parall`eles, et ouvertes `a des acteurs ´eventuellement peu fiables. Ces applications n´ecessitent
des techniques de programmation ad´equates et, pour certaines, requi`erent des garanties de s´ecurit´e. Le
mod`ele traditionnel des processus ne convient pas pour ces applications dans lesquelles il y a beaucoup
de partage de donn´ees. Dans les derni`eres ann´ees, on s'est rendu compte que les “threads” mis en oeuvre
dans les syst`emes d'exploitation sont trop limit´es et inefficaces pour fournir un support adapt´e `a ce
type d'applications, et qu'il fallait donc concevoir des syst`emes de “threads” accessibles au niveau de
l'utilisateur. La question de savoir si ce type de programmation doit adopter une discipline pr´eemptive,
ou bien un mod`ele “dirig´e par les ´ev´enements”, ou encore un style coop´eratif, reste encore une affaire de
recherche.
De fa¸con similaire, les technologies bien ´etablies dans le domaine de la s´ecurit´e (comme par exemple le
“bac `a sable”) sont inad´equates dans le cas o`u un grand nombre d'activit´es concurrentes doivent partager
un espace d'adressage. De plus, le traditionnel contrˆole d'acc`es doit ˆetre compl´et´e, dans les applications
massivement concurrentes (“multi-threaded”), par la mise en oeuvre de nouvelles politiques de s´ecurit´e,
assurant par exemple qu'un “thread” ne consomme pas les ressources communes de fa¸con immod´er´ee, ou
ne les corrompt pas, ou encore ne r´ev`ele pas des informations confidentielles `a d'autres “threads” ayant
des droits d'acc`es limit´es.
Notre projet PARSEC (pour “PARall´elisme et S´ECurit´e”, o`u parall´elisme doit ˆetre compris au sens
de “concurrency”) se propose d'´etudier les techniques de programmation parall`ele pour ces nouvelles
applications, en s'int´eressant particuli`erement aux probl`emes de s´ecurit´e qui se font jour dans les syst`emes
de “threads” multiples. Notre objectif principal est de comprendre ce que devrait et pourrait ˆetre un
mod`ele de programmation concurrente efficace et con¸cu avec des pr´eoccupations de s´ecurit´e. Un tel
mod`ele doit `a la fois ˆetre commode et efficace pour programmer le genre d'applications mentionn´ees cidessus,
et offrir des m´ecanismes permettant de mettre en oeuvre des politiques de s´ecurit´e de haut niveau.
Pour atteindre cet objectif nous aurons `a ´etudier des mod`eles bien connus, comme le “multi-threading”
`a la Java, les “threads” Posix, ou encore les mod`eles de m´emoire partag´ee, mais aussi des mod`eles moins
standards, comme le mod`ele coop´eratif qui tend `a ˆetre adopt´e dans les syst`emes de “threads” au niveau
utilisateur, ou le mod`ele synchrone. Nous aurons aussi `a comprendre quelles sont les propri´et´es de sˆuret´e
et de s´ecurit´e `a garantir s'agissant de syst`emes massivement concurrents, comme par exemple la propri´et´e
de “non-interf´erence”, qui n'est pas compl`etement claire dans ce cas, ou la propri´et´e de “disponibilit´e”,
pour assurer par exemple qu'un “thread” particulier ne monopolise pas de ressources partag´ees. Nous
aurons aussi `a concevoir et ´etudier des moyens de garantir ces propri´et´es, par exemple en utilisant et
en adaptant des outils usuels comme les syst`emes de types, les logiques de programmes (logiques de
Floyd-Hoare, temporelles, ou la logique de la s´eparation de Reynolds) ou des m´ecanismes de v´erification
`a l'ex´ecution.
Il y a de nombreuses difficult´es dans cette tˆache. Tout d'abord, la s´emantique de la programmation `a
base de threads est loin d'ˆetre bien ´etablie, pour des raisons vari´ees (d´etaill´ees dans notre proposition).
De plus, la synchronisation reste un art d´elicat, et tout ceci rend ce type de programmation tr`es difficile
et sujet `a erreur, du moins dans le cadre pr´eemptif classique. Il est donc n´ecessaire de concevoir des
techniques pour analyser les programmes concurrents de fa¸con `a ce qu'ils soient “thread safe”. Au del`a de
l'´etude du mod`ele pr´eemptif classique, on peut aussi explorer - et c'est ce que nous ferons - l'utilisation
de “threads” coop´eratifs au niveau du langage de programmation. Ceci est maintenant pr´esent´e comme
un meilleur mod`ele pour la programmation d'applications telles que celles que nous avons ´evoqu´ees,
mais ce mod`ele coop´eratif n'est pas pour autant sans d´efaut. En particulier, les programmes coop´eratifs
doivent imp´erativement coop´erer, pour ne pas priver les autres “threads” de la ressource que constitue le
processeur, et `a ce jour on ignore comment garantir cette propri´et´e pour des programmes ´ecrits dans un
langage suffisamment expressif. Le mˆeme probl`eme se pose dans le cas de la programmation synchrone.
Il reste donc `a faire beaucoup de recherche fondamentale pour aboutir `a la conception d'un mod`ele de
programmation concurrente qui soit raisonnablement sˆur.
3
S'agissant de s´ecurit´e, les applications concurrentes soul`event ´egalement nombre de difficult´es. Comme on
l'a dit plus haut, dans de telles applicationsle contrˆole d'acc`es doit ˆetre compl´et´e par d'autres v´erifications,
pour contrˆoler le flux d'information, et l'usage des ressources. Il est bien connu que la notion de flux
d'information sˆur est difficile `a d´efinir pour les syst`emes concurrents, `a cause en particulier de la vari´et´e
de types de fuites qui peuvent se produire, comme les fuites `a la terminaison ou les fuites dues `a la dur´ee
d'ex´ecution par exemple. De plus, mˆeme pour des notions de flux d'information sˆur relativement faibles,
la plupart des techniques connues (par exemple les syst`emes de types) pour assurer de telles propri´et´es de
s´ecurit´e sont beaucoup trop restrictives pour ˆetre utilisables dans la pratique. Nous croyons que le mod`ele
coop´eratif de la concurrence se pr`ete mieux que le mod`ele pr´eemptif `a une approche langage de l'analyse
du flux d'information, parce que dans ce mod`ele le flot de contrˆole est d´etermin´e au niveau du langage
de programmation, mais cette conviction doit encore ˆetre soutenue par des r´esultats formels. En fait,
quelques questions difficiles concernant le flux d'information sˆur se posent d´ej`a dans un cadre purement
s´equentiel. Par exemple, un traitement ad´equat des exceptions `a la Java manque toujours ; ´egalement, la
notion de flux d'information sˆur (non-interf´erence) devrait ˆetre rendue plus proche, dans une direction ou
l'autre, de ce que garantissent les analyses statiques (syst`emes de types) qui sont con¸cus pour l'assurer.
De mˆeme, et quoique les applications “multi-thread´ees” fournissent une motivation forte pour ´etudier le
contrˆole de ressources, il n'y a toujours pas de technique bien ´etablie qui permettrait, d´ej`a dans le cas
s´equentiel, d'assurer des bornes relativement exactes pour l'utilisation des ressources. Il y a mˆeme des
questions `a r´esoudre concernant le contrˆole d'acc`es, pour comprendre formellement par exemple ce qui
est garanti exactement par des m´ecanismes de protection `a l'ex´ecution en Java.
Nous nous proposons de contribuer e pr´etendons pas que nous allons r´esoudre tous les probl`emes qui
viennent d'ˆetre mentionn´es, mais sur chacun d'eux nous souhaitons proposer des contributions, afin
d'aboutir, `a la fin du projet, `a un fondement solide pour ce qui pourrait constituer un mod`ele de programmation
concurrente sˆur et pens´e pour la s´ecurit´e. Pour ce faire, nous utiliserons dans le projet PARSEC
l'approche langage pour ´etudier de mani`ere formelle les probl`emes de s´ecurit´e tels que le contrˆole d'acc`es,
la s´ecurit´e des flux d'information, le contrˆole de l'usage des ressources, en ce qui concerne particuli`erement
les constructions de programmation concurrente, et plus sp´ecialement la programmation coop´erative. A
cette fin nous avons constitu´e un groupe coh´erent de cinq ´equipes – l'´equipe Concurrency (R. Amadio)
du Laboratoire PPS de l'Universit´e Paris 7 et du CNRS, les ´equipes Everest (G. Barthe) et Mimosa (G.
Boudol) de l'INRIA Sophia Antipolis, l'´equipe Lande (T. Jensen) de l'IRISA et l'´equipe Moscova (J.-J.
L´evy) de l'INRIA Rocquencourt – partageant leur expertise en parall´elisme et/ou s´ecurit´e. Les r´esultats
scientifiques que nous obtiendrons seront communiqu´es lors d'ateliers et de conf´erences, et publi´es dans
des journaux techniques. Nous exp´erimenterons, autant que possible, nos id´ees via des logiciels prototypes,
mais ces logiciels ne sont pas a priori destin´es `a devenir des produits pr´e-comp´etitifs, exploitables
industriellement plus ou moins directement.