Sûreté et sécurité avec focal – SSURF

Le projet propos´e consiste :
- `a ´etudier et caract´eriser les fonctionnalit´es qu'un environnement integr´e de d´eveloppement (IDE) doit
offrir non seulement pour produire des logiciels en conformit´e avec les exigences requises pour atteindre
de hauts niveaux de confiance (EAL 5 6 7), mais aussi pour faciliter le processus d'´evaluation de ces
logiciels selon les standards (IEC61508, CC)
- `a d´evelopper un cadre formel g´en´erique dans lequel peuvent s'exprimer de nombreuses propri´et´es
de s´ecurit´e, comme celles concernant les politiques de contrˆole d'acc`es et leurs implantations, puis `a
consid´erer une implantation de ce cadre dans l'IDE du projet.
Les deux parties de ce projet sont fortement li´ees : tandis que la premi`ere partie a pour vocation de
fournir des th´eories/m´ethodes/outils permettant d'augmenter la confiance dans un syst`eme logiciel dans
un contexte g´en´eral, la deuxi`eme partie peut ˆetre vue comme un fil conducteur du projet, d´edi´e `a un
domaine particulier, celui des propri´et´es de s´ecurit´e, et plus particuli`erement le contrˆole d'acc`es, servant
`a illustrer et `a valider les r´esultats de la premi`ere partie. Evidemment, ces deux composantes du projet
partagent les mˆemes sujets d'int´erˆets : s´emantique, logique, assistant `a la preuve, compilation, r´e´ecriture
et s´ecurit´e des syst`emes informatiques.
Ce projet s'appuiera fortement sur l'atelier fournissant un environnement de d´eveloppement dans lequel
sp´ecifications, propri´et´es, programmes, et preuves peuvent ˆetre d´evelopp´es au mˆeme niveau (les preuves
´etant finalement v´erifi´ees par Coq et les programmes compil´es vers OCaml).